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

which is universally quantified over all the (possibly dynamically changing) objects `o` infinitely often enabled to receive a message of the form `m(o,q)` will receive it infinitely often,`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:

- Model Checking Linear Temporal Logic of Rewriting Formulas under Localized Fairness, Science of Computer Programming, 2014 (To appear)
- Model Checking LTLR Formulas under Localized Fairness, 9th International Workshop on Rewriting Logic and its Applications (WRLA), 2012

The parameterized fair model checking algorithm and localized fairness are presented in:

- State/Event-Based LTL Model Checking under Parametric Generalized Fairness, 23th International Conference on Computer Aided Verification (CAV), 2011
- Localized Fairness: A Rewriting Semantics, 16th International Conference on Rewriting Techniques and Applications (RTA), 2005

The automata-theoretic foundation, design, and implementation of the Maude LTLR Model Checker is illustrated at:

- The Linear Temporal Logic of Rewriting Maude Model Checker, 8th International Workshop on Rewriting Logic and its Applications (WRLA), 2010
- A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting, The 9th International Workshop on Rule-Based Programming, 2008

The following papers introduces the temporal logic of rewriting, the family of logics incorporating spatial action patterns.

- The Temporal Logic of Rewriting: A Gentle Introduction, LNCS 5065, 2008
- The Temporal Logic of Rewriting, Technical Report UIUCDCS-R-2007-2815, CS Dept., University of Illinois at Urbana-Champaign, 2007