ltsmin-mu(5)

SYNOPSIS

LTSmin syntax for Mu Calculus formulas

Table 1. Mu Calculus 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	&&	Logical and
4	\|\|	Logical or
5	X	neXt operator
5	E	Exist a successor
5	A	All successors
6	[edgevar]*	Globally (Always) operator
6	<edgevar>*	Finally (Eventually) operator
6	nu	greatest fixpoint operator
6	mu	least fixpoint operator

* not implemented

Caution

Using the letters X,E or A as state label name might confuse the parser.

nu Z. (A X Z) && (E X true)

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