Systematic Acceleration in Regular Model Checking

Abstract. Regular model checking is a form of symbolic model checking technique for systems whose states can be represented as finite words over a finite alphabet, where regular sets are used as symbolic representation. A major problem in symbolic model checking of parameterized and infinite-state systems is that fixpoint computations to generate the set of reachable states or the set of reachable loops do not terminate in general. Therefore, acceleration techniques have been developed, which calculate the effect of arbitrarily long sequences of transitions generated by some action. We present a systematic method for using acceleration in regular model checking, for the case where each transition changes at most one position in the word; this includes many parameterized algorithms and algorithms on data structures. The method extracts a maximal (in a certain sense) set of actions from a transition relation. These actions, and systematically obtained compositions of them, are accel...

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Bengt Jonsson, Mayank Saksena
• Keywords: CAV 2007, Formal Methods, Model Checking, Regular Model Checking, Symbolic Model Checking