Performing causality analysis by bounded model checking

Synchronous systems can immediately react to the inputs of their environment which may lead to so-called causal-ity 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 anal-yses 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 analy-sis. To this end, we model the ‘micro step ’ behavior of syn-chronous programs in terms of a transition relation that can be directly used for symbolic model checking. More-over, we show that the obtained model checking problems can be even decided by bounded model-checking prob-lems so that modern SAT-solvers can be used to efficiently solve the causality problem. 1