µ-Calculus

The µ-calculus used in mCRL2 is the modal µ-calculus extended with data. It also supports regular formulas as these allow to express many common properties more concisely. . This page describes the concrete syntax of these µ-calculus formulas, and how it is used in the toolset.

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

Multi-actions

Multi-actions are defined by the following syntax.

ActionList MultAct

```ActionList ::=  `Action` ('|' `Action`)*
MultAct    ::=  'tau' |
`ActionList`
```

The constant `tau` represents for the empty multi-action, `a0 | ... | an` represents the multi-action consisting of parameterised actions `ai`, for `0 ≤ i ≤ n`.

Action formulas

Action formulas α are defined by:

DataValExpr ActFrm

```DataValExpr ::=  'val' '(' `DataExpr` ')'
ActFrm      ::=  `DataValExpr` |
`MultAct` |
'(' `ActFrm` ')' |
'true' |
'false' |
'forall' `VarsDeclList` '.' `ActFrm` |
'exists' `VarsDeclList` '.' `ActFrm` |
`ActFrm` '=>' `ActFrm` |
`ActFrm` '||' `ActFrm` |
`ActFrm` '&&' `ActFrm` |
`ActFrm` '@' `DataExpr` |
'!' `ActFrm`
```

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 are defined by:

RegFrm

```RegFrm ::=  `ActFrm` |
'(' `RegFrm` ')' |
`RegFrm` '+' `RegFrm` |
`RegFrm` '.' `RegFrm` |
`RegFrm` '*' |
`RegFrm` '+'
```

Here, `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 are defined by:

StateVarAssignment StateVarAssignmentList StateVarDecl StateFrm

```StateVarAssignment     ::=  `Id` ':' `SortExpr` '=' `DataExpr`
StateVarAssignmentList ::=  `StateVarAssignment` (',' `StateVarAssignment`)*
StateVarDecl           ::=  `Id` ('(' `StateVarAssignmentList` ')')?
StateFrm               ::=  `DataValExpr` |
'(' `StateFrm` ')' |
'true' |
'false' |
`Id` ('(' `DataExprList` ')')? |
'delay' ('@' `DataExpr`)? |
'yaled' ('@' `DataExpr`)? |
'mu' `StateVarDecl` '.' `StateFrm` |
'nu' `StateVarDecl` '.' `StateFrm` |
'forall' `VarsDeclList` '.' `StateFrm` |
'exists' `VarsDeclList` '.' `StateFrm` |
'inf' `VarsDeclList` '.' `StateFrm` |
'sup' `VarsDeclList` '.' `StateFrm` |
'sum' `VarsDeclList` '.' `StateFrm` |
`StateFrm` '+' `StateFrm` |
`DataValExpr` '*' `StateFrm` |
`StateFrm` '*' `DataValExpr` |
`StateFrm` '=>' `StateFrm` |
`StateFrm` '||' `StateFrm` |
`StateFrm` '&&' `StateFrm` |
'[' `RegFrm` ']' `StateFrm` |
'<' `RegFrm` '>' `StateFrm` |
'-' `StateFrm` |
'!' `StateFrm`
```

Here `StateVarDecl` represents a propositional variable declaration and initialisation with a list of assignments (`StateVarAssignment`).

The `val` operator used in `DataExprVal` 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 `[` `RegFrm` `]` `StateFrm` and `<` `RegFrm` `>` `StateFrm` 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 a certain time, 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.

Note

The tool lps2pbes uses mu-calculus formulas files, which contain precisely one state formula.

Note

The suggested extension of formula files is “.mcf”.

Note

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

```[true*]<true>true
```

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

```[true*.c.!a*.b]false
```

The action `b` may not occur unless an action `a` happens first:

```[!a*.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 && [!a]Y) && [true]X)
nu X.([b]false && [!a]X)
mu X.(nu Y.(<a><b><c>Y) || <true>X)
```