Language reference/mu-calculus syntax

From MCRL2

Syntax definition

Lexical syntax Data syntax Process syntax mu-calculus syntax PBES syntax

Contents

The mu-calculus used in mCRL2 is a first-order modal mu-calculus extended with data-depended processes and regular formulas. This page describes the concrete syntax of these mu-calculus formulas, and how it is used in the toolset.

Contents 1 Syntax 1.1 Multiactions 1.2 Action formulas 1.3 Regular formulas 1.4 State formulas 1.5 Files 1.6 Remarks 2 Relations between symbols 3 Examples

Syntax

The syntax of the mu-calculus consists of multiactions, action formulas, regular formulas and state formulas. Next to these, the use of mu-calculus formulas in files is described.

Multiactions

Multiactions ma are defined by:

ma   ::= "tau"  |  pa "|" ... "|" pa
pa   ::= a  |  a "(" d "," ... "," d ")"

Here pa represents a parameterised action, d represents a data expression, and a stands for an action name, which is an identifier.

The constant "tau" represents for the empty multiaction, and pa₀ "|" ... "|" pa_n represents the multiaction consisting of parameterised actions pa_i, for 0 ≤ i ≤ n.

Action formulas

Action formulas α are inductively defined by:

α    ::=  ma  |  "val" "(" c ")"  |  "true"  |  "false"
       |  "!" α  |  α "&&" α  |  α "||" α  |  α "=>" α
       |  "forall" mvd "," ... "," mvd "." α  |  "exists" mvd "," ... "," mvd "." α
       |  |  α "@" t  |  "(" α ")"
mvd  ::=  x "," ... "," x ":" s

Here mvd represents a multiple variable declaration, ma a multiaction, s a sort expression, and c and t represent data expressions of sort "Bool" and "Real", respectively. For technical reasons, t may not have an infix operator, a where clause or a quantifier at the top-level (parentheses should be used instead). Finally, x stands for a data name, which is an identifier.

The "val" operator stands for the value of a boolean data expression, "true" stands for true, "false" for false, "!" for not, "&&" for and, "||" for or, and "=>" for implication. The rules starting with "forall" and "exists" stand for universal and existential quantification. The "@" operator stands for an action formula at the specified time.

The "!" operator has the higher priority, followed by "@", followed by "&&" and "||", followed by "=>", followed by "forall" and "exists". These priorities can be overruled with the use of parentheses "(" and ")". The infix operator "@" associates to the left, while the infix operators "&&", "||" and "=>" associate to the right.

Regular formulas

Regular formulas φ_r are inductively defined by:

φr  ::=  α  |  "nil"  |  φr "." φr  |  φr "+" φr
      |  φr "*"  |  φr "+"  |  "(" φr ")"

Here, α represents an action formula, "nil" represents empty, "." concatenation, infix "+" choice, "*" transitive reflexive closure, and postfix "+" transitive closure.

The unary operators have the highest priority, followed by ".", followed by infix "+". The infix operators associate to the right. These priorities can be overruled with the use of parentheses "(" and ")".

State formulas

State formulas φ_s are inductively defined by:

φs  ::=  "val" "(" c ")"  |  "true"  |  "false"
      |  "!" φs  |  φs "&&" φs  |  φs "||" φs  |  φs "=>" φs
      |  "forall" mvd "," ... "," mvd "." φs  |  "exists" mvd "," ... "," mvd "." φs 
      |  "[" φr "]" φs  |  "<" φr ">" φs
      |  "nu" pvdi "." φs  |  "mu" pvdi "." φs  |  pvo 
      |  "yaled" "@" t  |  "delay" "@" t  |  "yaled"  |  "delay" 
      |  "(" φs ")"
pvdi ::=  X  |  X "(" vdi "," ... "," vdi ")"
pvo  ::=  X  |  X "(" d "," ... "," d ")"
vdi  ::=  x ":" s "=" d

Here pvdi represents a propositional variable declaration and initialisation, pvo a propositional variable occurrence, vdi a variable declaration plus initialisation, mvd a multiple variable declaration, φ_r a regular formula, s a sort expression, and d, c and t represent data expressions of which c is of sort "Bool" and t is of sort "Real". For technical reasons, t may not have an infix operator, a where clause or a quantifier at the top-level (parentheses should be used instead). Furthermore, X stands for a propositional variable name, x for a data variable name, which are both identifiers.

