The Linear Temporal Logic of Rewriting (LTLR) is a state/event based extension of LTL with spatial action patterns which represent rewrite events. LTLR describes a property involving both events and state predicates, including mixed properties such as fairness. The Maude LTLR model checker is an explicit state model checker within the Maude system.
Our Maude LTLR model checker can verify LTLR properties under localized fairness assumptions, which are parameterized fairness conditions over certain system entities.
A good example of parametric fairness is provided by object fairness assumptions such as each object o infinitely often enabled to receive a message of the form m(o,q) will receive it infinitely often,
which is universally quantified over all the (possibly dynamically changing) objects o in the system.
Such universal quantification is succinctly captured by the notion of localized fairness; for example, fairness localized to the parameter o in object fairness conditions.
The Maude LTLR model checker is implemented at the C++ level by extending the existing Maude LTL model checker. Unlike our previous rewriting-based LTLR model checker based on a theory and formula transformation, our new implementation do not cause any increase in the state space.
The Maude LTLR model checker is available to download here.
The followings are LTLR model checking examples using our tool. Some of them have localized fairness specification (see our SCP paper for more details).
The Maude Fair LTLR Model checker is illustrated at:
The parameterized fair model checking algorithm and localized fairness are presented in:
The automata-theoretic foundation, design, and implementation of the Maude LTLR Model Checker is illustrated at:
The following papers introduces the temporal logic of rewriting, the family of logics incorporating spatial action patterns.