Language reference/PBES syntax

From MCRL2

Syntax definition

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

Contents

This page describes the concrete syntax of parameterised boolean equation systems (PBESs).

The syntax of parameterised boolean equations and specifications is described, and how they are used in files.

Parameterised boolean equations

Parameterised boolean expressions φ_e:

φe ::= "val" "(" c ")"  |  "true"  |  "false"  |  "!" φe
     |  φe "&&" φe  |  φe "||"  φe  |  φe "=>" φe
     |  "forall" mvd "," ... "," mvd "." φe  |  "exists" mvd "," ... "," mvd "." φe
     |  pvo
mvd  ::=  x "," ... "," x ":" s
pvo  ::=  X  |  X "(" d "," ... "," d ")"

Here mvd represents a multiple variable declaration, and pvo represents a propositional variable occurrence, s represents a sort expression, and d and c represent data expressions of which c is of sort "Bool", Furthermore, X stands for a propositional variable name, and 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 "!" operator has the highest priority, followed by "&&" and "||", followed by "=>", followed by "forall" and "exists". The infix operators "&&", "||" and "=>" associate to the right. These priorities can be overruled with the use of parentheses "(" and ")".

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.

Parameterised boolean equations pb_eqn:

pb_eqn ::= σ pvd "=" φe
σ      ::= "mu"  |  "nu"
pvd    ::=  X  |  X "(" mvd "," ... "," mvd ")"

Here σ represents a fixed point, and pvd represents a propositional variable declaration.

PBES specifications

PBES specifications pbes_spec:

pbes_spec      ::=  pbes_spec_elt*
pbes_spec_elt  ::=  data_spec
                 |  "glob" ( mvd ";" )+
                 |  "pbes" ( pb_eqn ";" )+
                 |  "init" pvo ";"

Here pbes_spec_elt represents a specification element, data_spec a data specification, mvd represents a multiple variable declaration, pbes_eqn a parameterised boolean equation, and pvo a propositional variable occurrence.

We impose the restriction that pbes_spec should contain precisely one occurrence of each of the keywords "pbes" and "init".

Files

Files containing an instance of pbes_spec can be parsed with the tool txt2pbes. For the syntax of the lexical elements, see the page on lexical syntax.

Example files can be found in the examples directory of the svn repository.

---

mu-calculus syntax