Systematic Acceleration in Regular Model Checking

10 years 9 months ago
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...
Bengt Jonsson, Mayank Saksena
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CAV
Authors Bengt Jonsson, Mayank Saksena
Comments (0)