A concurrent system can be naturally specified as a rewrite theory (Σ,E,R). Under simple conditions, narrowing with rules R modulo the equations E can be used to both represent the system's state space by means of terms with logical variables and for model checking verification of LTL properties. Folding abstraction may approximate infinite logical reachable subsystem into a finite logical system. The Maude LTL logical model checker (LMC) tool can verify LTL properties over such logical states from a pattern of (possibly infinite) initial states using the (folded) logical state space.
Using this method, one of four outcomes is possible: (i) a fixpoint (a finite state space) is reached and the formula is fully verified; (ii) no such fixpoint is reached and the formula is only verified up to a given bound; (iii) a real counterexample is found and reported; or (iv) a possibly spurious counterexample is found and reported.
The main feature and the usage of the Maude LMC tool are briefly described in this tutorial, where we illustrate the LMC tool using the examples below.
The following paper explains approximation methods for logical model checking:
The narrowing-based symbolic model checking method is introduced in:
The Maude LMC model checker is available to download here.
The followings are logical model checking examples using our tool.