The Linear Temporal Logic of Rewriting Model Checker

Introduction

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.

Usage

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.

• A system specification is a rewriting theory you want to check some properties. You should load Full Maude first before defining it, and the module must follow FULL Maude Syntax restrection; that is, module should be enclosed by parenthesis, and symbols

  ( ) [ ] { } ,

  must be quoted by a symbol `. For more information, please vist Maude Homepage.
• A property specification is a LTLR formula defining given properties. The other model is required including some predicates. This module should include a module of the form TLR[Mod], where Mod is a system specification module. TLR[_] module expression make a module containing special action patterns. To parse a spatial action patterns, tlr.maude must be loaded before defining this module.
• A new command tlr is provided for automatic transformation of the system. It takes two arguments; a state and a LTLR formula. (tlr in Module : check(State, LTLR Formula) .) Or, if a module context is clear, (tlr : check(State, LTLR Formula) .)

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.

Download

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

Example

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

Reference

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