Information Technology Reference
In-Depth Information
3 The mCRL2 Specification Language
We provide a brief overview of the
mCRL2
specification language and toolset. For
more details we refer to [7] and to the
mCRL2
website
1
.
The basic notion in
mCRL2
is the action. Actions represent atomic events
and can be parametrized with data. Actions in
mCRL2
can be synchronized. In
this case, we speak of multiactions which are constructed from other actions or
multiactions using the so-called synchronization operator
|
, like the multiaction
a
b
of simultaneous doing the actions
a
and
b
. The special action
τ
(tau) is used
to refer to an internal unobservable action. Processes are defined by process
expressions, which are compositions of actions and multiactions using a number
of operators. The basic operators include
|
-
deadlock
or
inaction
δ
, which does not display any behavior;
-
alternative composition
, written as
p
+
q
, which represents a non-deterministic
choice between the processes
p
and
q
;
-
sequential composition
, written
p
·
q
, which means that
q
is executed after
p
,
assuming that
p
terminates;
-
the
conditional operator
or
if-then-else
construct, written as
c
→
p
q
,where
c
is a data expression that evaluates to true or false;
-
summation
Σ
d
:
D
p
where
p
is a process expression in which the data vari-
able
d
may occur, used to quantify over a data domain
D
;
-
the
at operator
a
@
t
, which indicates that the multiaction
a
happens at the
time
t
;
-
parallel composition
or
merge
p
q
, which interleaves and synchronizes the
multiactions of
p
with those of
q
, where synchronization is governed by an
implicit communication function;
-
the
restriction operator
∇
V
(
p
), where
V
specifies which actions from
p
are
allowed to occur, and, complementary, the
encapsulation
∂
H
(
p
), where
H
is
a set of action names that are not allowed to occur;
-
the
renaming operator
ρ
R
(
p
), where
R
is a set of renamings of the form
a
b
,
meaning that every occurrence of action
a
in
p
is replaced by the action
b
;
→
-
the
communication operator
Γ
C
(
p
), where
C
is a set of communications of
the form
a
0
|
...
|
a
n
→
c
, which means that every group of actions
a
0
|
...
|
a
n
within a multiaction is replaced by
c
.
The
mCRL2
language provides a number of built-in data types such as boolean,
natural and positive numbers, integers and real numbers. All standard arithmetic
operations for them are predefined. Custom data type definition mechanisms in
mCRL2
allow users to declare new sorts, constructors and functions. A structured
type in
mCRL2
can be declared by a construct of the form
c
1
(
p
1
:
S
1
,...,p
k
1
:
S
k
1
)?
r
1
c
n
(
p
n
:
S
n
,...,p
k
n
:
S
k
n
)?
r
n
;
sort
S
=
struct
|
...
|
This construct defines the type
S
together with constructors
c
i
:
S
i
×
S
ki
i
...
×
→
S
, projections
p
i
:
S
S
i
, and recognizers
r
i
:
S
→
→
Bool
. Various examples of
1
http://mcrl2.org/mcrl2/wiki/index.php
