=Paper=
{{Paper
|id=None
|storemode=property
|title=Process Refinement and Asynchronous Composition with Modalities
|pdfUrl=https://ceur-ws.org/Vol-827/30_DorsafElhog-Benzina_article.pdf
|volume=Vol-827
|dblpUrl=https://dblp.org/rec/conf/acsd/Elhog-BenzinaHH10
}}
==Process Refinement and Asynchronous Composition with Modalities==
https://ceur-ws.org/Vol-827/30_DorsafElhog-Benzina_article.pdf
Process Refinement and Asynchronous
Composition with Modalities
Dorsaf Elhog-Benzina1 , Serge Haddad1 , and Rolf Hennicker2
1
LSV, CNRS & Ecole Normale Supérieure de Cachan
94235 CACHAN, 61 avenue du Président Wilson, France
{elhog, haddad}@lsv.ens-cachan.fr
2
Institut für Informatik Universität München
Oettingenstraße 67 D-80538 München, Germany
hennicke@pst.ifi.lmu.de
Abstract. We propose a framework for the specification of infinite state
systems based on Petri nets with distinguished may- and must-transitions
(called modalities) which specify the allowed and the required behavior
of refinements and hence of implementations. Formally, refinements are
defined by relating the modal language specifications generated by two
modal Petri nets according to the refinement relation for modal language
specifications. We show that this refinement relation is decidable if the
underlying modal Petri nets are weakly deterministic. We also show that
the membership problem for the class of weakly deterministic modal
Petri nets is decidable. As an important application of our approach we
consider I/O-Petri nets which are obtained by asynchronous composition
and thus exhibit inherently an infinite behavior.
Key words: Modal language specification and refinement, modal Petri
net, weak determinacy, asynchronous composition, infinite state system.
1 Introduction
Specification in component-based software products. In component based
software development, specification is an important phase of the components’
life cycle. It aims to produce a formal description of the component’s desired
properties and behavior. A behavior specification can be presented either in
terms of transition systems or in terms of logic, which both cannot be processed
by a machine. Thus an implementation phase is required to produce concrete
executable programs.
Modal specifications. Modal specifications have been introduced in [11] as a
formal model for specification and implementation. A modal specification explic-
itly distinguishes between required actions and allowed ones. Required actions,
denoted with the modality must, are compulsory in all possible implementations
while allowed actions, denoted with the modality may, may happen but are not
mandatory for an implementation. An implementation is seen as a specific spec-
ification in which all actions are required. Modal specifications are adequate for
Recent Advances in Petri Nets and Concurrency, S. Donatelli, J. Kleijn, R.J. Machado, J.M. Fernandes
(eds.), CEUR Workshop Proceedings, ISSN 1613-0073, Jan/2012, pp. 385–401.
386 Petri Nets & Concurrency Elhog-Benzina, Haddad, and Hennicker
2 Elhog-Benzina, Haddad and Hennicker
loose specifications as decisions can be delayed to later steps of the component’s
life cycle. Two different modal formalisms have been adopted in the literature,
the first one, introduced in [8], is based on transition systems while the sec-
ond one, introduced in [16], is a language-based model defining modal language
specifications.
Modal refinement. A transformation step from a more abstract specification
to a more concrete one is called a refinement. It produces a specification that is
more precise, i.e. has less possible implementations. It follows that the set of im-
plementations of a refinement is included in the set of possible implementations
of the original specification.
Computational issues. While dealing with modal specifications, three main
decision problems have been raised:
– (C) Consistency problem: Deciding whether a modal specification is con-
sistent, i.e deciding whether it admits an implementation. Consistency is
guaranteed for modal transition systems by definition [11] as every required
transition is also an allowed one. In the case of mixed transition systems,
i.e. if must-transitions are not necessarily may-transitions, the consistency
decision problem is EXPTIME-complete in the size of the specification [2].
A better result is obtained with modal language specifications since a poly-
nomial time algorithm has been proposed in [16].
– (CI) Common implementation: Deciding whether k > 1 modal specifica-
tions have a common implementation. Deciding common implementation of
k modal transition systems is PSPACE-hard in the sum of the sizes of the
k specifications [1] while it is EXPTIME-complete when dealing with mixed
transition systems [2].
– (TR) Thorough refinement: Deciding whether one modal specification S
thoroughly refines another modal specification S ′ , i.e deciding whether the
class of possible implementations of S is included in the class of possible
implementations of S ′ . The problem is also PSPACE-hard if S and S ′ are
modeled with modal transition systems and it is EXPTIME-complete when
they are modeled with mixed transition systems.
Limits of the existing formalisms. Both formalisms consider finite state sys-
tems. This restriction limits the existing approaches to synchronous composition.
In fact asynchronous composition introduces a delay between the actions of send-
ing and receiving a message between the communication partners. For instance,
if a sender is always active while a receiver is always blocked, we naturally obtain
an infinite state system.
Our contribution. We aim in this paper to deal with asynchronous composi-
tion of modal specifications while keeping most of the problems decidable. Petri
nets seem to be an appropriate formalism to our needs since they allow for a
finite representation of infinite state systems. Automata with queues might be
another alternative for modeling infinite state systems, but all significant prob-
lems (e.g. the reachability problem) are known to be undecidable while they are
decidable when considering deterministic Petri nets. In our approach we consider
Refinement and composition with modalities Petri Nets & Concurrency – 387
Process Refinement and Asynchronous Composition with Modalities 3
Petri nets with silent transitions and we define the generalized notion of a weakly
deterministic Petri net, as a variant of deterministic Petri nets that keeps decid-
ability for our targeted decision problems. We also follow a language approach
and use weakly deterministic Petri nets as a device to generate languages in the
same way as Raclet et. al. use deterministic finite transition systems as a device
to generate regular languages. Moreover, we extend Petri nets by modalities for
the transitions. In this setting, we are mainly interested in the following decision
problems:
1. Decide whether a given Petri net is weakly deterministic.
2. Decide whether a given language generated by a Petri net N is included in
the language generated by a given weakly deterministic Petri net N ′ .
3. Decide whether a given modal Petri net is (modally) weakly deterministic.
4. Given two modal language specifications S(M) and S(M) generated by
two weakly deterministic modal Petri nets M and M′ respectively, decide
whether S(M′ ) is a modal language specification refinement of S(M).
We show that all the above mentioned problems are decidable. As a particular
important application of our approach we consider I/O-Petri nets which are
obtained by asynchronous composition and thus exhibit an infinite behavior.
Since transitions with internal labels, in particular those obtained by internal
communications, are not relevant for refinements we abstract them away by a
general abstraction operator on modal I/O-Petri nets.
Outline of the paper. We proceed by reviewing in Sect. 2 modal language
specifications and the associated notion of refinement. In Sect. 3 we summarize
basics of Petri net theory and introduce weakly deterministic Petri nets. We
then introduce modal Petri nets, their generated language specifications and
we extend the concept of weak determinacy to Petri nets with modalities. In
Sect. 4, we consider modal Petri nets over an I/O-alphabet (with distinguished
input, output, and internal labels) and define their asynchronous composition.
We also define the abstraction of an I/O-Petri net by relabeling internal labels
to the empty word. In Sect. 5 we present the decision algorithms of the issues
mentioned above. Finally we conclude in Sect. 6.
2 Modal Language Specifications
Modal specification was first introduced by Larsen and Thomsen in [11] with
finite state modal transition systems by defining restrictions on specifications
transitions by the mean of may (allowed) and must (required) modalities. This
notion has then been adapted by Raclet in his PhD thesis who applied it to reg-
ular languages. Finite transition systems are low level models based on states,
which limits the level of abstraction of the specification. They also lead to state
number explosion while composing systems with an important number of states.
Moreover, the complexity of the decision problems discussed above are better
with modal languages than with modal transition systems. Besides, modal re-
finement is sound and complete with the language-based formalism while it is
388 Petri Nets & Concurrency Elhog-Benzina, Haddad, and Hennicker
4 Elhog-Benzina, Haddad and Hennicker
non-complete with transition system based formalism [9]. So a language approach
is more convenient to deal with modal specification issues. Next we review the
definition of modal language specification and refinement between specifications
as introduced in [16].
Definition 1 (Modal language specification). A modal language specifi-
cation S over an alphabet Σ is a triple hL, may, musti where L ⊆ Σ ∗ is a
prefix-closed language over Σ and may, must : L → P (Σ) are partial functions.
For every trace u ∈ L,
– a ∈ may(u) means that the action a is allowed after u,
– a ∈ must(u) means that the action a is required after u,1
– a∈/ may(u) means that a is forbidden after u.
The modal language specification S is consistent if the following two conditions
hold:
(C1) ∀ u ∈ L must(u) ⊆ may(u)
(C2) ∀ u ∈ L may(u) = {a ∈ Σ | u.a ∈ L}
Example 1. Let us consider the example of a message producer and a message
consumer represented in figure 1.
s0 s0
m in out m
s1 s1
(a) (b)
Fig. 1. Modal transition systems for a producer (a) and a consumer (b)
in
In the producer system, transition s0 → s1 is allowed but not required
m
(dashed line) while transition s1 → s0 is required (continuous line). In the con-
sumer model, all transitions are required. The languages associated with the the
producer is L ≡ (in.m)∗ + in.(m.in)∗ . The associated modal language specifica-
tion is then hL, may, musti with:
– ∀ u ∈ (in.m)∗ must(u) = ∅ ∧ may(u) = {in}
1
If must(u) contains more than one element, this means that any correct imple-
mentation must have after the trace u (at least) the choice between all actions in
must(u).
Refinement and composition with modalities Petri Nets & Concurrency – 389
Process Refinement and Asynchronous Composition with Modalities 5
– ∀ u ∈ in.(m.in)∗ must(u) = may(u) = {m}
Similarly, the modal language specification associated with the consumer is
h(m.out)∗ + m.(out.m)∗ , may, musti with:
– ∀ u ∈ (m.out)∗ must(u) = may(u) = m
– ∀ u ∈ m.(out.m)∗ must(u) = may(u) = out
Modal language specifications are related by a refinement relation that trans-
lates the degree of specialization. One can obtain a possible refinement by either
removing some allowed events or changing them to required events. So we review
the formal definition of modal language specification refinement.
Definition 2 (Modal language specification refinement).
Let S = hL, may, musti and S ′ = hL′ , may ′ , must′ i be two consistent modal
language specifications over the same alphabet Σ. S ′ is a modal language speci-
fication refinement of S, denoted by S ′ ⊑ S, if:
– L′ ⊆ L,
– for every u ∈ L′ , must(u) ⊆ must′ (u), i.e every required action after the
trace u in L is a required action after u in L′ .
3 Modal Petri Nets
In contrast to modal language specifications, Petri nets provide an appropriate
tool to specify the behavior of infinite state systems in a finitary way. Therefore
we are interested in the following to combine the advantages of Petri nets with the
flexibility provided by modalities for the definition of refinements. Of particular
interest are Petri nets which support silent transitions and hence are able to
characterize observable system behaviors. In the following we will consider such
Petri nets and extend them by modalities. Then we will use modal Petri nets as
a device to generate modal language specifications as the basis for refinement.
First, we review basic definitions of Petri net theory and we will introduce weakly
deterministic Petri nets.
3.1 Basics of Petri Nets
Definition 3 (Labeled Petri Net). A labeled Petri net over an alphabet Σ
is a tuple N = (P, T, W − , W + , λ, m0 ) where:
– P is a finite set of places,
– T is a finite set of transitions with P ∩ T = ∅,
– W − (resp. W + ) is a matrix indexed by P × T with values in N;
W − (resp. W + ) is called the backward (forward) incidence matrix,
– λ : T → Σ ∪ {ǫ} is a transition labeling function where ǫ denotes the empty
word, and
– m0 : P 7→ N is an initial marking.
390 Petri Nets & Concurrency Elhog-Benzina, Haddad, and Hennicker
6 Elhog-Benzina, Haddad and Hennicker
A marking is a mapping m : P 7→ N. The labeling function is extended
to sequences of transitions σ = t1 t2 ...tn ∈ T ∗ where λ(σ) = λ(t1 )λ(t2 )...λ(tn ).
For each t ∈ T , • t (t• resp.) denotes the set of input (output) places of t. i.e.
•
t = {p ∈ P | W − (p, t) > 0} (t• = {p ∈ P | W + (p, t) > 0} resp.). Likewise
for each p ∈ P , • p (p• ) denotes the set of input (output) transitions of p i.e.
•
p = {t ∈ T | W + (p, t) > 0} (p• = {t ∈ T | W − (p, t) > 0} resp.). The input
(output resp.) vector of a transition t is the column vector of matrix W − (W +
resp.) indexed by t.
In the sequel labeled Petri nets are simply called Petri nets. We have not
included final markings in the definition of a Petri net here, because we are in-
terested in potentially infinite system behaviors. We now introduce the semantic
of a net.
Definition 4 (Firing rule). Let N be a Petri net. A transition t ∈ T is firable
in a marking m, denoted by m[ti, iff ∀p ∈ • t, m(p) ≥ W − (p, t). The set of firable
transitions in a marking m is defined by f irable(m) = {t ∈ T | m[ti}. For a
marking m and t ∈ f irable(m), the firing of t from m leads to the marking m′ ,
denoted by m[tim′ , and defined by ∀p ∈ P, m′ (p) = m(p) − W − (p, t) + W + (p, t).
Definition 5 (Firing sequence). Let N be a Petri net with the initial marking
m0 . A finite sequence σ ∈ T ∗ is firable in a marking m and leads to a marking
m′ , also denoted by m[σim′ , iff either σ = ǫ or σ = σ1 .t with t ∈ T and there
exists m1 such that m[σ1 im1 and m1 [tim′ . For a marking m and σ ∈ T ∗ , we
write m[σi if σ is firable in m. The set of reachable markings is defined by
Reach(N , m0 )= {m | ∃σ ∈ T ∗ such that m0 [σim}.
The reachable markings of a Petri net correspond to the reachable states of
the modeled system. Since the capacity of places are not restricted, the set of the
reachable markings of the Petri nets considered here may be infinite. Thus, Petri
nets can model infinite state systems. Now, let us define the language generated
by a labeled Petri net.
Definition 6 (Petri net language). Let N be a labeled Petri net over the
alphabet Σ. The language generated by N is:
L(N ) = {u ∈ Σ ∗ | ∃σ ∈ T ∗ and m such that λ(σ) = u and m0 [σim} .
A particular interesting class of Petri nets are deterministic Petri nets as
defined, e.g., in [14]. Since in our approach we also deal with silent transitions,
which are not taken into account for the generated languages, we are interested
in a more general notion of determinacy which allows us to abstract from silent
transitions. This leads to our notion of weakly deterministic Petri net. We call a
Petri net weakly deterministic if any two firing sequences σ and σ ′ which produce
the same word u can be mutually extended to produce the same continuations
of u. In this sense our notion of weak deterministic Petri net corresponds to
Milner’s (weak) determinacy [13] and to the concept of a weakly deterministic
transition system in [5]. It is also related to to the notion of output-determinacy
in [7].
Refinement and composition with modalities Petri Nets & Concurrency – 391
Process Refinement and Asynchronous Composition with Modalities 7
Definition 7 (Weakly Deterministic Petri net). Let N be a labeled Petri
net with initial marking m0 and labeling function λ : T → Σ ∪ {ǫ}. For any
marking m, let
maymk (m) = {a ∈ Σ | ∃σ ∈ T ∗ such that λ(σ) = a and m[σi}
N is called weakly deterministic, if for each σ, σ ′ ∈ T ∗ with λ(σ) = λ(σ ′ ) and
for any markings m and m′ with m0 [σim and m0 [σ ′ im′ , we have maymk (m) =
maymk (m′ ).
Since weakly deterministic Petri nets play an important role in our further
development it is crucial to know, whether a given Petri net belongs to the class
of weakly deterministic Petri nets. This leads to our first decision problem stated
below. Our second decision problem is motivated by the major goal of this work
to provide formal support for refinement in system development. Since, in a
simple form, refinement can be defined by language inclusion, we want to be
able to decide this. Unfortunately, it is well-known that the language inclusion
problem for Petri nets is undecidable [4]. However, in [14] it has been shown
that for languages generated by deterministic Petri nets the language inclusion
problem is decidable. Therefore we are interested in a generalization of this
result for languages generated by weakly deterministic Petri nets which leads to
our second decision problem. Observe that we do not require N ′ to be weakly
deterministic.
First decision problem. Given a labeled Petri net N , decide
whether N is weakly deterministic.
Second decision problem. Let L(N ) and L(N ′ ) be two lan-
guages with the same alphabet Σ such that L(N ) is generated
by a weakly deterministic Petri net N and L(N ′ ) is generated
by a Petri net N ′ . Decide whether L(N ′ ) is included in L(N ).
3.2 Modal Petri Nets
In the following we introduce modal Petri nets which extend, similarly to modal
language specifications, Petri nets with modalities may and must on its transi-
tions.
Definition 8 (Modal Petri net). A modal Petri net M over an alphabet Σ
is a pair M = (N , T ) where N = (P, T, W − , W + , λ, m0 ) is a labeled Petri net
over Σ and T ⊆ T is a set of must (required) transitions. The set of may
(allowed) transitions is the set of transitions T .
Example 2. Let us consider the same example of a message producer and a
message consumer (see Fig. 2). The consumer may receive an input in (white
transition) but must produce a message m (black transition). The consumer
must receive a message m and produce an output out.
392 Petri Nets & Concurrency Elhog-Benzina, Haddad, and Hennicker
8 Elhog-Benzina, Haddad and Hennicker
• •
in m m out
(a) (b)
Fig. 2. Modal Petri nets for a producer (a) and a consumer (b)
Any modal Petri net M = (N , T ) gives rise to the construction of a modal
language specification (see Def. 1) which extends the language L(N ) by may
and must modalities. Similarly to the construction of L(N ) the definition of the
modalities should abstract from silent transitions in an appropriate way. While
for the may modality this is rather straightforward, special care has to be taken
for the definition of the must modality. For this purpose, we introduce the follow-
ing auxiliary definition which expresses, for each marking m, the set mustmk (m)
of all labels a ∈ Σ which must be produced by firing (in m) some silent must-
transitions succeeded by a must-transition labeled by a. This means that the
label a must be produced as the next visible label by some firing sequence of m.
Formally, for any marking m, let
mustmk (m) = {a ∈ Σ | ∃σ ∈ T∗ , t ∈ T such that λ(σ) = ǫ, λ(t) = a and m[σti}
On this basis we can now compute for each word u ∈ L(N ) and for each marking
m reachable by firing a sequence of transitions which produces u (and which
has no silent transition at the end2 ), the set mustmk (m). Then the labels in
mustmk (m) must be the possible continuations of u in the generated modal
language specification.
Definition 9 (Modal Petri Net Language Specification). Let M = (N , T )
be a modal Petri net over an alphabet Σ such that λ : T → Σ ∪ {ǫ} is the labeling
function and m0 is the initial marking of N . M generates the modal language
specification S(M) = hL(N ), may, musti where:
– L(N ) is the language generated by the Petri net N ,
– ∀u ∈ L(N ), may(u) =
{a ∈ Σ | ∃σ ∈ T ∗ and m such that λ(σ) = u, m0 [σim and a ∈ maymk (m)},
– ∀u ∈ L(N ), x ∈ Σ,
• must(ǫ) = mustmk (m0 ),
• must(ux) = {a ∈ Σ | ∃σ ∈ T ∗ , t ∈ T and m such that λ(σ) = u, λ(t) =
x, m0 [σtim and a ∈ mustmk (m)}.
2
We require it to avoid false detection of must transitions starting from intermediate
markings.
Refinement and composition with modalities Petri Nets & Concurrency – 393
Process Refinement and Asynchronous Composition with Modalities 9
Remark 1. Any modal language specification generated by a modal Petri net is
consistent.
Example 3. Let us consider the modal Petri net in Fig. 3.
ǫ ǫ
•
a b
Fig. 3. Modal Petri net with silent transitions
The modal language specification generated by this net consists of the lan-
guage L presented by the regular expression (a∗ b∗ )∗ and of the modalities may(u) =
{a, b}, and must(u) = {a} for u ∈ L. Note that b is not a must as it is preceeded
by a silent may-transition (which can be omitted in a refinement).
The notion of weakly deterministic Petri net can be extended to modal Petri
nets by taking into account an additional condition for must-transitions. This
condition ensures that for any two firing sequences σ and σ ′ which produce
the same word u, the continuations of u produced by firing sequences of must-
transitions after σ and σ ′ are the same.
Definition 10 (Weakly Deterministic Modal Petri Net). Let M = (N , T )
be a modal Petri net over an alphabet Σ such that λ : T → Σ ∪ {ǫ} is the labeling
function of N . For any marking m, let
mustmk (m) = {a ∈ Σ | ∃σ ∈ T∗ , t ∈ T such that λ(σ) = ǫ, λ(t) = a and m[σti}
M is (modally) weakly deterministic, if
1. N is weakly deterministic, and
2. for each σ, σ ′ ∈ T ∗ with λ(σ) = λ(σ ′ ) and for any markings m and m′ with
m0 [σim and m0 [σ ′ im′ , we have mustmk (m) = mustmk (m′ ).
Remark 2. For any weakly deterministic modal Petri net M = (N , T ) the def-
inition of the modalities of its generated modal language specification L(M) =
hL(N ), may, musti can be simplified as follows:
– ∀u ∈ L(N ), let σ ∈ T ∗ and let m be a marking such that λ(σ) = u and
m0 [σim, then may(u) = maymk (m).
394 Petri Nets & Concurrency Elhog-Benzina, Haddad, and Hennicker
10 Elhog-Benzina, Haddad and Hennicker
– ∀u ∈ L(N ), x ∈ Σ, let σ ∈ T ∗ , t ∈ T and let m be a marking such that
λ(σ) = u, λ(t) = x and m0 [σtim, then must(ux) = mustmk (m). Moreover,
must(ǫ) = mustmk (m0 ).
Example 4. Let us consider the modal Petri net in Fig. 4.
a a
•
b
ǫ ǫ
Fig. 4. Non weakly deterministic modal Petri net
Let tl (tr resp.) be the left (right resp.) transition labeled with a and let
ml (mr resp.) be the marking obtained by firing the transition tl (tr resp.).
Obviously, both transitions produce the same letter but must(ml ) = {b} while
must(mr ) = ∅ (since the silent transition firable in mr is only a may-transition).
The two decision problems of Sect. 3.1 induce the following obvious exten-
sions in the context of modal Petri nets and their generated modal language
specifications. Observe that for the refinement problem we require that both
nets are weakly deterministic.
Third decision problem. Given a modal Petri net M, decide
whether M is (modally) weakly deterministic.
Fourth decision problem. Let S(M) and S(M′ ) be two
modal language specifications over the same alphabet Σ such
that S(M) (S(M′ ) resp.) is generated by a weakly determinis-
tic modal Petri net M (M resp.). Decide whether S(M′ ) is a
modal language specification refinement of S(M).
4 Modal I/O-Petri Nets
In this section we consider modal Petri nets where the underlying alphabet Σ
is partitioned into disjoint sets in, out, and int of input, output and internal
labels resp., i.e Σ = in ⊎ out ⊎ int. Such alphabets are called I/O-alphabets and
modal Petri nets over an I/O-alphabet are called modal I/O-Petri nets. The
Refinement and composition with modalities Petri Nets & Concurrency – 395
Process Refinement and Asynchronous Composition with Modalities 11
discrimination of input, output and internal labels provides a means to specify
the communication abilities of a Petri net and hence provides an appropriate
basis for Petri net composition. A syntactic requirement for the composability
of two modal I/O-Petri nets is that their labels overlap only on complementary
types, i.e. their underlying alphabets must be composable. Formally, two I/O-
alphabets Σ1 = in1 ⊎ out1 ⊎ int1 and Σ2 = in2 ⊎ out2 ⊎ int2 are composable if
Σ1 ∩ Σ2 ⊆ (in1 ∩ out2 ) ∪ (in2 ∩ out1 ).3
Definition 11 (Alphabet Composition). Let Σ1 = in1 ⊎ out1 ⊎ int1 and
Σ2 = in2 ⊎ out2 ⊎ int2 be two composable I/O-alphabets. The composition of Σ1
and Σ2 is the I/O-alphabet Σc = inc ⊎ outc ⊎ intc where:
– inc = (in1 \ out2 ) ⊎ (in2 \ out1 ),
– outc = (out1 \ in2 ) ⊎ (out2 \ in1 ),
– intc = {∗a | ∗ ∈ {!, ?}, a ∈ Σ1 ∩ Σ2 } ⊎ int1 ⊎ int2 .
The input and output labels of the alphabet composition are the input and
output labels of the underlying alphabets which are not used for communica-
tion, and hence are “left open”. The internal labels of the alphabet composition
are obtained from the internal labels of the underlying alphabets and from their
shared input/output labels. Since we are interested here in asynchronous com-
munication each shared label a is duplicated to !a and ?a where the former
represents the asynchronous sending of a message and the latter represents the
receiption of the message (at some later point in time). We are now able to de-
fine the asynchronous composition of composable modal I/O-Petri nets. For the
realization of the asynchronous communication, for each shared label a a new
place pa is introduced in the composition.
Definition 12 (Asynchronous Composition). Let M1 = (N1 , T1 ), N1 =
(P1 , T1 , W1− , W1+ , λ1 , m10 ) be a modal I/O-Petri net over the I/O-alphabet Σ1 =
in1 ⊎ out1 ⊎ int1 and let M2 = (N2 , T2 ), N2 = (P2 , T2 , W2− , W2+ , λ2 , m20 ) be a
modal I/O-Petri net over the I/O-alphabet Σ2 = in2 ⊎ out2 ⊎ int2 . M1 and M2
are composable if P1 ∩ P2 = ∅, T1 ∩ T2 = ∅ and if Σ1 and Σ2 are composable.
In this case, their asynchronous composition Mc , also denoted by M1 ⊗as M2 ,
is the modal Petri net over the alphabet composition Σc , defined as follows:
– Pc = P1 ⊎ P2 ⊎ {pa | a ∈ Σ1 ∩ Σ2 } (each pa is a new place)
– Tc = T1 ⊎ T2 and Tc, = T1 ⊎ T2
– Wc− (resp. Wc+ ) is the Pc × Tc backward (forward) incidence matrix defined
by:
• for each p ∈ P1 ∪ P2 , t ∈ Tc ,
−
W1 (p, t) if p ∈ P1 and t ∈ T1
Wc (p, t) = W2− (p, t) if p ∈ P2 and t ∈ T2
−
0 otherwise
3
Note that for composable alphabets in1 ∩ in2 = ∅ and out1 ∩ out2 = ∅.
396 Petri Nets & Concurrency Elhog-Benzina, Haddad, and Hennicker
12 Elhog-Benzina, Haddad and Hennicker
+
W1 (p, t) if p ∈ P1 and t ∈ T1
Wc+ (p, t) = W2+ (p, t) if p ∈ P2 and t ∈ T2
0 otherwise
• for each pa ∈ Pc \ {P1 ∪ P2 } with a ∈ Σ1 ∩ Σ2 and for each t ∈ Ti with
i ∈ {1, 2},
1 if a = λi (t) ∈ ini ∩ outj with i 6= j
Wc− (pa , t) =
0 otherwise
1 if a = λi (t) ∈ inj ∩ outi with i 6= j
Wc+ (pa , t) =
0 otherwise
– λc : Tc → Σc is defined, for all t ∈ Tc and for i ∈ {1, 2}, by
λi (t) if t ∈ Ti , λi (t) ∈ / Σ1 ∩ Σ2
λc (t) = ?λi (t) if t ∈ Ti , λi (t) ∈ ini ∩ outj with i 6= j
!λi (t) if t ∈ Ti , λi (t) ∈ inj ∩ outi with i 6= j
– mc0 is defined, for each place p ∈ Pc , by
m10 (p) if p ∈ P1
mc0 (p) = m20 (p) if p ∈ P2
0 otherwise
Proposition 1. The asynchronous composition of two weakly deterministic modal
I/O-Petri nets is again a weakly deterministic modal I/O-Petri net.
We will not give a proof of this fact here, since it is not a main result of this
work.
Example 5. We consider the two modal producer and consumer Petri nets of
Fig. 2 as I/O-nets where the producer alphabet has the input label in, the
output label m and no internal labels while the consumer has the input label
m, the output label out and no internal labels as well. Obviously, both nets are
composable and their asynchronous composition yields the net shown in Fig. 5.
The alphabet of the composed net has the input label in, the output label
out and the internal labels ?m and !m. The Petri net composition describes
an infinite state system and its generated modal language specification has a
language which is no more regular.
When studying refinements it is crucial to rely on the observable behavior
specified by a requirements specification while one can abstract from internal
actions performed by a more concrete specification or an implementation. An
important case is the situation where the concrete specification is given by the
composition of (already available) specifications of single components. Then their
Refinement and composition with modalities Petri Nets & Concurrency – 397
Process Refinement and Asynchronous Composition with Modalities 13
• •
!m ?m
in out
(a) (b)
Fig. 5. Composition of the producer and consumer Petri nets
in out
Fig. 6. Requirements specification for an infinite state producer/consumer system
composition must exhibit the required observable behaviour of a given abstract
specification.
As an example we consider the requirements specification for an infinite state
producer/consumer system presented by the modal I/O-Petri net in Fig. 6. Ob-
viously, the asynchronous composition of the single producer and consumer nets
in Fig. 5 is not (yet) a correct refinement since there are still the internal labels
which do not correspond to silent transitions (yet) and therefore must be taken
into account when comparing the two generated modal language specifications.
However, since internal lables describe internal actions which are invisible from
the outside, we can apply an abstraction to the composition which relabels all
internal actions to the empty word ǫ. In the example the internal label are just
the labels !m and ?m used for the communication but, in general, transitions
with internal labels may also describe internal computation steps of an imple-
mentation and then its is also meaningful to abstract them away. Hence we define
a general abstraction operator which can be applied to any (modal) I/O-Petri
net.
Definition 13 (Abstraction). Let M = (N , T ) be a modal I/O-Petri net
over the I/O-alphabet Σ = in ⊎ out ⊎ int with underlying Petri net N =
(P, T, W − , W + , λ, m0 ). Let α(Σ) = in ⊎ out ⊎ ∅ and let α : Σ ∪ {ǫ} → α(Σ) ∪ {ǫ}
be the relabeling defined by α(a) = a if a ∈ in⊎out, α(a) = ǫ otherwise. Then the
abstraction from M is the modal I/O-Petri net α(M) = (α(N ), T ) over the
I/O-alphabet α(Σ) with underlying Petri net α(N ) = (P, T, W − , W + , α ◦ λ, m0 ).
398 Petri Nets & Concurrency Elhog-Benzina, Haddad, and Hennicker
14 Elhog-Benzina, Haddad and Hennicker
Coming back to our example the “abstract” Petri net in Fig. 6 is obviously
modally weakly deterministic. For the abstraction of the composed Petri nets in
Fig. 5 this is not obvious but, according to the results of the next section, we
can decide it (and get a positive answer). Note, however, that in the case where
one of the transitions used for the communication would not be a “must” the
abstraction of the Petri net composition would not satisy the second condition of
modal weak determinacy. The next problem is to decide whether the refinement
relation holds between their generated modal language specifications. Again,
according to the results of the next section, we can decide this (and also get a
positive answer).
5 Decision Algorithms
We begin this section by some recalls about semi-linear sets and decision proce-
dures in Petri nets.
Let E ⊆ Nk , E is a linear setP if there exists a finite set of vectors of Nk
{v0 , . . . , vn } such that E = {v0 + 1≤i≤n λi vi | ∀i λi ∈ N}. A semi-linear set
is a finite union of linear sets; a representation of it is given by the family of
finite sets of vectors defining the corresponding linear sets. Semi-linear sets are
effectively closed by union, intersection and complementation. This means that
one can compute a representation of the union, intersection and complementation
starting from a representation of the original semi-linear sets. E is an upward
closed set if ∀v ∈ E v ′ ≥ v ⇒ v ′ ∈ E. An upward closed set has a finite set of
minimal vectors denoted min(E). An upward closed set is a semi-linear set which
has a representation that can be derived from the equation E = min(E) + Nk if
min(E) is computable.
Given a Petri net N and a marking m, the reachability problem consists in
deciding whether m is reachable from m0 in N . This problem is decidable [12].
Furthermore this procedure can be adapted to semi-linear sets. Given a semi-
linear set E of markings, in order to decide whether there exists a marking of
′
P which is reachable, we proceed as follows. For any linear set E = {v0 +
E
1≤i≤n i i λ v | ∀i λ i ∈ N} associated with E we build a net N E by adding
′
transitions t1 , . . . , tn . Transition ti has vi as input vector and the null vector as
output vector. Then one checks whether v0 is reachable in NE ′ . E is reachable
from m0 iff one of these tests is positive.
In [18] given a Petri net, several procedures have been designed to compute
the minimal set of markings of several interesting upward closed sets. In par-
ticular, given a transition t, the set of markings m from which there exists a
transition sequence σ with m[σti is effectively computable.
Now we solve the decision problems stated in the previous sections.
Proposition 2. Let N be a labeled Petri net, then it is decidable whether N is
weakly deterministic.
Proof. First we build a net N ′ defined as follows.
Refinement and composition with modalities Petri Nets & Concurrency – 399
Process Refinement and Asynchronous Composition with Modalities 15
– Its set of places is the union of two disjoint copies P1 and P2 of P .
– There is one transition (t, t′ ) for every t and t′ s.t. λ(t) = λ(t′ ) 6= ε. The input
(resp. output) vector of this transition is the one of t with P substituted by
P1 plus the one of t′ with P substituted by P2 .
– There are two transitions t1 , t2 for every t s.t. λ(t) = ε. The input (resp.
output) vector of t1 (resp t2 ) is the one of t with P substituted by P1 (resp.
P2 ).
– The initial marking is m0 with P substituted by P1 plus m0 with P substi-
tuted by P2 .
Then for every a ∈ Σ, we compute a representation of the set Ea from which,
in N a transition labelled by a is eventually fireable after the firing of silent
transitions (using results of [18]) and a representation of its complementary set
Ea . Afterwards we compute the representation of the semi-linear set Fa whose
projection on P1 is a vector of Ea with P substituted by P1 andS whose projection
on P2 is a vector of Ea with P substituted by P2 . Let F = a∈Σ Fa then N is
weakly deterministic iff F is not reachable which is decidable.
Proposition 3. Let N be a weakly deterministic labeled Petri net and N ′ be a
labeled Petri net then it is decidable whether L(N ) ⊆ L′ (N ′ ).
Proof. W.l.o.g. we assume that P and P ′ are disjoint. First we build a net N ′′
defined as follows.
– Its set of places is the union of P and P ′ .
– There is one transition (t, t′ ) for every t ∈ T and t′ ∈ T ′ s.t. λ(t) = λ(t′ ) 6= ε.
The input (resp. output) vector of this transition is the one of t plus the one
of t′ .
– Every transition t ∈ T ∪ T ′ s.t. λ(t) = ε is a transtion of N ′′ .
– The initial marking is the m0 + m′0 .
Then for every a ∈ Σ, we compute a representation of the set EN ,a (resp.
EN ′ ,a ) from which in N a transition labelled by a is eventually fireable preceeded
only by silent transitions and a representation of its complementary set EN ,a
(resp. EN ′ ,a ). Afterwards we compute the representation of the semi-linear set Fa
whose projection onS P is a vector of EN ,a and whose projection on P ′ is a vector
of EN ′ ,a . Let F = a∈Σ Fa then L(N ) ⊆ L′ (N ′ ) iff F is not reachable. This
procedure is sound. Indeed assume that some marking (m, m′ ) ∈ Fa is reachable
in N ′′ witnessing that after some word w, some firing sequences σ ∈ N , σ ′ ∈ N ′
s.t. m0 [σim, m′0 [σ ′ im′ and λ(σ) = λ′ (σ ′ ) from m one cannot “observe” a and
from m′ one can “observe” a. Then due to weak determinism of N for every m∗
s.t. there exists a sequence σ ∗ with m0 [σ ∗ im∗ and λ(σ ∗ ) = λ(σ), m∗ is also in
EN ,a .
Proposition 4. Let M be a modal Petri net, then it is decidable whether M is
(modally) weakly deterministic.
400 Petri Nets & Concurrency Elhog-Benzina, Haddad, and Hennicker
16 Elhog-Benzina, Haddad and Hennicker
Proof. Observe that the first condition for being weakly deterministic is decid-
able by proposition 2. In order to decide the second condition, we build as in the
corresponding proof the net N ′ . Then we build representations for the following
semi-linear sets. Ga is the set of markings m of N such that from m a transi-
tion of T labelled by a is eventually fireable after firing silent transitions of T .
Afterwards we compute the representation of the semi-linear set Ha whose pro-
jection on P1 is a vector of Ga with P substituted by P1 andSwhose projection
on P2 is a vector of Ga with P substituted by P2 . Let H = a∈Σ Ha then M
fulfills the second condition of weak determinism iff H is not reachable.
Proposition 5. Let M, M′ be two weakly deterministic modal Petri nets then
it is decidable whether the modal specification S(M) refines S(M′ ).
Proof. Observe that the first condition for refinement is decidable by proposi-
tion 3. In order to decide the second condition, we build as in the corresponding
proof the net N ′′ . Then we build representations for the semi-linear sets Ga (as
in the previous proof) and similarly G′a in the case of N ′ . Afterwards we compute
the representation of the semi-linear set Ha whose projection onSP is a vector
of Ga and whose projection on P ′ is a vector of G′a . Let H = a∈Σ Ha then
the second condition for refinement holds iff H is not reachable. This procedure
is sound. Indeed assume that some marking (m, m′ ) ∈ Ha is reachable in N ′′
witnessing that after some word w, some firing sequences σ ∈ N , σ ′ ∈ N ′ s.t.
m0 [σim, m′0 [σ ′ im′ and λ(σ) = λ′ (σ ′ ) = w and from m one can “observe” b by a
“must” sequence and from m′ one cannot observe a by a must sequence. Then
due to (the second condition of) weak determinism of N ′ for every m∗ s.t. there
exists a sequence σ ∗ with m′0 [σ ∗ im∗ and λ′ (σ ∗ ) = λ′ (σ ′ ), m∗ is also in G′a .
6 Conclusion
In the present work, we have introduced modal I/O-Petri nets and we have
provided decision procedures to decide whether such Petri nets are weakly de-
terministic and whether two modal language specifications generated by weakly
deterministic modal Petri nets are related by the modal refinement relation. An
important role has been played by the notion of modal weak determinacy and by
the abstraction operator which considers internal transitions to be silent. Since,
in general, the abstraction operator does not preserve modal weak determinacy,
we are interested in the investigation of conditions which ensure this preser-
vation property. This concerns also conditions for single components such that
the abstraction of their composition is modally weakly deterministic. Another
direction of future research concerns the study of compatibility of component
behaviours represented by modal I/O-Petri nets and the establishment of an
interface theory for this framework along the lines of [3].
References
1. A. Antonik, M. Huth, K. G. Larsen, U. Nyman and A. Wasowski. Complexity of
decision problems for mixed and modal specifications. In Proc. of the 10th Int.
Refinement and composition with modalities Petri Nets & Concurrency – 401
Process Refinement and Asynchronous Composition with Modalities 17
Conf. on Found. of Software Science and Comp. Struct. (FoSSaCS’08), vol. 4962
of LNCS, Springer, 2008.
2. A. Antonik, M. Huth, K.G. Larsen, U. Nyman and A. Wasowski. EXPTIME-
complete decision problems for mixed and modal specifications. In: Proc. of EX-
PRESS, July 2008.
3. S. Bauer and P. Mayer and A. Schroeder and R. Hennicker. On Weak Modal
Compatibility, Refinement, and the MIO Workbench. In Proc. 16th Int. Conf.
Tools and Algor. for the Constr. and Analysis of Systems (TACAS’10), 2010
4. M.H.T. Hack. Decidability questions for Petri Nets. Ph.D.Thesis. M.I.T (1976)
5. R. Hennicker and S. Janisch and A. Knapp. On the Observable Behaviour of Com-
posite Components. In Electr. Notes Theor. Comput. Sci. Volume 260, 2010, pages
125-153. http://dx.doi.org/10.1016/j.entcs.2009.12.035, DBLP, http://dblp.uni-
trier.de
6. R.M. Karp, R.E. Miller Parallel program schemata. In: JTSS 4, 1969, pp 147-195.
7. V. Khomenko, M. Schaefer and W. Vogler. Output-Determinacy and Asynchronous
Circuit Synthesis. In: Fundam. Inf. 88, 4, pages 541-579 (Dec. 2008)
8. K.G. Larsen. Modal specifications. In: Joseph Sifakis, editor, Automatic Veri-
fication Methods for Finite State Systems, volume 407 of LNCS, pages 232–246,
1989.
9. K.G. Larsen, U. Nyman and A. Wasowski. On modal refinement and consistency. In
Proc. of the 18th International Conference on Concurrency Theory, (CONCUR07),
LNCS pages 105–119, Springer Verlag, 2007.
10. K.G. Larsen, U. Nyman and A. Wasowski. Modal I/O automata for interface and
product line theories. In Programming Languages and Systems, 16th European
Symposium on Programming (ESOP07), vol. 4421 of LNCS, pages 64–79. Springer,
2007.
11. K.G. Larsen and b. Thomsen. A modal process logic. In:Third Annual IEEE
Symposium on Logic in Computer Science LICS, pages 203–210, 1988.
12. E. Mayr. An algorithm for the general Petri net reachability problem. In Proc.
of the 13th Annual ACM Symposium on Theory of Computing (STOC’81) pages
238–246, 1981.
13. R. Milner Communication and concurrency. Prentice Hall, 1989.
14. E. Pelz. Closure properties of deterministic Petri net languages. In STACS’87, vol.
247 of LNCS, Springer 1987.
15. J.L. Peterson, Petri net theory and the modeling of systems, Prentice-Hall, Engle-
wood Cliffs, NJ, 1981
16. J.-B. Raclet. Residual for Component Specifications. In: Proc. of the 4th Inter-
national Workshop on Formal Aspects of Component Software (FACS07), Sophia-
Antipolis, France, September 2007.
17. J.-B. Raclet, E. Badouel, A. Benveniste, B. Caillaud, A. Legay and R. Passerone.
Modal Interfaces: Unifying Interface Automata and Modal Specifications. In Proc.
of 9th International Conference on Embedded Software (EMSOFT’09), Grenoble,
France, ACM, October 2009.
18. R. Valk, M. Jantzen The residue of vector sets with applications to decidability
problems in Petri nets Advances in Petri Nets 1984, LNCS volume 188 pp. 234-258