A model checker typically supports two different levels of specification: (1) a system specification level, in which the concurrent system to be analyzed is formalized; and (2) a property specification level, in which the properties to be model checked—for example, temporal logic formulae—are specified. The Maude LTL model
checker has been designed with the goal of combining a very expressive and general system specification language (Maude [1]) with an advanced on-the-fly explicit-state LTL model checking engine.
The first two authors’ work has been partially supported by DARPA through Air Force Research Laboratory Contract F30602-97-C-0312,
NSF grants CCR-9900326 and CCR-9900334, ONR Contract N00012-99-C-0198, and DARPA through Air Force Research Laboratory Contract
F30602-02-C-0130. The last two authors’ work is also supported in part by the ONR Grant N00014-02-1-0715.