Performing causality analysis by bounded model checking

Synchronous systems can immediately react to the inputs of their environment which may lead to so-called causality cycles between actions and their trigger conditions. Systems with causality cycles may not be consistent or may become nondeterministic. For this reason, compilers for synchronous languages usually employ special analyses to guarantee a predictable runtime behavior of the considered programs. In this paper, we show how causality analysis can be formulated as a model checking problem, so that all of the sophisticated algorithms originally developed for model checking can now also be used for causality analysis. To this end, we model the dasiaemicro steppsila behavior of synchronous programs in terms of a transition relation that can be directly used for symbolic model checking. Moreover, we show that the obtained model checking problems can be even decided by bounded model-checking problems so that modern SAT-solvers can be used to efficiently solve the causality problem.