This version is an experimental implementation of LTLR model checker. The new C++ implementation of the Maude LTLR modal checker is available here.

LTLR Model Checker is the rewriting based model checker in Maude. It uses an existing Maude LTL Model Checker by transforming LTLR system to LTL system using reflective properties of Maude. TLR* is a very simple extension of CTL* which just adds action atoms, in the form of spatial action patterns. It has more expressive power than purely state-based logics like CTL*, or purely action-based logics like A-CTL*. This tool automates the transformation between LTL and LTLR by using Full Maude. For more details, see Reference.


The LTLR Model Checker is written Maude, and consists of a single file tlr.maude. A typical model checking process using LTLR model checker consists of 3 parts; defining a system specification, defining a property specification, and doing model checking the properties.

Pre-defined names

There are 1 pre-defined sort and 3 pre-defined operators; a sort Action, operators top, * and [_]. A sort Action is a sort for a spatial action pattern and a subsort of Formula. A operator top is a top spatial action pattern, a operator * is a "don't care" pattern of a spatial action pattern and a operator [_] is a spatial action identifier, which encloses every spatial action pattern in a formula. This can be redefined if they conflict with names of given system specification modules, as you can see in Example.


Here is the source file of TLR Model Checker (For Maude 2.4. If you use Maude 2.3, please try Old Version.) We also need the latest version of Maude and Full Maude, which can be downloaded at Maude Homepage


The following example is about verifying a property of client-server specification. Before doing medel checking, we should define a system specification of the desired system. In the following specification, because pre-defined operator [_] is used in the specification, I changed an action identifier by redefining a module TLR-ACTIONF-DEF. This example contains only fragment of the whole code. For the full code, please see an example in the source file.

load tlr    *** must be loaded before

*** redefining an action identifier
    protecting TLR-SETTING-OP .
    eq actionFormula = '`{_`} .

select FULL-MAUDE .
loop init .

*** a system specification
    protecting NAT .
    sorts Oid Nat? Cnts Conf .
    subsort Nat < Nat? .
    subsort Cnts < Conf .

    op `{_`,_`} : Oid Nat -> Cnts [ctor] .


    rl [req] : [C,S,N,nil] => [C,S,N,nil] (S <- {C,N}) .
    rl [reply] : (S <- {C,N}) [S] => [S] (C <- {S,f(S,C,N)}) .


The next step is to define a checking module, containing a predicate definition and so on.
    protecting TLR[CLIENT-SERVER] .
    subsort Conf < State .

    op enabled : Action -> Prop .


    eq X [C, S, N, nil] |= enabled({req(C\ C)}) = true .
    eq X |= enabled({req(C\ C)}) = false [owise] .
    eq X (C <- {S,M}) [C,S,N,W] |= enabled({rec(C\ C)}) = true .
    eq X |= enabled({rec(C\ C)}) = false [owise] .
    eq X (S <- {C, N}) [S] |= enabled({reply(S\ S ; C\ C)}) = true .
    eq X |= enabled({reply(S\ S ; C\ C)}) = false [owise] .

    eq Just(A) = (<> [] enabled(A)) -> ([] <> A) .
    eq Fair(A) = ([] <> enabled(A)) -> ([] <> A) .

    eq FairnessAssumptions = 
	Just({req(C\ b)}) /\ Fair({reply(S\ a ; C\ b)}) /\ Fair({rec(C\ b)}) .

    eq init = [a] [b,a,1,nil] [c,a,0,nil] . 


Then, we can do model checking the desired property by the following command. Maude> (tlr check(init,FairnessAssumptions -> <> {rec(C\ b)}) .)
result : true


A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting, Kyungmin Bae and José Meseguer, The 9th International Workshop on Rule-Based Programming, 2008

The Temporal Logic of Rewriting: A Gentle Introduction, José Meseguer, LNCS 5065, 2008

The Temporal Logic of Rewriting, José Meseguer, Technical Report UIUCDCS-R-2007-2815, CS Dept., University of Illinois at Urbana-Champaign, 2007

Last Updated: