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.
( ) [ ] { } ,must be quoted by a symbol `. For more information, please vist Maude Homepage.
(tlr in Module : check(State, LTLR Formula) .)
Or, if a module context is clear,
(tlr : check(State, LTLR Formula) .)
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 fmod TLR-ACTIONF-DEF is protecting TLR-SETTING-OP . eq actionFormula = '`{_`} . endfm select FULL-MAUDE . loop init . *** a system specification (mod CLIENT-SERVER is 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)}) . ... endm)The next step is to define a checking module, containing a predicate definition and so on.
(mod TLR-CLIENT-SERVER-CHECK is 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] . ... endm)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, The 9th International Workshop on Rule-Based Programming, 2008
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
Last Updated: