Information Technology Reference
In-Depth Information
protocols specification. Section 4 presents the encodings from multiset rewriting
to process algebra (Section 4.1), and vice versa (Section 4.2). Section 5 provides
the notion of equivalence motivating the encodings. Finally, Section 6 gives some
concluding remarks.
2 Background
In this section, we recall the syntax and formal semantics of multiset rewriting
(MSR) and of process algebras (PA).
2.1 First Order Multiset Rewriting
The language of first-order MSR is defined by the following grammar:
Elements
a
˜
::=
·|a
(
t
)
,
˜
a
˜
Rewriting Rules
r
::=
˜
a
(
x
)
→∃
n
.
b
(
x
,
n
)
Rule sets
r
˜
::=
·|r,
r
˜
Multiset elements are chosen as atomic formulas
a
(
t
) for terms
t
=(
t
1
,...,t
n
)
over some first-order signature
Σ
. We will write ˜
a
(
x
) (resp.,
t
(
x
)) when we want
to emphasize that variables, drawn from
x
, appear in a multiset ˜
a
(resp., a term
t
” will denote multiset union and will implicitly
be considered commutative and associative, while “
). In the sequel, the comma “
,
·
”, the empty multiset, will
act as a neutral element (which will allow us to omit it when convenient). The
operational semantics of MSR is expressed by the following two judgments:
˜
Single rule application
r
˜
:˜
a −→
b
a −→
∗
˜
Iterated rule application
r
˜
:˜
b
and
˜
The multisets ˜
are called
states
and are always ground formulas. The
arrow represents a transition. These judgments are defined as follows:
a
b
˜
˜
(˜
r,
˜
a
(
x
)
→∃
n
.
b
(
x
,
n
)) : (˜
c,
˜
a
[
t
/
x
])
−→
(˜
c,
b
[
t
/
x
,
k
/
n
])
˜
:
˜
b −→
∗
˜
r
˜
:˜
a −→
b
r
˜
c
a −→
∗
˜
a −→
∗
˜
r
˜
:˜
a
r
˜
:˜
c
˜
) is used
to transform a state into a successor state: it identifies a ground instance ˜
The first inference shows how a rewrite rule
r
=˜
a
(
x
)
→∃
n
.
b
(
x
,
n
a
(
t
)of
its antecedent and replaces it with the ground instance
˜
b
(
t
,
k
) of its consequent,
where
k
are fresh constants. Here [
t
/
x
] denotes the substitution (also written
θ
)
x
x
replacing every occurrence of a variable
among
with the corresponding term
t
t
. These rules implement a non-deterministic (in general several rules are
applicable at any step) but sequential computation model (one rule at a time).
Concurrency is captured as the permutability of (some) rule applications. The
remaining rules define
−→
∗
as the reflexive and transitive closure of
−→
.
in
