Mapping for Specification Patterns (LTL)

This page describes mappings for property patterns in linear temporal logic (LTL), for buchi Automata and for Property Sequence Charts.

Some of the mappings use the weak until operator (W) which is related to the strong until operator (U) by the following equivalences:

        p W q = ([]p) | (p U q)
              = <>(!p) -> (p U q)
              = p U (q | []p)
        

This operator often makes the mappings easier to understand (thanks to William Chan for suggesting this).

Pattern mappings are parametric. They are presented in terms of place-holder symbols (e.g. P,Q,R,S) that are to be replaced by users when writing actual specifications. These place holders are filled with descriptions of specific system states or events of interest. These descriptions can be more complex than just a single proposition or event name. In this pages we describes the mappings by considering the place-holder symbols as single messages exchanged by the system (e.g., the place-holder P can be considered as the message label p). More complex mapping can be obtained by simply using the Basic Rules and the Composition Rules.

For information about the meaning of scopes look here.

Information about the entire pattern system is available at the Specification Patterns Home Page.

Absence P is false : Scope LTL LTL2BA PSC2BA Globally [](!P) Before R <>R -> (!P U R) After Q [](Q -> [](!P)) Between Q and R []((Q & !R & <>R) -> (!P U R)) (*) After Q until R [](Q & !R -> (!P W R)) Existence P becomes true : Scope LTL LTL2BA PSC2BA Globally <>(P) (*) Before R !R W (P & !R) After Q Original formulae [](!Q) | <>(Q & <>P)) Our formulae [](Q -> <>(P)) (*) Between Q and R [](Q & !R -> (!R W (P & !R))) (*) After Q until R [](Q & !R -> (!R U (P & !R))) Bounded Existence These mappings illustrate one instance of the bounded existence pattern, where the bound is at most 2 designated states. Other bounds can be specified by variations on this mapping. transitions to P-states occur at most 2 times : Scope LTL LTL2BA PSC2BA Globally (!P W (P W (!P W (P W []!P)))) Before R <>R -> ((!P & !R) U (R | ((P & !R) U (R | ((!P & !R) U (R | ((P & !R) U (R | (!P U R))))))))) After Q Original formulae <>Q -> (!Q U (Q & (!P W (P W (!P W (P W []!P)))))) Our formulae [](P -> (!P U ((P U ((!P U (P U ([]!P | []P)) | []!P) | []P)) | []!P))) Between Q and R []((Q & <>R) -> ((!P & !R) U (R | ((P & !R) U (R | ((!P & !R) U (R | ((P & !R) U (R | (!P U R)))))))))) After Q until R [](Q -> ((!P & !R) U (R | ((P & !R) U (R | ((!P & !R) U (R | ((P & !R) U (R | (!P W R) | []P))))))))) Universality P is true : Scope LTL LTL2BA PSC2BA Globally [](P) Before R <>R -> (P U R) After Q [](Q -> [](P)) Between Q and R []((Q & !R & <>R) -> (P U R)) (*) After Q until R [](Q & !R -> (P W R)) Precedence S precedes P: Scope LTL LTL2BA PSC2BA (*) Globally !P W S (*) Before R <>R -> (!P U (S | R)) (*) After Q Original formulae []!Q | <>(Q & (!P W S)) Our formulae [] (Q -> ( !P W S )) (*) Between Q and R []((Q & !R & <>R) -> (!P U (S | R))) (*) After Q until R [](Q & !R -> (!P W (S | R))) Response S responds to P : Scope LTL LTL2BA PSC2BA Globally [](P -> <>S) (*) Before R <>R -> (P -> (!R U (S & !R))) U R After Q [](Q -> [](P -> <>S)) (*) Between Q and R []((Q & !R & <>R) -> (P -> (!R U (S & !R))) U R) (*) After Q until R [](Q & !R -> ((P -> (!R U (S & !R))) W R) Precedence Chain This illustrates the 2 cause-1 effect precedence chain. S, T precedes P: Scope LTL LTL2BA PSC2BA Globally <>P -> (!P U (S & !P & o(!P U T))) Before R <>R -> (!P U (R | (S & !P & o(!P U T)))) After Q Original formulae ([]!Q) | (!Q U (Q & <>P -> (!P U (S & !P & o(!P U T)))) Our formulae [](Q -> (<>P -> (!P U (S & !P & o(!P U T))))) Between Q and R []((Q & <>R) -> (!P U (R | (S & !P & o(!P U T))))) After Q until R [](Q -> (<>P -> (!P U (R | (S & !P & o(!P U T)))))) This illustrates the 1 cause-2 effect precedence chain. P precedes (S, T): Scope LTL LTL2BA PSC2BA Globally Original formulae (<>(S & o<>T)) -> ((!S) U P)) Our formulae (<>(S & o<>T)) -> (!(S & o<>T) U P) Before R <>R -> ((!(S & (!R) & o(!R U (T & !R)))) U (R | P)) After Q Original formulae ([]!Q) | ((!Q) U (Q & ((<>(S & o<>T)) -> ((!S) U P))) Our formulae [](Q -> (<>(S & o<>T) -> (!(S & o <>T) U P)) ) Between Q and R []((Q & <>R) -> ((!(S & (!R) & o(!R U (T & !R)))) U (R | P))) After Q until R Original formulae [](Q -> (!(S & (!R) & o(!R U (T & !R))) U (R | P) | [](!(S & o<>T)))) Our formulae []((Q & <>R) -> ((!(S & (!R) & o(!R U (T & !R)))) W (R | P))) = [](Q -> ((!(S & (!R) & o(!R U (T & !R)))) U ((R | P) | [](!(S & (!R) & o(!R U (T & !R))))))) Response Chain This illustrates the 2 stimulus-1 response chain. P responds to S,T: Scope LTL LTL2BA PSC2BA Globally [] (S & o<> T -> o(<>(T & <> P))) Before R Original formulae <>R -> (S & o(!R U T) -> o(!R U (T & <> P))) U R Our formulae <>R -> (S & o(!R U (!R & T)) -> o(!R U (!R & P))) U R After Q Original formulae [] (Q -> [] (S & o<> T -> o(!T U (T & <> P)))) Our formulae [] (Q -> [] (S & o<> T -> o(F (T & <> P)))) Between Q and R Original formulae [] ((Q & <>R) -> (S & o(!R U T) -> o(!R U (T & <> P))) U R) Our formulae [] ((Q & <>R) -> (S & o(!R U T) -> o(!R U (!R & P))) U R) After Q until R Original formulae [] (Q -> (S & o(!R U T) -> o(!R U (T & <> P))) U (R | [] (S & o(!R U T) -> o(!R U (T & <> P))))) Our formulae [] (Q -> (S & o(!R U T) -> o(!R U (!R & P))) U (R | [] (S & o(!R U T) -> o(!R U (!R & P))))) This illustrates the 1 stimulus-2 response chain. S,T responds to P: Scope LTL LTL2BA PSC2BA Globally [] (P -> <>(S & o<>T)) Before R <>R -> (P -> (!R U (S & !R & o(!R U T)))) U R After Q [] (Q -> [] (P -> (S & o<> T))) Between Q and R [] ((Q & <>R) -> (P -> (!R U (S & !R & o(!R U T)))) U R) After Q until R Original formulae [] (Q -> (P -> (!R U (S & !R & o(!R U T)))) U (R | [] (P -> (S & o<> T)))) Our formulae [](Q -> (P -> (!R U (S & !R & o(!R U T)))) U (R | [] (!R U (S & !R & o(!R U T)))))

Paola ::©www.di.univaq.it/inverard
Marco ::©www.di.univaq.it/marco.autili
Patrizio ::©www.di.univaq.it/pellicci
::last modified: 10th Sep 2005