SYNOPSIS

LTSmin syntax for Linear Temporal Logic formulas

DESCRIPTION

Table 1. LTL operators and priority
Priority Operator Meaning

0

true

constant true

0

false

constant false

1

==

test operator (state variable name==number)

2

!

Logical negation

3

[]

Globally (Always) operator

3

<>

Finally (Eventually) operator

3

X

neXt operator

4

&&

Logical and

5

||

Logical or

6

<->

Logical equivalence

7

->

Logical implication

8

U

Until operator

8

R

Release operator
Caution
 Using the letters X,U or R as state label name might confuse the parser.

EXAMPLE

! ([] ( (phil_0 == 1) -> <> phil_0 == 2) )

For variable naming consult the --labels option in the PINS tools.

SEE ALSO

ltsmin(7), dve2lts-seq(1), dve2lts-mc(1), etf2lts-seq(1), etf2lts-mc(1), prom2lts-seq(1), prom2lts-mc(1) ltsmin-type-system(5)