µ-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

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:

[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)