README-ltlr.md

The Maude Linear Temporal Logic of Rewriting Model Checker

Introduction

The Linear Temporal Logic of Rewriting (LTLR) is a state/event based extension of LTL with spatial action patterns representing rewrite events. LTLR describes a property that involves 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 tool 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 that is 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.

Examples

Below are examples of LTLR model checking with our tool. Some of them have localized fairness specifications. More details about the tool and examples can be found here.

• Evolving Dining Philosophers (c.f., Classical Dining Philosophers)
• Blanced Sliding Window Protocol
• Simple Client-Server model
• Dekker's Algorithm
• Bounded retransmission protocol
• Unordered-channel
• Position fairness

References

The Maude Fair LTLR Model checker is illustrated in:

• Model Checking Linear Temporal Logic of Rewriting Formulas under Localized Fairness, by Kyungmin Bae and José Meseguer, Science of Computer Programming 99, 2015

• Model Checking LTLR Formulas under Localized Fairness, by Kyungmin Bae and José Meseguer, 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, by Kyungmin Bae and José Meseguer, International Conference on Computer Aided Verification (CAV), 2011

• Localized Fairness: A Rewriting Semantics, by José Meseguer, 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, by Kyungmin Bae and José Meseguer, International Workshop on Rewriting Logic and its Applications (WRLA), 2010

• A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting, by Kyungmin Bae and José Meseguer,
  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, by José Meseguer, Concurrency, Graphs and Models, vol 5065 of LNCS. Springer, 2008

• The Temporal Logic of Rewriting, by José Meseguer, Technical report, University of Illinois at Urbana-Champaign, 2007. http://hdl.handle.net/2142/11293