The Effect of Transition Granularity in the Model Checking of Reactive Systems

Abstract

The Theta model checking framework offers the eXtended Symbolic Transition System (XSTS) formalism as a target language for the transformation of high-level models to verify. In XSTS, multiple symbolic transitions can be defined by imperative and declarative statements. The language is flexible enough to offer a broad variety of expressing the semantics of high-level models (e.g., statecharts). Two extremes are i) encoding every (possibly non-deterministic) atomic behavior of the high-level model into a single transition (big steps with only stable states) or ii) modeling the control flow of the computation of the next state (small steps with transient states). Experience shows that big steps are efficient in reducing the state space but sometimes yield transitions that are too complex to handle. Furthermore, internal non-determinism in "big-step" transitions is hard to back-annotate from a counterexample to the high-level model. We examine the effect of transition granularity on model checking by applying a post-processing step that can split "big-step" transitions.