The "val" operator stands for the value of a boolean data expression, "true" stands for true, "false" for false, "!" for not, "&&" for and, "||" for or, and "=>" for implication. The rules starting with "forall" and "exists" stand for universal and existential quantification, the rules "[" φ_r "]" φ_s and "<" φ_r ">" φ_s for the must and may operators, and the rules starting with "nu" and "mu" for the greatest and smallest fixed point operators. The timed "delay" and "yaled" operators stand for the possibility to delay until time t, or not. The untimed "delay" and "yaled" operators stand for the possibility to delay forever, or not.

The prefix operators and the must and may operators have the highest priority, followed by "&&" and "||", followed by "=>", followed by "forall", "exists", "nu" and "mu". The infix operators "&&", "||" and "=>" associate to the right. These priorities can be overruled with the use of parentheses "(" and ")".

The must and may operators have the following meaning. In a state of the state space a formula "[φ_r]φ_s" is valid if all paths that start in this state and satisfy φ_r, lead to a state where φ_s is valid. In a state of the state space a formula "<φ_r>φ_s" is valid if there exists a path that starts in this state, satisfies φ_r and leads to a state where φ_s is valid.

The following restrictions apply to propositional variables:

• monotonicity: every occurrence of a propositional variable should be in a scope such that the number of "!" operators plus the number of left-hand sides of the "=>" operator is even;
• no overloading: it is not allowed to declare two propositional variables with the same name but with a different type.

Files

The tool lps2pbes uses mu-calculus formulas files, which contain precisely one state formula. For the syntax of the lexical elements, see the page on lexical syntax.

The suggested extension of formula files is ".mcf".

Remarks

Data variables declared using "forall", "exists", "nu" and "mu" quantifiers, we have the following variable conventions:

• Each occurrence of a variable is bound by the nearest quantifier in scope of which the bound variable has the same name and the same number of arguments.
• Variables introduced by a "nu" or "mu" quantifier may not conflict, i.e. all names of data variables have to be distinct.

Relations between symbols

Besides the well-known relations between symbols of first-order logic, the following relations hold for regular formulas:

[nil]φs   = [false*]φs
[φr.ψr]φs = [φr][ψr]φs
[φr|ψr]φs = [φr]φs && [ψr]φs
[φr*]φs   = nu X.(φs && [φr]X), if X is fresh for φs
[φr+]φs   = [φr.φr*]φs

<nil>φs   = <false*>φs
<φr.ψr>φs = <φr><ψr>φs
<φr|ψr>φs = <φr>φs || <φr>φs
<φr*>φs   = mu X.(φs || <φr>X), if X is fresh for φs
<φr+>φs   = <φr.φr*>φs

The following relations hold for the modal operators, where φ_s(!X) represents substitution of !X for every free occurrence of X in φ_s:

[φr]φs    = !<φr>!φs
nu X.φs   = !mu X.!φs(!X)

We have the following identities for the "delay" and "yaled" operators:

delay     = forall t: Real. delay@t
yaled@t   = !(delay@t)
yaled     = !delay

Examples

Freedom of deadlock:

[true*]<true>true

Action b may not happen after an action c, unless an action a occurs after this c and before this b:

[(!c)*.c.((!a && !b)* + a.(!c)*.c)*.b]false

The same formula but now b may not occur initially:

[((!a && !b)* + a.(!c)*.c)*.b]false

There exists an infinite sequence of a.b.c's:

<true*>nu X.<a.b.c>X

These formulas are equivalent to the following formulas in which no regular operations, i.e. empty path "nil", concatenation ".", choice "+", transitive reflexive closure "*" and transitive closure "+", occur:

nu X.(<true>true && [true]X)
nu X.([c] nu Y.([b]false && (nu Z.(Y && [!a && !b]Z) && [a] nu Z.([c]Y && [!c]Z))) && [!c]X)
nu X.([b]false && (nu Y.(X && [!a && !b]Y) && [a] nu Y.([c]X && [!c]Y)))
mu X.(nu Y.(<a><b><c>Y) || <true>X)

---

Process syntax

PBES syntax