Finite-net multi-CCS is a CCS-like calculus which is able to model atomic sequences of actions and, together with parallel composition, also multi-party synchronization. This calculus is equipped with a labeled transition system semantics and also with an unsafe P/T Petri net semantics, which is sound w.r.t. the transition system semantics. For any process p of the calculus, the net associated to p by the semantics has always a finite number of places, but it has a finite number of transitions only for so-called well-formed processes. The main result of the paper is that well-formed finite-net multi-CCS processes are able to represent all finite, statically reduced, P/T Petri nets.
1 Introduction
Finite-state labeled transition systems (i.e., LTSs with finitely many states and transitions) can be expressed by the CCS [25] sub-calculus of finite-state processes, i.e., the sequential processes generated from the empty process \(\mathbf{0}\), prefixing \(\mu .p\), alternative composition \(p_1+p_2\) and a finite number of process constants C, each one equipped with a defining equation of the form \(C {{{\mathop {=}\limits ^{\mathrm{def}}}}}p\). More precisely, the semantics of any finite-state CCS process is a finite-state LTS and, conversely, given a reduced, finite-state LTS TS, it is possible to define a finite-state CCS process \(p_{\mathrm{TS}}\) such that the operational semantics for \(p_{\mathrm{TS}}\) generates an LTS isomorphic to TS. Hence, this famous result of Milner offers a process calculus to represent, up to isomorphism, all and only finite-state LTSs.
This paper addresses the same language representability problem for finite labeled Place/Transition Petri nets without capacity bounds on places. We single out a fragment (called finite-net processes) of an extension of CCS (called multi-CCS, fully described in [19]), such that not only all processes of this fragment generate finite P/T nets, but also for any finite (statically reduced) P/T net we can find a term of the calculus that generates it. This solves the open problem of providing a process calculus representing finite P/T Petri nets, and opens interesting possibilities of cross-fertilization between the areas of Petri nets and process calculi. In particular, it is now possible, on the one hand, (i) to define any (statically reduced) finite P/T net compositionally and (ii) to study algebraic laws for net-based behavioral equivalences (such as net isomorphism) over such a class of systems; on the other hand, it is now possible (iii) to reuse all the techniques and decidability results available for finite P/T nets [12] also for this fragment of multi-CCS, as well as (iv) to continue the study of non-interleaving semantics, typical of Petri nets (e.g., [11, 27, 29]), also for process algebras (initiated in [8, 28]), in particular for finite-net multi-CCS.
Anzeige
Finite-net multi-CCS includes the operator \(\underline{\alpha }.s\) of strong prefixing (in contrast to normal prefixing \(\mu .t\)), which states that the visible action \(\alpha \) is the initial part of an atomic sequence that continues with the sequential process s. So, by strong prefixing, a transition can be labeled with a sequence of visible actions. This operator, introduced in [16, 17] with a slightly different semantics, is also at the base of multi-party synchronization, obtained as an atomic sequence of binary CCS-like synchronizations. In finite-net multi-CCS, parallel composition may occur inside the body of a recursively defined constant C; on the contrary, the restriction operator \({(\mathbf{\nu } a)}\) is not allowed in the body of C. So, a finite-net process may be represented as \({(\mathbf{\nu } L)}t\), where L is a set of actions (if L is empty, the restriction operator is not present) and t a restriction-free process.
We equip our calculus with a net semantics that, differently from the approach by Degano et al. [8‐10, 28], uses unsafe P/T nets, as done in [13, 15] for a CCS sub-calculus without restriction, and in [5] for the \(\pi \)-calculus, where however inhibitor arcs are used to model restriction. The extension of the approach to restriction and strong prefixing is not trivial and passes through the introduction of an auxiliary set of restricted actions i.e., actions which are only allowed to synchronize. We prove that the net semantics associates a P/T net Net(p) to any finite-net multi-CCS process p, such that Net(p) has finitely many places; if p is well-formed, then Net(p) has also finitely many transitions; intuitively, process p is well-formed if the sequences that p may generate via strong prefixing have never the possibility to synchronize. We also provide a soundness result, i.e., p and Net(p) are bisimilar [25]. Finally, we also prove the representability theorem: for any finite, statically reduced, P/T net N, we can find a well-formed, finite-net multi-CCS process \(p_N\) such that Net\((p_N)\) and N are isomorphic.
The paper is organized as follows. Section 2 contains some basic background on LTSs and Petri nets. Section 3 introduces the process calculus called finite-net multi-CCS, its interleaving semantics in terms of LTSs, the well-formedness condition on its processes, and also the concurrent readers/writers example. Section 4 defines the operational net semantics for the calculus and presents the finiteness theorem (for any well-formed process p, Net(p) is finite) and some examples of net construction. Section 5 provides the soundness theorem (p and Net(p) are bisimilar). Section 6 proves the language expressibility theorem, i.e., the representability theorem mentioned above. Finally, some conclusions are drawn in Sect. 7, together with a comparison with related literature, in particular with the earlier version [18] of this paper. This paper is the full version of the extended abstract [14].
2 Background
2.1 Labeled transition systems and bisimulation
Definition 1
A labeled transition system (or LTS for short) is a triple \(TS = (Q, A,\)\( \rightarrow \)) where
Q is the countable set of states,
A is the countable set of labels,
\(\rightarrow \subseteq Q\times A\times Q\) is the transition relation.
In the following \(q{{{\,\mathop {\longrightarrow }\limits ^{a}}}}q'\) denotes \((q,a,q')\in \rightarrow \). A rooted LTS is a pair \((\mathrm{TS}, q_0)\) where \(\mathrm{TS} = (Q, A, \)\(\rightarrow )\) is a transition system and \(q_0\in Q\) is the initial state; a rooted LTS is usually represented as \(\mathrm{TS} = (Q, A, \rightarrow , q_0)\). A path from \(q_1\) to \(q_{n+1}\) is a sequence of transitions \(q_1{{{\,\mathop {\longrightarrow }\limits ^{a_1}}}} q_2 {{{\,\mathop {\longrightarrow }\limits ^{a_2}}}} \ldots q_n{{{\,\mathop {\longrightarrow }\limits ^{a_n}}}} q_{n+1}\). We say that \(q'\) is reachable from q if there exists a path from q to \(q'\). A rooted LTS \((Q, A, \rightarrow , q_0)\) is reduced if all the states in Q are reachable from the initial state \(q_0\).
Definition 2
Given two LTSs \(\mathrm{TS}_1 = (Q_1, A,\)\( \rightarrow _1)\) and \(\mathrm{TS}_2 = (Q_2, A,\)\( \rightarrow _2)\) a bisimulation between \(\mathrm{TS}_1\) and \(\mathrm{TS}_2\) is a relation \(R\subseteq (Q_1\times Q_2)\) such that if \((q_1, q_2) \in R\) then for all \(a \in A\)
\(\forall q'_1\) such that \(q_1{{{\,\mathop {\longrightarrow _1}\limits ^{a}\,}}}q_1'\), \(\exists \, q'_2\) such that \(q_2{{{\,\mathop {\longrightarrow _2}\limits ^{a}\,}}}q_2'\) and \((q_1', q_2') \in R\)
\(\forall q'_2\) such that \(q_2{{{\,\mathop {\longrightarrow _2}\limits ^{a}\,}}}q_2'\), \(\exists \, q'_1\) such that \(q_1{{{\,\mathop {\longrightarrow _1}\limits ^{a}\,}}}q_1'\) and \((q_1', q_2') \in R\).
If \(\mathrm{TS}_1 = \mathrm{TS}_2\) we say that R is a bisimulation on \(\mathrm{TS}_1\). Two states q and \(q'\) are bisimilar, \(q \sim q'\), if there exists a bisimulation R such that \((q, q') \in R\).
2.2 Finite place/transition Petri nets
We recall some basic notions on finite P/T Petri nets (see, e.g., [7, 30‐32] for an introduction). We use here a non-standard notation that better suits our needs.
Anzeige
Definition 3
(Multisets) Let \({\mathbb N}\) be the set of natural numbers. Given a set S, a finite multiset over S is a function \(m: S \rightarrow {\mathbb N}\) such that dom\((m) = \{ s \in S \, | \,m(s) \ne 0\}\) is finite. The set of all finite multisets over S, \({\mathcal M}_{\mathrm{fin}}(S)\), is ranged over by m. A multiset m such that dom\((m) = \emptyset \) is called empty and is denoted with \(\emptyset \), with abuse of notation. We write \(m \subseteq m'\) if \(m(s) \le m'(s)\) for all \(s \in S\). The operator \(\,\oplus \,\) denotes multiset union: \((m \,\oplus \, m')(s)\)\( = m(s) + m'(s)\). The operator \(\ominus \) denotes multiset difference: if \(m' \subseteq m\), then \((m \ominus m')(s)\)\( = m(s) - m'(s)\). The scalar product of a natural j with m is \((j \cdot m)(s) = j \cdot (m(s))\). A finite multiset m over a finite set \(S = \{s_1, \ldots , s_n\}\) can be represented also as \(k_1\cdot s_{1} \,\oplus \, k_2 \cdot s_{2} \,\oplus \, \cdots \,\oplus \, k_n \cdot s_{n}\), where \(k_j = m(s_{j}) \ge 0\) for \(j= 1, \ldots , n\).
Definition 4
(Finite P/T Petri nets) A labeled finite Place/Transition Petri net is a tuple \(N = (S, A, T)\), where
S is the finite set of places, ranged over by s (possibly indexed),
A is the finite set of labels, ranged over by a (possibly indexed), and
\(T \subseteq {(\mathcal M}_{\mathrm{fin}}(S){\setminus }\emptyset ) \times A \times {\mathcal M}_{\mathrm{fin}}(S)\) is the finite set of transitions, ranged over by t (possibly indexed), such that \(\forall a \in A \, \exists \, t \in T\) with \(l(t) = a\).
A finite multiset over the set S of places is called a marking. Given a marking m and a place s, we say that the place s contains m(s) tokens. Given a transition \(t = (m, a,m')\), we use the notation \({^{\bullet }t}\) to denote its pre-setm (which cannot be an empty marking), \({t^{\bullet }}\) for its post-set\(m'\) and l(t) for its label a. Hence, transition t can be also represented as \({^{\bullet }t} {{{\,\mathop {\longrightarrow }\limits ^{l(t)}}}} {t^{\bullet }}\). A P/T system is a tuple \(N(m_0) = (S, A, T, m_{0})\), where (S, A, T) is a P/T net and \(m_{0}\) is a finite multiset over S, called the initial marking.
Our definition of T as a set of triples ensures that the net is transition simple: for any \(t_1, t_2 \in T\), if \({^{\bullet }t}_1 = {^{\bullet }t}_2\) and \({t_1^{\bullet }} = {t_2^{\bullet }}\) and \(l(t_1) = l(t_2)\), then \(t_1 = t_2\). We are also assuming that a transition has a nonempty pre-set. These are the only constraints we impose over the definition of P/T net. The additional condition that A is covered by T (i.e., \(\forall a \in A \, \exists \, t \in T\) with label a) is just for economy.
Definition 5
(Net isomorphism) Two P/T nets \(N_1 = (S_1, A, T_1)\) and \(N_2 = (S_2, A, T_2)\) are isomorphic if there exists a bijection \(f: S_1 \rightarrow S_2\), homomorphically extended to markings, such that \((m, a, m') \in T_1\) iff \((f(m), a, f(m')) \in T_2\). Two systems \(N_1( m_{1})\) and \(N_2(m_{2})\) are isomorphic if \(N_1\) and \(N_2\) are isomorphic by f, which, additionally, preserves the initial markings: \(f(m_{1}) = m_{2}\).
Definition 6
Given a labeled P/T net \(N = (S, A, T)\), we say that a transition t is enabled at marking m, written as \(m[t\rangle \), if \({^{\bullet }t} \subseteq m\). The execution of t enabled at m produces the marking \(m' = (m \ominus {^{\bullet }t}) \,\oplus \, {t^{\bullet }}\), denoted by \(m[t\rangle m'\). The set of markings reachable from m, denoted by \([m\rangle \), is defined as the least set such that
\(m\in [m\rangle \) and
if \(m_1\in [m\rangle \) and, for some transition \(t\in T\), \(m_1[t\rangle m_2\), then \(m_2\in [m\rangle \).
Given a P/T system \(N(m_0) = (S, A, T, m_{0})\), we say that m is reachable if m is reachable from the initial marking \(m_{0}\). A P/T system \(N(m_0) = (S, A, T, m_{0})\) is said safe if for all \(m\in [m_{0}\rangle \) and for all \(s\in S\) we have that \(m(s)\le 1\).
Definition 7
Given a P/T system \(N(m_0) = (S, A, T, m_{0})\), the interleaving marking graph of \(N(m_0)\) is the rooted LTS \(\mathrm {IMG}(N(m_0))\)\( = ([m_{0}\rangle , A, \rightarrow , m_{0})\), where \(m_0\) is the initial state and the transition relation \(\rightarrow \subseteq {\mathcal M}_\mathrm{{fin}}(S)\times A\times {\mathcal M}_\mathrm{{fin}}(S)\) is defined by \(m{{{\,\mathop {\longrightarrow }\limits ^{a}}}}m'\) if and only if there exists a transition \(t\in T\) such that \(m[t\rangle m'\) and \(l(t) = a\). The P/T systems \(N_1(m_{1})\) and \(N_2(m_{2})\) are interleaving bisimilar—denoted by \(N_1(m_{1}) \sim N_2(m_{2})\) —if and only if there exists a bisimulation \(R \subseteq [m_{1}\rangle \times [m_{2}\rangle \) such that \((m_1, m_2) \in R\).
Definition 8
(Dynamically reduced) A P/T system \(N(m_0) = (S, A, T, m_{0})\) is dynamically reduced if
\(\forall s \in S \; \exists \, m \in [m_0\rangle \) such that \(m(s) \ge 1\), and
\(\forall t \in T \; \exists \, m, m' \in [m_0\rangle \) such that \(m[t\rangle m'\).
Definition 9
(Statically reduced) Given a finite P/T net \(N = (S, A, T)\), we say that a transition t is statically enabled by a set of places \(S' \subseteq S\), denoted by \(S' \llbracket t \rangle \), if dom\(({^{\bullet }t}) \subseteq S'\). Given two sets of places \(S_1, S_2 \subseteq S\), we say that \(S_2\) is statically reachable in one step from \(S_1\) if there exists \(t \in T\), such that \(S_1 \llbracket t \rangle \), dom\(({t^{\bullet }}) \not \subseteq S_1\) and \(S_2 = S_1 \cup \mathrm{dom}({t^{\bullet }})\); this is denoted by \(S_1 {{{\,\mathop {\Longrightarrow }\limits ^{t}\,}}} S_2\). The static reachability relation\({{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}} \subseteq {{\wp }}(S)_{\mathrm{fin}} \times {{\wp }}(S)_{\mathrm{fin}}\) is the least relation such that
\(S_1{{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}} S_1\) and
if \(S_1 {{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}} S_2\) and \(S_2 {{{\,\mathop {\Longrightarrow }\limits ^{t}\,}}} S_3\), then \(S_1 {{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}} S_3\).
A set of places \(S_k \subseteq S\) is the largest set statically reachable from \(S_1\) if \(S_1 {{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}} S_k\) and for all \(t \in T\) such that \(S_k \llbracket t \rangle \), we have that dom\(({t^{\bullet }}) \subseteq S_k\).
Given a finite P/T system \(N(m_0) = (S, A, T, m_{0})\), we denote by \(\llbracket \mathrm{dom}(m_0) \rangle \) the largest set of places statically reachable from dom\((m_0)\), i.e., the largest \(S_k\) such that dom\((m_0) {{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}} S_k\). A finite P/T net system \(N(m_0) = (S, A, T, m_{0})\) is statically reduced if all the places are statically reachable from the places in the initial marking, i.e., if \(\llbracket \mathrm{dom}(m_0) \rangle = S\).
Note that if \(N(m_0) = (S, A, T, m_{0})\) is statically reduced, then all the transitions in T are statically enabled by S. Note also that if \(N(m_0) = (S, A, T, m_{0})\) is dynamically reduced, then it is also statically reduced. However, there are statically reduced P/T systems that are not dynamically reduced. For instance, the statically reduced P/T system \(N(s_1) = (\{s_1, s_2, s_3\}, \{a, b\}, \{(s_1, a, s_2), (2 \cdot s_1,\)\( b, s_3)\}, s_1)\) cannot reach dynamically place \(s_3\).
3 Finite-net multi-CCS
Now we present finite-net multi-CCS: first its syntax, then the LTS operational semantics, followed by the definition of well-formedness; finally, an example.
3.1 Syntax
Let \({\mathcal L}\) be a denumerable set of names (inputs), ranged over by \(a,b,\ldots \). Let \(\overline{\mathcal L}\) be the set of co-names (outputs), ranged over by \(\overline{a}, \overline{b},\ldots \). The set \({\mathcal L}\cup \overline{\mathcal L}\), ranged over by \(\alpha , \beta , \ldots \), is the set of visible actions. With \(\overline{\alpha }\) we mean the complement of \(\alpha \), assuming that \(\overline{\overline{\alpha }} = \alpha \). Let \(\mathrm{Act} = {\mathcal L} \cup \overline{\mathcal L} \cup \{\tau \}\), such that \(\tau \not \in {\mathcal L}\cup \overline{\mathcal L}\), be the set of actions, ranged over by \(\mu \). Action \(\tau \) denotes an invisible, internal activity. Let \({\mathcal C}\) be a denumerable set of process constants, disjoint from Act, ranged over by \(A, B, C,\ldots \). The process terms are generated by the following abstract syntax
where we are using three syntactic categories: s, to range over sequential processes (i.e., processes that start sequentially), t, to range over restriction-free processes, and, finally p, to range over-restricted processes.
As for CCS [25], term \(\mathbf{0}\) is the terminated process, \(\mu .t\) is a normally prefixed process where action \(\mu \) is first performed and then t is ready. Note that \(s + s'\) is the sequential process obtained by the alternative composition of sequential processes s and \(s'\); hence we are restricting the use of \(+\) to so-called guarded sum. Term \(t {\,|\,}t'\) is the parallel composition of t and \(t'\). \({(\mathbf{\nu } a)}p\) is process p where the name a is made private by applying the restriction operator over a. Finally, C is a process constant, equipped with a defining equation \(C {{{\mathop {=}\limits ^{\mathrm{def}}}}}t\), i.e., the body of a constant must be a restriction-free process. The only new operator of the calculus is strong prefixing: \( \underline{\alpha }.s\) is a strongly prefixed process, where \(\alpha \) is the first action of a transaction that continues with the sequential process s (provided that s can complete the transaction).
We sometimes use the syntactic convention of writing \({(\mathbf{\nu } a)}({(\mathbf{\nu } b)}p))\) as \({(\mathbf{\nu } a,b)}p\). Generalizing this convention, a finite-net multi-CCS process may be represented as \({(\mathbf{\nu } L)}t\), where L is a set of actions (if L is empty, the restriction operator is not present) and t is a restriction-free process.
The set \({\mathcal P}\) of processes contains those terms which use finitely many constants only and are, w.r.t. the constants they use, closed (all possess a defining equation) and guarded (for any defining equation \(C {{{\mathop {=}\limits ^{\mathrm{def}}}}}t\), any occurrence of a constant in t is within a normally prefixed subprocess \(\mu .t'\) of t). \({\mathcal P}_{\mathrm{seq}}\) is the set of sequential processes, i.e., those of syntactic category s. Note that the restriction operator cannot occur syntactically in any term of \({\mathcal P}_{\mathrm{seq}}\). With abuse of notation, \({\mathcal P}\) will be ranged over by \(p, q, r, \ldots \) (hence p may denote any kind of process terms, also sequential ones), possibly indexed.
Definition 10
For any finite-net multi-CCS process p, the set of its sequential subterms sub(p) is defined by means of the auxiliary function (with the same name, with abuse of notation) sub\((p, \emptyset )\), whose second parameter is a set of already known constants, initially empty, described in Table 1.
Proposition 1
For any finite-net multi-CCS process p, the set of its sequential subterms sub(p) is finite.
\(\begin{array}{rclrclrcl} &{}&{}\mathrm{sub}(p_1 + p_2, I)= \{p_1 + p_2\} \cup \mathrm{sub}(p_1, I) \cup \mathrm{sub}(p_2, I)\\ &{}&{} \mathrm{sub}(p_1 {\,|\,}p_2, I) = \mathrm{sub}(p_1, I) \cup \mathrm{sub}(p_2, I) \\ &{}&{} \mathrm{sub}(A, I) = {\left\{ \begin{array}{ll} \emptyset &{} \! \! A \in I ,\\ \mathrm{sub}(p, I \cup \{A\}) &{} \! \! A \not \in I \wedge A {{{\mathop {=}\limits ^{\mathrm{def}}}}}p \\ \end{array}\right. } \end{array}\)
Proof
By induction on the definition of sub\((p, \emptyset )\). The base cases are sub\((\mathbf{0}, I)\) and sub(A, I) when \(A \in I\). Note that induction will end eventually because the constants that a finite-net multi-CCS process may use are finitely many. \(\square \)
Remark 1
Note that for any processes p and q, if the sequential process p is such that \(p \in \mathrm{sub}(q)\), then sub\((p) \subseteq \mathrm{sub}(q)\). This is because the definition of sub(q) recursively calls itself on all of its sequential subterms.
3.2 Operational semantics with LTSs
The operational semantics for finite-net multi-CCS is given by the labeled transition system \(({\mathcal P}, {\mathcal A}, {{{\,\mathop {\longrightarrow }\limits ^{ }}}})\), where the states are the processes in \({\mathcal P}\), \({\mathcal A} = \{\tau \} \cup (\mathcal {L} \cup \overline{\mathcal L})^+\) is the set of labels (ranged over by \(\sigma \) and composed of the invisible action \(\tau \) and by sequences of visible actions), and \({{{\,\mathop {\longrightarrow }\limits ^{ }}}} \subseteq {\mathcal P}\times {\mathcal A}\times {\mathcal P}\) is the minimal transition relation generated by the rules listed in Table 2.
We briefly comment on the rules that are less standard. Rule (S-pref) allows for the creation of transitions labeled by nonempty sequences of actions. In order for \(\underline{\alpha }.p\) to make a move, it is necessary that p be able to perform a transition, i.e., the rest of the transaction. Hence, if \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\) then \(\underline{\alpha }.p {{{\,\mathop {\longrightarrow }\limits ^{\alpha \diamond \sigma }}}} p'\), where the label \(\alpha \diamond \sigma = \alpha \) if \(\sigma = \tau \), \(\alpha \diamond \sigma = \alpha \sigma \) otherwise. Note that \(\underline{\alpha }.\mathbf{0}\) cannot execute any action, as \(\mathbf{0}\) is terminated. If a transition is labeled with \(\sigma = \alpha _1 \ldots \alpha _{n-1} \alpha _n\), then all the actions \(\alpha _1 \ldots \alpha _{n-1}\) are due to strong prefixes, while \(\alpha _n\) is due to a normal prefix (or \(\alpha _n\) is a strong prefix followed by a normal prefix \(\tau \)). Rule (S-Com) has a side-condition on the possible synchronizability of \(\sigma _1\) and \(\sigma _2\). Relation \(\mathrm {Sync}(\sigma _1, \sigma _2, \sigma )\), defined by the axioms of Table 3, holds if at least one of the two sequences is a single action, say \(\sigma _1 = \overline{\alpha }\), and the other starts with the complementary action \(\alpha \). Note that it is not possible to synchronize two sequences. This means that, usually, a multi-party synchronization can take place only among one leader, i.e., the process performing the atomic sequence, and as many other components (the servants), as is the length of the atomic sequence, where each servant executes one visible action. This is strictly the case for so-called well-formed processes, i.e., processes that do not allow for the synchronization of two sequences, not even indirectly. However, more elaborate forms of synchronization are possible, as illustrated in Sect. 3.3, for non-well-formed processes. Rule (S-Res) is slightly more general than the corresponding one for CCS, as it requires that no action in \(\sigma \) can be a or \(\overline{a}\). With \(n(\sigma )\) we denote the set of all actions occurring in \(\sigma \). Formally: \(n(\mu ) = \{\mu \}\), \(n(\alpha \sigma ) = \{\alpha \} \cup n(\sigma )\).
There is one further rule, called (Cong), which makes use of the structural congruence \(\equiv \), induced by the three axioms in Table 4. Axioms E1 and E2 are for associativity and commutativity, respectively, of the parallel operator. Axiom E3 is for unfolding and explains why we have no explicit operational rule for handling constants in Table 2: the transitions derivable from C are those transitions derivable from the structurally congruent term p if \(C {{{\mathop {=}\limits ^{\mathrm{def}}}}}p\). Rule (Cong) enlarges the set of transitions derivable from a given process p, as the following example shows. The intuition is that, given a process p, a transition is derivable from p if it is derivable from any \(p'\) obtained as a rearrangement in any order (or association) of all of its sequential subprocesses.
Axioms generating the structural congruence \(\equiv \)
\(\begin{array}{llrclllrrl} \mathbf{E1} &{}\; \; &{}\; \; (p {\,|\,}q) {\,|\,}r &{} = &{} p {\,|\,}(q {\,|\,}r) \\ \mathbf{E2} &{}\; \; &{}\; \; p {\,|\,}q &{} = &{} q {\,|\,}p &{} \\ \mathbf{E3} &{}\; \; &{}\; \; A &{} = &{} q &{} \quad \text{ if }\,\, A {{{\mathop {=}\limits ^{\mathrm{def}}}}}q\\ \end{array}\)
Table 5
Multi-party synchronization among three processes
×
Example 1
(Associativity and commutativity) Consider \((\underline{a}.b.p {\,|\,}\overline{a}.q) {\,|\,}\overline{b}.r\). The ternary synchronization among them, \((\underline{a}.b.p {\,|\,}\overline{a}.q) {\,|\,}\overline{b}.r {{{\,\mathop {\longrightarrow }\limits ^{\tau }}}} (p {\,|\,}q) {\,|\,}r\), can take place, as proved in Table 5, without using rule (Cong). However, if we consider the very similar process \(\underline{a}.b.p {\,|\,}(\overline{a}.q {\,|\,}\overline{b}.r)\), then we can see that \(\underline{a}.b.p\) is able to synchronize with both \(\overline{a}.q\) and \(\overline{b}.r\) only by using rule (Cong), as follows:
If we consider the slightly different variant process \((\underline{a}.b.p {\,|\,}\overline{b}.r) {\,|\,}\overline{a}.q \), we see easily that, without rule (Cong), no ternary synchronization is possible, because \(\mathrm {Sync}(ab, \overline{b}, a)\) does not hold. This example shows that, by using the axioms E1 and E2, it is possible to reorder the servant subcomponents (in this example, subprocesses \( \overline{a}.q\) and \( \overline{b}.r\)) in such a way that the actions they offer are in the expected order by the leader process (in this example, \(\underline{a}.b.p\)).
Two processes p and q are bisimilar, \(p \sim q\), if there exists a bisimulation \(R \subseteq \mathcal {P}\times \mathcal {P}\) such that \((p,q)\in R\). The following obvious result holds.
Proposition 2
If \(p \equiv q\) then \(p \sim q\).
3.3 Well-formed processes
We propose a syntactic condition on a process p, ensuring that, during its execution, p is unable to synchronize two atomic sequences, not even indirectly; a process satisfying such a syntactic condition will be called well-formed. The restriction to well-formed processes will be crucial in the following sections.
The definition of relation \(\mathrm {Sync}(\sigma _1, \sigma _2, \sigma )\) requires that at least one of \(\sigma _1\) or \(\sigma _2\) be a single action; this is not enough to prevent that two sequences may synchronize, even if indirectly. For instance, assume we have three processes \(p_1 = \underline{a}.b.\mathbf{0}\), \(p_2 = \overline{a}.\mathbf{0}\) and \(p_3 = \underline{\overline{b}}.c.\mathbf{0}\), which may perform the sequences \(ab, \overline{a}, \overline{b}c\), respectively; then a ternary synchronization is possible, because first we synchronize \(p_1\) and \(p_2\), by \(\mathrm {Sync}(ab, \overline{a}, b)\), getting a single action b, which can be then used for a synchronization with \(p_3\), by \(\mathrm {Sync}(b, \overline{b}c, c)\); in such a way, the two atomic sequences ab and \(\overline{b}c\) have been synchronized, by means of the single action \(\overline{a}\). So, we would like to mark \((p_1 {\,|\,}p_2) {\,|\,}p_3\) as not well-formed. In order to define well-formed multi-CCS processes, some auxiliary definitions are needed.
Definition 11
(Initials for sequential processes) For any sequential process p, \(In(p) \subseteq \mathcal {A}\) is the set of initials of p, defined inductively as
(Names in sequences of a process) Let ns\((p) \subseteq \mathcal {L} \cup \overline{\mathcal {L}}\) be the set of (free) names occurring in sequences of length two or more of p. Set ns(p) is defined by means of the auxiliary function (with the same name, with abuse of notation) ns\((p, \emptyset )\), whose second parameter is a set of constants, where ns(p, I) is defined in Table 6.
A process p is well-formed if \({{\mathrm{wf}}(p)}\) holds, and \({{\mathrm{wf}}(p)}\) holds if the auxiliary relation (with the same name, with abuse of notation) \({{\mathrm{wf}}(p, \emptyset )}\) holds; the auxiliary relation \({{\mathrm{wf}}(p, I)}\), where the second parameter is a set of constants, is defined as the least relation induced by the axioms and rules of Table 7. The assumption that any process uses finitely many constants ensures that the well-formedness predicate is well-defined.
Let us consider processes \(p_1 = \underline{a}.b.\mathbf{0}\), \(p_2 = \overline{a}.\mathbf{0}\) and \(p_3 = \underline{\overline{b}}.c.\mathbf{0}\). Note that \({{\mathrm{wf}}(p_2)}\), because \({{\mathrm{wf}}(\mathbf{0})}\) holds; similarly, \({{\mathrm{wf}}(b.\mathbf{0})}\); as a consequence, \({{\mathrm{wf}}(p_1)}\) holds, because ns\((p_1) = \{a, b\}\) does not contain a pair of complementary actions. In the same way, we can prove that \({{\mathrm{wf}}(p_3)}\) holds, with ns\((p_3) = \{\overline{b}, c\}\). We also have that \({{\mathrm{wf}}(p_1{\,|\,}p_2)}\), as no action of ns\((p_1)\) occurs complemented in ns\((p_2) = \emptyset \). However, it is not the case that \({{\mathrm{wf}}((p_1 {\,|\,}p_2) {\,|\,}p_3)}\), because there exists an action, namely b, such that \(b \in \mathrm{ns}(p_1 {\,|\,}p_2)\) and \(\overline{b} \in \mathrm{ns}(p_3)\).
To conclude this section, we comment on the well-formedness relation: if a process is well-formed, then it is not possible to synchronize two sequences, not even indirectly. Theorem 2 will prove this fact on the net semantics. A direct proof on the LTS semantics is reported in [19].
3.4 An example: concurrent readers and writers
In this problem, originally introduced in [6], there are two types of processes: reader processes and writer processes. All processes share a common file; so, each writer process must exclude all the other writers and all the readers while writing on the file, while multiple reader processes can access the shared file simultaneously. The problem is to define a control structure that does not deadlock or allow violations of the mutual exclusion criteria.
Assume we have n readers and m writers and that at most \(k \le n\) readers can read simultaneously. We can assume we have k lock resources such that a reader can read if at least one lock is available, while a writer can write if all the k locks are available, so that it prevents all the k possible concurrent reading operations. In a naïve CCS solution to this problem, a deadlock may occur when two writers are competing for the acquisition of the k locks, so that one has acquired i locks and the other one \(k - i\), for some \(0 < i < k\); in such a situation, both writers are stuck, waiting for the missing locks, and all the readers are not allowed to read as no lock is available. A simple multi-ccS solution to this coordination problem is forcing atomicity on the writer’s acquisition of the k locks, so that either all or none are taken. To make the presentation simple, assume that \(n = 4, k=3, m=2\). Each reader process R, each lock process L, each writer W can be represented as follows, where action l stands for lock and u for unlock:
$$\begin{aligned} \begin{array}{lcllcllcl} R &{} {{{\mathop {=}\limits ^{\mathrm{def}}}}}&{} l.\mathrm{read}.u.R &{} \; \; L &{} {{{\mathop {=}\limits ^{\mathrm{def}}}}}&{} \overline{l}.\overline{u}.L &{} \; \; W &{} {{{\mathop {=}\limits ^{\mathrm{def}}}}}&{} \underline{l}.\underline{l}.l.\mathrm{write}.\underline{u}.\underline{u}.u.W \\ \end{array} \end{aligned}$$
where parentheses are omitted as \({\,|\,}\) is associative. Note that a writer W executes a four-way synchronization with the three instances of the lock process L in order to get permission to write:
where \(W' = \mathrm{write}.\underline{u}.\underline{u}.u.W\) and \(L' = \overline{u}.L\). The LTS for CRW is finite-state. Note that, to ensure correctness, it is not necessary to require atomicity on the release of the locks: This choice is only done in order to have a smaller model.
4 Operational net semantics
4.1 Places and markings
The finite-net multi-CCS processes are built upon the set \({\mathcal L}\cup \overline{\mathcal L}\), ranged over by \(\alpha \), of visible actions. We assume we have also sets \({\mathcal L}' = \{a' \, | \, a\in \mathcal {L}\}\) and \(\overline{{\mathcal L}'} =\)\( \{\overline{a'} \, | \, \)\(\overline{a}\in \overline{\mathcal {L}}\}\), where \({\mathcal L}' \cup \overline{\mathcal L'}\), ranged over by \(\alpha '\), is the set of auxiliary restricted actions; by definition, each restricted action \(\alpha '\) corresponds exactly to one visible action \(\alpha \). Set \(\mathcal {G} =\)\( {\mathcal L}\cup \overline{\mathcal L} \)\(\cup {\mathcal L}' \cup \overline{{\mathcal L}'}\) is ranged over by \(\gamma \). The set of all actions Act\(_{\gamma } = {\mathcal G} \cup \{\tau \}\), ranged over by \(\mu \) (with abuse of notation), is used to build the set of extended, finite-net multi-CCS processes \({\mathcal P}^{\gamma }\). The infinite set of places, ranged over by s, is \(S_{\mathrm{MCCS}} = {\mathcal P}^{\gamma }_{\mathrm{seq}} {\setminus }\{\mathbf{0}\}\), i.e., the set of all sequential processes (except \(\mathbf{0}\)) whose prefixes are in Act\(_{\gamma }\) and whose strong prefixes are in \({\mathcal G}\).
Function \({\mathrm{dec}}: {\mathcal P}^{\gamma } \times {{\wp }}({\mathcal {C}}) \rightarrow {\mathcal M}_{\mathrm{fin}}(S_{\mathrm{MCCS}})\) defines the decomposition of extended processes into markings (see Table 8), where the second argument is the set of already known constants, initially empty. For simplicity sake, we often omit the second argument when it is empty or inessential. Process \(\mathbf{0}\) generates no places. The decomposition of a sequential process p produces one place with name p. This is the case of \(\mu .p\) (where \(\mu \) can be any action in Act\(_{\gamma }\)), \(\underline{\gamma }.p\) and \(p + p'\). Parallel composition is interpreted as multiset union; e.g., the decomposition of \(a.\mathbf{0}{\,|\,}a.\mathbf{0}\) produces the marking \(a.\mathbf{0}\, \,\oplus \,\, a.\mathbf{0}= 2 \cdot a.\mathbf{0}\). The decomposition of a restricted process \({(\mathbf{\nu } a)}p\)—where \(a \in \mathcal {L}\)—generates the multiset obtained from the decomposition of p, to which the substitution \({\{a'/a\}}\) is applied; the application of the substitution \({\{a'/a\}}\) to a multiset is performed elementwise, as shown in the example below. Finally, a process constant A is first unwound once (according to its defining equation) and then decomposed, if A is not known yet.
We assume that, in decomposing \({(\mathbf{\nu } a)}p\), the choice of the restricted name is fixed by the rule that associates to a visible action a its unique corresponding restricted action \(a'\). As a process is of the form \({(\mathbf{\nu } L)}t\) with \(L = \{a_1, a_2, \ldots , a_n\}\), it can be first translated to the restriction-free process \(t{\{a_1'/a_1\}}\ldots {\{a_n'/a_n\}}\) (shortened as \(t{\{L'/L\}}\), for \(L' = \{a_1', \ldots , a'_n\} \subseteq \mathcal {L}'\)), and then decomposed to obtain a multiset. Function \({\mathrm{dec}}\) essentially performs this decomposition, by removing the restriction (which can occur only externally, by syntactic definition) and by replacing the bound names in L with the corresponding restricted names in \(L'\).
Proposition 3
For any restriction-free \(t \in {\mathcal P}\), \({\mathrm{dec}}({(\mathbf{\nu } L)}t) = {\mathrm{dec}}(t{\{L'/L\}})\).
This means that we can restrict our attention to restriction-free processes built over Act\(_{\gamma }\), as a restricted process \({(\mathbf{\nu } L)}t\) in \(\mathcal {P}\) is mapped via \({\mathrm{dec}}\) to the same marking of the restriction-free process \(t{\{L'/L\}}\) in \(\mathcal {P}^\gamma \).
Example 3
Consider the (non-well-formed) finite-net multi-CCS process \(p = {(\mathbf{\nu } a)}p'\), where \(p' = (a.\mathbf{0}{\,|\,}(\underline{\overline{a}}.a.\mathbf{0}{\,|\,}\overline{a}.\mathbf{0}))\). Then,
where \(a'\) is the corresponding restricted name in \({\mathcal L}'\).
Function \({\mathrm{dec}}\) is well-defined because the constants a process may use are finitely many. This also ensures the following fact.
Proposition 4
For any \(p \in {\mathcal P}^{\gamma }\), \({\mathrm{dec}}(p)\) is a finite multiset of places.
Of course, function \({\mathrm{dec}}\) is not injective, because it considers the parallel operator as commutative, associative, with \(\mathbf{0}\) as neutral element. In fact, \({\mathrm{dec}}((p {\,|\,}q) {\,|\,}r)\)\( = {\mathrm{dec}}(p {\,|\,}(q {\,|\,}r))\), \({\mathrm{dec}}(p {\,|\,}q) = {\mathrm{dec}}(q {\,|\,}p)\), \({\mathrm{dec}}(p {\,|\,}\mathbf{0}) = {\mathrm{dec}}(p)\), etc. However, contrary to the decomposition functions in [8, 28], one can prove that our \({\mathrm{dec}}\) is surjective. Take any finite multiset of places \(m = k_1 \cdot s_1 \,\oplus \, \cdots \,\oplus \, k_n \cdot s_n\), for \(n \ge 0\) (\(m = \emptyset \) if \(n = 0\)), where each \(s_i \in S_{\mathrm{MCCS}}\), for \(i = 1, \ldots , n\). Then, process \(p =\)\(s_1^{k_1} {\,|\,}\cdots {\,|\,}s_n^{k_n}\), where \(s^1 = s\) and \(s^{n+1} = s {\,|\,}s^n\), is such that \({\mathrm{dec}}(p) = m\). We can be even more demanding and prove that function \({\mathrm{dec}}\) is surjective even if we restrict ourselves to processes in \(\mathcal {P}\).
Proposition 5
Function \({\mathrm{dec}}: {\mathcal P}\rightarrow {\mathcal M}_{\mathrm{fin}}(S_{\mathrm{MCCS}})\) is surjective.
Proof
Take any finite multiset of places \(m = k_1\cdot s_1 \,\oplus \, \cdots \,\oplus \, k_n \cdot s_n\), for \(n \ge 0\) (\(m = \emptyset \) if \(n = 0\)), where each \(s_i \in S_{\mathrm{MCCS}}\), for \(i = 1, \ldots , n\). It is possible to find a substitution \(\rho = {\{a_1, \ldots , a_k/a'_1, \ldots , a'_k\}}\) (with \(a'_i \in {\mathcal L}'\) and \(a_i \in {\mathcal L}\)) such that, for all \(i = 1, \ldots , n\), \(p_i = s_i\rho \) and \(p_i \in {\mathcal P}_{\mathrm{seq}}\). Take process \(p =\)\( {(\mathbf{\nu } a_1 a_2 \ldots a_k)}(p_1^{k_1} {\,|\,}\cdots {\,|\,}p_n^{k_n})\), assuming that no restriction is present if \(k = 0\) and that, if \(n = 0\), \((p_1^{k_1} {\,|\,}\cdots {\,|\,}p_n^{k_n}) = \mathbf{0}\). It is easy to observe that \({\mathrm{dec}}(p) = m\). \(\square \)
4.2 Properties of places and markings
We now list some useful properties of places and markings. First, we extend the definition of sequential subterm of a process p to a set of places S. The goal is to prove that the sequential subterms of dom\(({\mathrm{dec}}(p))\) are essentially the same sequential subterms of p. This property will be useful in proving (Theorem 3) that each place statically reachable from \(\mathrm{dom}({\mathrm{dec}}(p))\) is a sequential subterm of p (up to a possible renaming of bound names to the corresponding restricted names), so that, since sub(p) is finite for any p (Proposition 1), the set of all the places statically reachable from \(\mathrm{dom}({\mathrm{dec}}(p))\) is finite as well.
Definition 13
Function sub\((-)\), defined over finite-net multi-CCS processes in Definition 10, can be extended to a finite set S of places (i.e., of sequential processes) as follows: sub\((\emptyset ) = \emptyset \) and sub\((S) = \bigcup _{s \in S} \mathrm{sub}(s)\).
Proposition 6
For any finite set of places \(S_1\) and \(S_2\), if \(S_1 \subseteq \mathrm{sub}(S_2)\), then sub\((S_1) \subseteq \mathrm{sub}(S_2)\).
Proof
By induction on the cardinality of \(S_1\), using Remark 1. \(\square \)
Proposition 7
For any set of places S, \(S \subseteq \mathrm{sub}(S)\).
Proof
For any sequential process s, Definition 10 ensures that \(s \in \mathrm{sub}(s)\); hence, the thesis follows trivially. \(\square \)
Proposition 8
If p is restriction-free, then sub(dom\(({\mathrm{dec}}(p))\)\(\subseteq \mathrm{sub}(p)\) , while if \(p = {(\mathbf{\nu } L)}t\), then sub(dom\(({\mathrm{dec}}(p))) \subseteq \mathrm{sub}(p){\{L'/L\}}\). Hence, for any p, \(|\mathrm{sub}(p)| \ge \)\( |\mathrm{sub(dom}({\mathrm{dec}}(p))|\).
Proof
By induction on the definitions of sub(p, I) and \({\mathrm{dec}}(p, I)\).
The first base case is when \(p = \mathbf{0}\); in such a case sub\((\mathbf{0}, I) = \{\mathbf{0}\}\); as \({\mathrm{dec}}(\mathbf{0}, I) \)\(= \emptyset \), the thesis follows trivially. The second base case is when \(p = A\) and \(A \in I\); in such a case, sub\((A, I) = \emptyset \); as \({\mathrm{dec}}(A, I) = \emptyset \), the thesis follows trivially. The other simple case is when p is sequential (and not \(\mathbf{0}\)); in such a case, \({\mathrm{dec}}(p, I) = \{p\}\) and the thesis follows trivially.
Now the inductive cases. If \(p = p_1 {\,|\,}p_2\), then sub\((p, I) = \mathrm{sub}(p_1, I) \cup \mathrm{sub}(p_2, I)\) and \(\mathrm{sub(dom}({\mathrm{dec}}(p, I))) = \mathrm{sub(dom}({\mathrm{dec}}(p_1, I)) \cup \mathrm{sub(dom(dec}(p_2, I))\); by induction, we have that \(\mathrm{sub(dom}(\mathrm{dec}(p_i, I)) \subseteq \mathrm{sub}(p_i, I)\), for \(i = 1, 2\); hence, the thesis follows trivially. If \(p = A\), with \(A \not \in I\) and \(A {{{\mathop {=}\limits ^{\mathrm{def}}}}}t\), then \(\mathrm{sub}(A, I) = \mathrm{sub}(t, I \cup \{A\})\) and \({\mathrm{dec}}(A, I) = {\mathrm{dec}}(t, I \cup \{A\})\); by induction, we have \(\mathrm{sub(dom}({\mathrm{dec}}(t, I \cup \{A\})) \subseteq \mathrm{sub}(t, I \cup \{A\}))\), and so \(\mathrm{sub(dom}(\mathrm{dec}(A, I)) \subseteq \mathrm{sub}(A, I)\), as required. Finally, if \(p = {(\mathbf{\nu } L)}t\), then sub\((p, I) = \mathrm{sub}(t, I)\), while \(\mathrm{sub(dom}({\mathrm{dec}}({(\mathbf{\nu } L)}t, I))) = \mathrm{sub(dom}({\mathrm{dec}}(t, I){\{L'/L\}})) = \mathrm{sub(dom}({\mathrm{dec}}(t, I))){\{L'/L\}}\); by induction, we have that \(\mathrm{sub(dom}({\mathrm{dec}}(t, I)) \subseteq \mathrm{sub}(t, I)\), and therefore also \(\mathrm{sub(dom}({\mathrm{dec}}(t, I))){\{L'/L\}}\)\(\subseteq \mathrm{sub}(t, I){\{L'/L\}}\), from which the thesis follows. \(\square \)
Now we want to extend the definition of well-formed processes to sets of places. To this aim, we define a notion of well-behaved set of places, which will be useful in the next section in proving that any transition statically enabled by a well-behaved set S is such that no synchronization of sequences is possible (Theorem 2); first, we prove that a well-formed process p generates a marking \({\mathrm{dec}}(p)\) such that dom\(({\mathrm{dec}}(p))\) is well-behaved (Theorem 1).
Definition 14
Function ns\((-)\) of Definition 12 is defined over a set S of places as ns\((S) = \mathrm{ns}(S, \emptyset )\), where ns\((S, I) = \bigcup _{s\in S} \mathrm{ns}(s, I)\) and ns\((\emptyset , I) = \emptyset \).
Lemma 1
If p is restriction-free, then \(\mathrm{ns}(p, I) = \mathrm{ns(dom}({\mathrm{dec}}(p, I)), I)\).
Proof
By induction on the definitions of ns(p, I) and \({\mathrm{dec}}(p, I)\). The proof is very similar to that of Proposition 8, hence omitted. \(\square \)
Definition 15
(Well-behaved) A set of places S is well-behaved if there exist no \(\beta \in \mathcal {G}\) such that \(\beta \in \mathrm{ns}(S)\) and \(\overline{\beta } \in \mathrm{ns}(S)\).
Theorem 1
If p is well-formed, then dom\(({\mathrm{dec}}(p))\) is well-behaved.
Proof
By induction on the proof of \({{\mathrm{wf}}(p, I)}\). The first base case is \(p = \mathbf{0}\), and the thesis trivially holds. The second base case is when \(p = A\) and \(A \in I\); in such a case, \({{\mathrm{wf}}(A, I)}\) holds and dom\(({\mathrm{dec}}(A, I)) = \emptyset \), hence the thesis trivially holds.
Now the inductive cases. If \(p = \mu .p'\), then \({{\mathrm{wf}}(p, I)}\) holds only if \({{\mathrm{wf}}(p', I)}\) holds. By induction, we have that dom\(({\mathrm{dec}}(p', I))\) is well-behaved. Hence, also dom\(({\mathrm{dec}}(\mu .p', I))\) is well-behaved, as ns(dom\(({\mathrm{dec}}(\mu .p', I)), I)\)\( = \mathrm{ns}(\{\mu .p'\}, I) = \mathrm{ns}(\mu .p', I) = \mathrm{ns}(p', I)\) and \(\mathrm{ns}(p', I) = \mathrm{ns(dom}({\mathrm{dec}}(p', I)), I)\) by Lemma 1.
If \(p = \underline{\alpha }.p'\), then \({{\mathrm{wf}}(p, I)}\) holds if there exists no \(\beta \in \mathcal {G}\) such that \(\beta \in \mathrm{ns}(p, I)\) and \(\overline{\beta } \in \mathrm{ns}(p, I)\); by Lemma 1, \(\mathrm{ns}(p, I) = \mathrm{ns(dom}({\mathrm{dec}}(p, I)), I)\), and so the thesis follows trivially.
If \(p = p_1 + p_2\), then \({{\mathrm{wf}}(p, I)}\) holds only if \({{\mathrm{wf}}(p_1, I)}\) and \({{\mathrm{wf}}(p_2, I)}\) hold and, additionally, there exists no \(\beta \in \mathcal {G}\) such that \(\beta \in \mathrm{ns}(p_1, I)\) and \(\overline{\beta } \in \mathrm{ns}(p_2, I)\). By induction, we have that \(\mathrm{dom}({\mathrm{dec}}(p_i, I))\) is well-behaved, for \(i = 1, 2\); so, there exists no \(\beta \in \mathcal {G}\) such that \(\beta \in \mathrm{dom}({\mathrm{dec}}(p_i, I))\) and \(\overline{\beta } \in \mathrm{dom}({\mathrm{dec}}(p_i, I))\), for \(i = 1, 2\). By Lemma 1, ns\((\mathrm{dom}({\mathrm{dec}}(p_i, I)), I) = \mathrm{ns}(p_i, I)\) for \(i = 1, 2\), and so there exists no \(\beta \in \mathcal {G}\) such that \(\beta \in \mathrm{ns}(p_i, I)\) and \(\overline{\beta } \in \mathrm{ns}(p_i, I)\), for \(i = 1, 2\). Therefore, \(\mathrm{dom}({\mathrm{dec}}(p_1 + p_2, I)) = \{p_1 + p_2\}\) is well-behaved, too, because ns\((p_1 + p_2, I) = \mathrm{ns}(p_1, I) \cup \mathrm{ns}(p_2, I)\), and then there exists no \(\beta \in \mathcal {G}\) such that \(\beta \in \mathrm{ns}(p_1 + p_2, I)\) and \(\overline{\beta } \in \mathrm{ns}(p_1 + p_2, I)\), as required. The case when \(p = p_1 {\,|\,}p_2\) is similar to the above, hence omitted.
If \(p = {(\mathbf{\nu } a)}p'\), then \({{\mathrm{wf}}(p, I)}\) holds only if \({{\mathrm{wf}}(p', I)}\) holds. By induction, we have that \(\mathrm{dom}(\mathrm{dec}(p', I))\) is well-behaved. It is easy to see that \(\mathrm{dom}(\mathrm{dec}(p', I)){\{a'/a\}}\) is well-behaved too, as the substitution replaces action a with a new name \(a'\) not in use. Hence, as \(\mathrm{dom}(\mathrm{dec}(p', I)){\{a'/a\}} = \mathrm{dom}(\mathrm{dec}(p', I){\{a'/a\}}) = \mathrm{dom}({\mathrm{dec}}(p, I))\), also \(\mathrm{dom}(\mathrm{dec}(p, I))\) is well-behaved.
If \(p = A\), with \(A \not \in I\) and \(A {{{\mathop {=}\limits ^{\mathrm{def}}}}}q\), then \({{\mathrm{wf}}(A, I)}\) holds only if \({{\mathrm{wf}}(q, I \cup \{A\})}\) holds. By induction, \(\mathrm{dom}(\mathrm{dec}(q, I \cup \{A\}))\) is well-behaved. Since \({\mathrm{dec}}(A, I) = {\mathrm{dec}}(q, I \cup \{A\})\), also \(\mathrm{dom}(\mathrm{dec}(A, I))\) is well-behaved. \(\square \)
4.3 Net transitions
Let \({\mathcal A}^{\gamma } = \{\tau \} \cup \mathcal {G}^{+}\), ranged over by \(\sigma \) with abuse of notation, be the set of labels, and let \(\rightarrow \subseteq {\mathcal M}_{\mathrm{fin}}(S_{\mathrm{MCCS}}) \times {\mathcal A}^{\gamma } \times {\mathcal M}_{\mathrm{fin}}(S_{\mathrm{MCCS}})\), be the least set of transitions generated by the axiom and rules in Table 9, where in a transition \(m_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}}m_2\), \(m_1\) is the pre-set, \(\sigma \) is the label and \(m_2\) is the post-set.
Axiom (pref) states that if one token is present in the place \(\mu .p\) then a \(\mu \)-labeled transition is derivable from marking \(\{\mu .p\}\), producing the marking \({\mathrm{dec}}(p)\). This holds for any \(\mu \), i.e., for the invisible action \(\tau \), for any visible action \(\alpha \) as well as for any restricted action \(\alpha '\). In rule (s-pref), \(\gamma \) ranges over visible actions \(\alpha \) and restricted ones \(\alpha '\). This rule requires that the premise transition \(\{p\} {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} m\) be derivable by the rules, starting form the sequential process p. Rule (sum\(_1\)) and its symmetric (sum\(_2\)) are as expected: the transition from place \(p + p'\) are those from places p and \(p'\), as both p and \(p'\) are sequential. Finally, rule (s-com) explains how synchronization takes place: it is needed that \(m_1\) and \(m_2\) perform synchronizable sequences \(\sigma _1\) and \(\sigma _2\), producing \(\sigma \); here we assume that \(\mathrm {Sync}\) has been extended also to restricted actions in the obvious way, i.e., a restricted action \(\overline{\alpha '}\) can be synchronized only with its complementary restricted action \(\alpha '\) or with a sequence beginning with \(\alpha '\). As an example, net transition \(\{\underline{a}.b'.p, \overline{a}.q, \overline{b'}.r\} {{{\,\mathop {\longrightarrow }\limits ^{\tau }}}} {\mathrm{dec}}(p) \,\oplus \, {\mathrm{dec}}(q) \,\oplus \, {\mathrm{dec}}(r)\) is derivable (see Table 10).
Table 9
Rules for net transitions [symmetric rule (sum\(_2\)) omitted]
Transitions with labels containing restricted actions should not be taken in the resulting net, as we accept only transitions labeled on \({\mathcal A} = \{\tau \} \cup (\mathcal {L} \cup \overline{\mathcal {L}})^{+}\). However, they are useful in producing acceptable transitions, as two complementary restricted actions can synchronize, producing a \(\tau \)-labeled transition or shortening the synchronized sequence: e.g., in the example above, the derivable transition \(\{b'.p\} {{{\,\mathop {\longrightarrow }\limits ^{b'}}}} {\mathrm{dec}}(p)\) is not an acceptable transition because its label is not in \({\mathcal A}\), while \(\{\underline{a}.b'.p, \overline{a}.q, \overline{b'}.r\} {{{\,\mathop {\longrightarrow }\limits ^{\tau }}}} {\mathrm{dec}}(p) \,\oplus \, {\mathrm{dec}}(q) \,\oplus \, {\mathrm{dec}}(r)\) is so. Hence, the P/T net for finite-net multi-CCS is the triple \(N_{\mathrm{MCCS}} = (S_{\mathrm{MCCS}}, {\mathcal A},\)\( T_{\mathrm{MCCS}})\), where the set \(T_{\mathrm{MCCS}} = \{ (m_1, \sigma , m_2) \mid m_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}}m_2\)\( \text{ is } \text{ derivable } \text{ by } \text{ the } \text{ rules } \text{ and } \sigma \in {\mathcal A} \}\) is obtained by filtering out those transitions derivable by the rules such that no restricted name \(\alpha '\) occurs in \(\sigma \).
4.4 Properties of net transitions
Some useful properties of net transitions are listed here. First, given a transition \(t = (m_1, \sigma , m_2)\), derivable by the rules in Table 9, we show that the marking \(m_2\) generates subterms that are already present in the marking \(m_1\).
Proposition 9
Let \(t = m_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}}m_2\) be a transition derivable by the rules in Table 9. Then, sub(dom\((m_2)) \subseteq \mathrm{sub(dom}(m_1))\).
Proof
By induction on the proof of t. \(\square \)
Lemma 2
Let \(t = m_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}}m_2\) be a transition derivable by the rules in Table 9. Then, \(\mathrm{ns(dom}(m_2)) \subseteq \mathrm{ns(dom}(m_1))\).
Proof
By induction on the proof of t. \(\square \)
Proposition 10
If \(t = m_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}}m_2\) is derivable by the rules and \(\mathrm{dom}(m_1)\) is well-behaved, then \(\mathrm{dom}(m_2)\) is well-behaved.
Proof
By Lemma 2, we know that ns(dom\((m_2)) \subseteq \mathrm{ns(dom}(m_1))\). Therefore, if dom\((m_1)\) is well-behaved, then dom\((m_2)\) is well-behaved, too. \(\square \)
Corollary 1
If \(S_1\) is well-behaved and \(S_1 {{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}} S_k\), then \(S_k\) is well-behaved.
Proof
By induction on the static reachability relation \({{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}}\). The base case is \(S_1 {{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}} S_1\) and it is trivial. The inductive case is \(S_1 {{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}} S_{k-1} {{{\,\mathop {\Longrightarrow }\limits ^{t}\,}}}S_k\). By induction we can assume that \(S_{k-1}\) is well-behaved. Let \(t = m_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}}m_2\) be a transition in \(T_{\mathrm{MCCS}}\). The set ns\((S_{k-1})\) is ns\((S_{k-1}{\setminus }\mathrm{dom}(m_1)) \cup \mathrm{ns(dom}(m_1))\). The set ns\((S_k)\) is ns\((S_{k-1}) \cup \mathrm{ns(dom}(m_2))\). By Lemma 2, we have \(\mathrm{ns(dom}(m_2)) \subseteq \mathrm{ns(dom}(m_1))\). Therefore, ns\((S_k) = \mathrm{ns}(S_{k-1}) \cup \mathrm{ns(dom}(m_2)) \subseteq \mathrm{ns}(S_{k-1}) \cup \mathrm{ns(dom}(m_1)) = \mathrm{ns}(S_{k-1})\); hence, also \(S_k\) is well- behaved. \(\square \)
Now we want to prove that when a transition \(m {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} m'\), whose label \(\sigma \ne \tau \), involves in its proof some sequence of length greater than one, then the names of \(\sigma \) are all contained in ns(dom(m)).
Lemma 3
If \(t = (m, \sigma , m')\) is derivable by the rules of Table 9, and either \(|\sigma | \ge 2\) or \(\sigma \ne \tau \) and there exists a transition label \(\sigma '\) in its proof tree with \(|\sigma '| \ge 2\), then \(n(\sigma ) \subseteq \mathrm{ns(dom}(m))\).
Proof
By induction on the proof of transition t. If \(m = \{\mu .p\}\), then, by axiom (pref), \(t = (m, \mu , {\mathrm{dec}}(p))\). This case is vacuous as the only transition label in the proof tree is \(\mu \). If \(m = \{\underline{\gamma }.p\}\), then \(t = (m, \sigma , m')\) is derivable only if \((\{p\}, \sigma ', m')\) is derivable, with \(\sigma = \gamma \diamond \sigma '\). If \(|\sigma '| \ge 2\), then induction can be applied to conclude that \(n(\sigma ') \subseteq \mathrm{ns(dom}(\{p\}))) = \mathrm{ns}(\{p\}) = \mathrm{ns}(p)\); hence, \(n(\sigma ) = \{\gamma \} \cup n(\sigma ') \subseteq \{\gamma \} \cup \mathrm{ns}(p)\). Since \(\mathrm{ns}(m) = \mathrm{ns}(\{\underline{\gamma }.p\}) = \mathrm{ns}(\underline{\gamma }.p)\) and \(\{\gamma \} \cup \mathrm{ns}(p) \subseteq \mathrm{ns}(\underline{\gamma }.p)\), the thesis \(n(\sigma ) \subseteq n(m)\) follows trivially. If \(|\sigma '| = 1\), then two further subcases are possible: either \(\sigma ' = \tau \) or \(\sigma ' = \gamma '\); in the former subcase, this is possible only if p, being sequential, has performed a prefix \(\tau \) via (pref), so that no transition label in the proof tree is longer than one, hence this subcase is vacuous; in the latter subcase, \(\sigma = \gamma \gamma '\) and \(n(\sigma ) \subseteq \mathrm{ns}(\underline{\gamma }.p)\), because \(\gamma ' \in \mathrm{In}(p)\).
If \(m = \{p_1 + p_2\}\), then \(t = (m, \sigma , m')\) is derivable only if \((\{p_1\}, \sigma , m')\) or \((\{p_2\}, \sigma , m')\) are derivable. W.l.o.g., assume that \((\{p_1\}, \sigma , m')\); then, if the hypothesis holds for this premise, by induction, we have \(n(\sigma ) \subseteq \mathrm{ns}(\{p_1\}) = \mathrm{ns}(p_1)\). Since ns\((p_1) \subseteq \mathrm{ns}(p) = \mathrm{ns}(m)\), the thesis follows by transitivity.
If t is derived by rule (s-com), then \(m = m_1 \,\oplus \, m_2\), \(m' = m'_1 \,\oplus \, m'_2\) and transitions \(t_1 = (m_1, \sigma _1, m_1')\) and \(t_2 = (m_2, \sigma _2, m_2')\) are derivable, with \(\mathrm {Sync}(\sigma _1, \sigma _2, \sigma )\). As by hypothesis \(\sigma \ne \tau \), then \(\sigma _1\) or \(\sigma _2\) must be of length greater than one. W.l.o.g., assume \(|\sigma _1| \ge 2\). Since \(\mathrm {Sync}(\sigma _1, \sigma _2, \sigma )\), necessarily \(n(\sigma ) \subseteq n(\sigma _1)\). By induction, \(n(\sigma _1) \subseteq \mathrm{ns(dom}(m_1))\); as \(\mathrm{ns(dom}(m_1)) \subseteq \mathrm{ns(dom}(m_1\,\oplus \, m_2))\), the thesis follows by transitivity. \(\square \)
Proposition 11
If \(t = (m, \gamma , m')\) is derivable by the rules of Table 9 by using rule (s-com), then \(\gamma \in \mathrm{ns(dom}(m))\).
Proof
By induction on the proof of t. If rule (s-com) occurs in the proof of t, then m cannot be a sequential process. Therefore, the first rule must be (s-com), and so \(m = m_1 \,\oplus \, m_2\), \(m' = m'_1\, \,\oplus \,\, m'_2\), \(t_1 = (m_1, \sigma _1, m_1')\) and \(t_2 = (m_2, \sigma _2, m_2')\) are derivable, with \(\mathrm {Sync}(\sigma _1, \sigma _2, \gamma )\). So, \(\sigma _1\) or \(\sigma _2\) must be a sequence of length greater than one, and so by Lemma 3, it follows that \(\gamma \in \mathrm{ns(dom}(m))\). \(\square \)
Theorem 2
If \(t = (m, \sigma , m')\) is derivable by the rules and \(\mathrm{dom}(m)\) is well-behaved, then the proof of t never synchronizes two sequences, not even indirectly.
Proof
By induction on the proof of t. If m is a singleton, then rule (s-com) is never used, and so no synchronization of sequences is possible. Otherwise, the first rule must be (s-com), and so \(m = m_1 \,\oplus \, m_2\), \(m' = m'_1 \,\oplus \, m'_2\), \(t_1 = (m_1, \sigma _1, m_1')\) and \(t_2 = (m_2, \sigma _2, m_2')\) are derivable, with \(\mathrm {Sync}(\sigma _1, \sigma _2, \sigma )\). As \(\mathrm{dom}(m)\) is well-behaved, so are also \(\mathrm{dom}(m_1)\) and \(\mathrm{dom}(m_2)\); therefore, by induction, we know that in the proofs of transitions \(t_1\) and \(t_2\) two sequences are never synchronized. So, it remains to prove that the thesis holds for the resulting \(\sigma \). By definition of \(\mathrm {Sync}\), if \(\sigma = \tau \), then both \(\sigma _1\) and \(\sigma _2\) are complementary actions, say \(\sigma _1 = \gamma \) and \(\sigma _2 = \overline{\gamma }\). If both \(t_1\) and \(t_2\) are derived by using rule (s-com), then t synchronizes two sequences, even if indirectly; however, this is not possible, because Proposition 11 would ensure that \(\gamma \in \mathrm{ns(dom}(m_1))\) and \(\overline{\gamma } \in \mathrm{ns(dom}(m_2))\), contradicting that \(\mathrm{dom}(m_1 \,\oplus \, m_2)\) be well-behaved. Therefore, \(t_1\) or \(t_2\) is derived without using rule (s-com) and so no synchronization of sequences is produced. By definition of \(\mathrm {Sync}\), if \(\sigma \ne \tau \), then either \(\sigma _1\) or \(\sigma _2\) is a sequence of length greater than one; w.l.o.g. assume that \(|\sigma _1|\ge 2\) and \(\sigma _2 = \overline{\gamma }\). By Lemma 3, \(n(\sigma _1) \subseteq \mathrm{ns(dom}(m_1))\), in particular, \(\gamma \in \mathrm{ns(dom}(m_1))\). If \(t_2\) is derived by using rule (s-com), then Proposition 11 would ensure that \(\overline{\gamma } \in \mathrm{ns(dom}(m_2))\), contradicting that \(\mathrm{dom}(m_1 \,\oplus \, m_2)\) be well-behaved. Therefore, \(t_2\) is derived without using rule (s-com) and so no synchronization of sequences is produced. \(\square \)
Remark 2
By the proof of the prop above, it is clear that any transition \(t = m_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} m_2\) derivable from a well-behaved set of places \(\mathrm{dom}(m_1)\) is such that in the proof tree for t, whenever rule (s-com) is used with premise transitions \(t_1\) and \(t_2\), at least one of the two, say \(t_1\) w.l.o.g., is such that \({^{\bullet }t}_1\) is a singleton and \(l(t_1)\) is a single action in Act\(^{\gamma }\). That is, any derivable transition t from a well-behaved set of places \(\mathrm{dom}(m_1)\) is such that one sequential process \(s \in \mathrm{dom}(m_1)\) acts as the leader of the multi-party synchronization, while the other sequential components contribute each with a single action, acting as servants.
4.5 The reachable subnet \(\mathrm {Net}(p)\)
The P/T system associated to \(p \in \mathcal {P}^{\gamma }\) is the subnet of \(N_{\mathrm{MCCS}}\) statically reachable from the initial marking \({\mathrm{dec}}(p)\). We indicate with Net(p) such a subnet.
Definition 16
Let p be a process in \(\mathcal {P}^{\gamma }\). The P/T net system statically associated to p is Net\((p) = (S_p, A_p, T_p, m_0)\), where \(m_0 = {\mathrm{dec}}(p)\) and
$$\begin{aligned} S_p= & {} \llbracket \mathrm{dom}(m_0) \rangle \,\, \text{ computed } \text{ in }\,\, N_{\mathrm{MCCS}},\\ T_p= & {} \{ t \in T_{\mathrm{MCCS}} \mid S_p \llbracket t\rangle \}\\ A_p= & {} \{\sigma \in {\mathcal A} \mid \exists t \in T_p \text{ such } \text{ that } l(t) = \sigma \}. \end{aligned}$$
The following three propositions present facts that are obviously true by construction of the net Net(p) associated to a finite-net multi-CCS process p.
Proposition 12
For any \(p \in {\mathcal P}\), Net(p) is a statically reduced P/T net.
Proposition 13
If \({\mathrm{dec}}(p) = {\mathrm{dec}}(q)\), then Net\((p) = \mathrm{Net}(q)\).
Proposition 14
For any \(t \in \mathcal {P}\), let Net\((t) = (S, A, T, m_0)\). Then, for any \(n \ge 1\), Net\((t^n) = (S, A, T, n \cdot m_0)\), where \(t^1 = t\) and \(t^{n+1} = t {\,|\,}t^n\).
For any \({(\mathbf{\nu } L)}t \in \mathcal {P}\), let Net\(({(\mathbf{\nu } L)}t) = (S, A, T, m_0)\). Then, for any \(n \ge 1\), Net\(({(\mathbf{\nu } L)}(t^n)) = (S, A, T, n \cdot m_0)\).
Definition 16 suggests a way of generating Net(p) with an algorithm based on the inductive definition of the static reachability relation (see Definition 9): start by the initial set of places \(\mathrm{dom}({\mathrm{dec}}(p))\), and then apply the rules in Table 9 in order to produce the set of transitions (labeled on \({\mathcal A}\)) statically enabled at \(\mathrm{dom}({\mathrm{dec}}(p))\), as well as the additional places statically reachable by means of such transitions. Then repeat this procedure from the set of places statically reached so far. The problems with this algorithm are two:
the obvious halting condition is “until no new places are statically reachable”; of course, the algorithm terminates if we know that the set \(S_p\) of places statically reachable from \(\mathrm{dom}({\mathrm{dec}}(p))\) is finite; additionally,
at each step of the algorithm, we have to be sure that the set of transitions derivable from the current set of statically reachable places is finite.
We are going to prove these two facts: (i) \(S_p\) is finite for any \(p \in \mathcal {P}\), and (ii) for any well-formed process p, and for any set of places S, statically reachable from \(\mathrm{dom}({\mathrm{dec}}(p))\), the set of transitions statically enabled at S is finite.
Theorem 3
For any \(p \in \mathcal {P}\), let Net\((p) = (S_p, A_p, T_p, m_0)\) be defined as in Definition 16. Then, set \(S_p\) is finite.
Proof
We prove, by induction on the static reachability relation \({{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}}\), that any set \(S_i\) of places, statically reachable from \(\mathrm{dom}(m_0)\), is a subset of \(\mathrm{sub(dom}(m_0))\). This is enough as, by Proposition 8, we know that \(|\mathrm{sub}(p)| \ge |\mathrm{sub(dom}(m_0))|\); moreover, by Proposition 1, sub(p) is finite and so the thesis follows trivially.
The base case is \(\mathrm{dom}(m_0) {{{\,\mathop {\Longrightarrow }\limits ^{}\!\!\!^*\,}}} \mathrm{dom}(m_0)\). By Proposition 7, we have the required \(\mathrm{dom}(m_0) \subseteq \mathrm{sub(dom}(m_0))\).
Now, let us assume that \(S_i\) is a set of places statically reachable from \(\mathrm{dom}(m_0)\) and let \(t = m_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} m_2\) be such that \(S_i {{{\,\mathop {\Longrightarrow }\limits ^{t}\,}}}S_{i+1}\). By induction, we know that \(S_i \subseteq \mathrm{sub(dom}(m_0))\). So, we have to prove that the new places reached via t are in \(\mathrm{sub(dom}(m_0))\). Note that since \(\mathrm{dom}(m_1) \subseteq S_i\), it follows that \(\mathrm{dom}(m_1) \subseteq \mathrm{sub(dom}(m_0))\) and also that \(\mathrm{sub(dom}(m_1))) \subseteq \mathrm{sub(dom}(m_0))\), by Proposition 6. By Proposition 7, we have that \(\mathrm{dom}(m_2) \subseteq \mathrm{sub(dom}(m_2)\); by Proposition 9, we have that \(\mathrm{sub(dom}(m_2)) \subseteq \mathrm{sub(dom}(m_1))\); by transitivity, \(\mathrm{dom}(m_2) \subseteq \mathrm{sub(dom}(m_0))\), and so \(S_{i+1} = S_i \cup \mathrm{dom}(m_2) \subseteq \mathrm{sub(dom}(m_0))\), as required.
Summing up, any place statically reachable from \(\mathrm{dom}(m_0)\) is a (possibly, one-time renamed) sequential subterm of p. As by Proposition 1, sub(p) is finite, then also \(S_p\) (the largest set of places statically reachable from \(\mathrm{dom}(m_0)\)) is finite.
\(\square \)
We now want to prove that for any well-formed finite-net multi-CCS process p, and for any set of places \(S \subseteq S_{\mathrm{MCCS}}\), statically reachable from \(\mathrm{dom}({\mathrm{dec}}(p))\), the set of transitions statically enabled at S is finite. Some auxiliary definitions and results are necessary. Given a single place \(s \in S\), by \(s \vdash t\) we mean that transition \(t = (\{s\}, \sigma , m)\) is derivable by the rules in Table 9, hence with \(\sigma \in \mathcal {A}^{\gamma }\).
Lemma 4
Set \(T_s = \{ t \mid s \vdash t\}\) is finite, for any \(s \in S_{\mathrm{MCCS}}\).
Proof
By induction on the structure of the sequential process s and then by induction on the rules in Table 9.
Given a finite set of places \(S \subseteq S_{\mathrm{MCCS}}\), let \(T_1\) be \(\bigcup _{s \in S} T_s\), i.e., the set of all transitions, with a singleton preset in S, derivable by the rules with labeling in \(\mathcal {A}^{\gamma }\). Set \(T_1\) is finite, being the finite union (as S is finite) of finite sets (as \(T_s\) is finite for any s).
If p is well-formed, then \(\mathrm{dom}({\mathrm{dec}}(p))\) is well-behaved by Theorem 1. If S is statically reachable from \(\mathrm{dom}({\mathrm{dec}}(p))\), then S is well-behaved by Corollary 1. Let \(k \in {\mathbb N}\) be the length of the longest label of any transition in \(T_1\). Remark 2 explains that if a multi-party transition t is derivable by the rules from the well-behaved set \(\mathrm{dom}({^{\bullet }t}) \subseteq S\), then its proof contains \(k+1\) synchronizations at most, each one between a transition (labeled with a sequence) and a singleton-preset transition (labeled with a single action). Therefore, the set of all the transitions statically enabled at a well-behaved set S can be defined by means of a sequence of sets \(T_i\) of transitions, for \(2 \le i \le k+1\), where each transition \(t \in T_i\) has a preset \({^{\bullet }t}\) composed of i tokens, as follows:
Note that \(T_2\) is finite, because \(T_1\) is finite; inductively, \(T_{i+1}\), for \(2 \le i \le k\) is finite, because \(T_{i}\) and \(T_1\) are finite. The set \(T_S\) of all the transitions statically enabled at S is \(\{t \mid t \in \bigcup _{i = 1}^{k+1} T_i \wedge l(t) \in \mathcal {A}\}\), where only transitions labeled on \(\mathcal {A}\) are considered. \(T_S\) is finite, being a finite union of finite sets; therefore, we have the following result.
Proposition 15
If \(S \subseteq S_{\mathrm{MCCS}}\) is a well-behaved, finite set of places, then set \(T_S\) of all the transitions enabled at S is finite.
Example 4
Consider the non-well-formed process \(p = {(\mathbf{\nu } a)}(a.\mathbf{0}{\,|\,}(\underline{\overline{a}}.a.\mathbf{0}{\,|\,}\overline{a}.\mathbf{0}))\), discussed in Example 3. We have that \({\mathrm{dec}}(p) = a'.\mathbf{0}\,\oplus \, \underline{\overline{a'}}.a'.\mathbf{0}\,\oplus \, \overline{a'}.\mathbf{0}\), which is not well-behaved because \(a' \in \mathrm{ns(dom}({\mathrm{dec}}(p)))\) and \(\overline{a'} \in \mathrm{ns(dom}({\mathrm{dec}}(p)))\). It is easy to observe that transition \(t_1 = a'.\mathbf{0}\,\oplus \, \underline{\overline{a'}}.a'.\mathbf{0}\,\oplus \, \overline{a'}.\mathbf{0}{{{\,\mathop {\longrightarrow }\limits ^{\tau }}}} \emptyset \) is derivable, because first we synchronize \(\overline{a'}a'\) with \(a'\), yielding \(a'\), which is then synchronized with \(\overline{a'}\), yielding \(\tau \). However, the occurrence of action \(a'\) produced by the first synchronization may be used to synchronize an additional sequence \(\overline{a'}a'\), yielding \(a'\) again. Therefore, it is not difficult to see that also \(t_n = a'.\mathbf{0}\,\,\oplus \,\, n \cdot \underline{\overline{a'}}.a'.\mathbf{0}\,\oplus \, \overline{a'}.\mathbf{0}{{{\,\mathop {\longrightarrow }\limits ^{\tau }}}} \emptyset \), is statically enabled at \(\mathrm{dom}({\mathrm{dec}}(p))\), for any \(n \ge 1\). Hence, the set of transitions statically enabled at \(\mathrm{dom}({\mathrm{dec}}(p))\) is infinite.
Theorem 4
For any well-formed, finite-net multi-CCS process p, Net\((p) = (S_p, A_p, T_p, {\mathrm{dec}}(p))\) is a finite P/T net.
Proof
If p is well-formed, then \(\mathrm{dom}({\mathrm{dec}}(p))\) is well-behaved, by Theorem 1, and finite, by Proposition 4. By Proposition 15, set \(T_{\mathrm{dom(dec}(p))}\) is finite. Let \(S_1\) be the set of places \(\mathrm{dom}({\mathrm{dec}}(p)) \cup \bigcup _{t \in T_{\mathrm{dom}({\mathrm{dec}}(p))}} \mathrm{dom}({t^{\bullet }})\). If \(S_1 = \mathrm{dom}({\mathrm{dec}}(p))\), then \(S_p = \mathrm{dom}({\mathrm{dec}}(p))\) and \(T_p = T_{\mathrm{dom}({\mathrm{dec}}(p))}\). Otherwise, repeat the step above for \(S_1\); in fact, \(S_1\) is a finite set of places, because \(\mathrm{dom}({\mathrm{dec}}(p))\) is finite, set \(T_{\mathrm{dom}({\mathrm{dec}}(p))}\) is finite and each transition has a finite post-set; moreover, \(S_1\) is well-behaved by Corollary 1. By repeating the step above for \(S_1\), we compute a new finite set \(T_{S_1}\) of transitions statically enabled at \(S_1\), and a new finite set \(S_2\) of places statically reachable from \(S_1\) via the transitions in \(T_{S_1}\); if \(S_2 = S_1\), then \(S_p = S_1\) and \(T_p = T_{S_1}\). Otherwise, repeat the step above for \(S_2\). This procedure will end eventually because, by Theorem 3, we are sure that \(S_p\) is a finite set.
\(\square \)
Example 5
(Semi-counter) A semi-counter, i.e., a counter that cannot test for zero, can be described by the finite-net multi-CCS process \(B {{{\mathop {=}\limits ^{\mathrm{def}}}}}\)\(\mathrm{inc. (dec}.\mathbf{0}{\,|\,}B)\). Net(B) is the net \((S_B, A_B, T_B, m_0)\) we are going to construct, where the initial marking \(m_0\) is \({\mathrm{dec}}(B) =\)\( \{\mathrm{inc. (dec}.\mathbf{0}{\,|\,}B)\}\). Then, the only enabled transition is
and the set \(S_1\) of places statically reachable in one step from dom\((m_0)\) is \(S_1 = \{\mathrm{dec}.\mathbf{0}, \mathrm{inc.(dec}.\mathbf{0}{\,|\,}B)\}\). From \(S_1\), besides transition \(t_1\) above, also transition \(t_2 \, = \, \{\mathrm{dec}.\mathbf{0}\} {{{\,\mathop {\longrightarrow }\limits ^{\mathrm{dec}}}}} \emptyset \) is derivable, which however does not add any new reachable place. So, \(S_1\) is the set \(S_B\), \(\{t_1, t_2\}\) is the set \(T_B\) and \(\{\mathrm{inc, dec}\}\) is the set \(A_B\). The resulting net Net(B) is outlined in Fig. 1. \(\square \)
Fig. 1
The finite P/T system for a semi-counter
Table 11
The proof of a net transition, where \(s_2 = \underline{c'}.\underline{c'}.\mathrm{dec}.\mathbf{0}+ \overline{c}'.\mathbf{0}\)
×
×
Example 6
(1/3 Semi-counter) For the well-formed process \(p = {(\mathbf{\nu } c)}A\), where \(A {{{\mathop {=}\limits ^{\mathrm{def}}}}}\mathrm{inc.}(A {\,|\,}(\underline{c}.\underline{c}.\mathrm{dec}.\mathbf{0}+ \overline{c}.\mathbf{0}))\), three occurrences of inc are needed to enable one dec. Net(p) is the net \((S_p, A_p, T_p, m_0)\) we are going to construct, where the initial marking \(m_0\) is \({\mathrm{dec}}(p) = {\mathrm{dec}}({(\mathbf{\nu } c)}A) = {\mathrm{dec}}(A){\{c'/c\}} = \{\mathrm{inc}.(A {\,|\,}(\underline{c}.\underline{c}.\mathrm{dec}.\mathbf{0}+ \overline{c}.\mathbf{0}))\}{\{c'/c\}} = \{s_1\}\); place \(s_1\) is \(\mathrm{inc}.(A_{{\{c'/c\}}} {\,|\,}(\underline{c'}.\underline{c'}.\mathrm{dec}.\mathbf{0}+ \overline{c}'.\mathbf{0}))\), where the new constant \(A_{{\{c'/c\}}}\) is obtained by applying the substitution \({\{c'/c\}}\) to the body of A: \(A_{{\{c'/c\}}} {{{\mathop {=}\limits ^{\mathrm{def}}}}}\mathrm{inc}.(A_{{\{c'/c\}}} {\,|\,}(\underline{c'}.\underline{c'}.\mathrm{dec}.\mathbf{0}+ \overline{c'}.\mathbf{0}))\). Now, only transition \(t_1 = \{s_1\} {{{\,\mathop {\longrightarrow }\limits ^{\mathrm{inc}}}}} \{s_1, s_2\}\) is derivable from \(\mathrm{dom}(m_0) = \{s_1\}\), where \(s_2 = \underline{c'}.\underline{c'}.\mathrm{dec}.\mathbf{0}+ \overline{c}'.\mathbf{0}\) is a new statically reachable place. Note that \(s_2\) can produce two transitions in \(T_{s_2}\), namely \(t' = \{s_2\} {{{\,\mathop {\longrightarrow }\limits ^{c'c'\mathrm{dec}}}}} \emptyset \) and \(t'' = \{s_2\} {{{\,\mathop {\longrightarrow }\limits ^{\overline{c'}}}}} \emptyset \), but both are not labeled with a sequence in \(\mathcal {A}\). However, these transitions can be composed by means of rule (s-com), as shown in Table 11, to produce transition \(t_2 = 3\cdot s_2 {{{\,\mathop {\longrightarrow }\limits ^{\mathrm{dec}}}}} \emptyset \), which does not add any new reachable place. So, \(S_p = \{s_1, s_2\}\) and \(T_p = \{t_1, t_2\}\).
4.6 The CRW example
Let us consider process CRW of Sect. 3.4. The net associated to CRW is \(\mathrm{Net(CRW)} = (S_{\mathrm{CRW}}, A_{\mathrm{CRW}}, T_{\mathrm{CRW}}, m_0)\) we are going to construct, where the initial marking is \(m_0 = {\mathrm{dec}}(\mathrm{CRW}) = {\mathrm{dec}}({(\mathbf{\nu } l,u)}(R {\,|\,}R {\,|\,}R {\,|\,}R {\,|\,}W {\,|\,}W {\,|\,}L {\,|\,}L {\,|\,}L))\)\(= {\mathrm{dec}}(R {\,|\,}R {\,|\,}R {\,|\,}R {\,|\,}W {\,|\,}W {\,|\,}L {\,|\,}L {\,|\,}L){\{l'/l\}}{\{u'/u\}}\)\(= 4 \cdot rd \; \,\oplus \, \; 3 \cdot lk \; \,\oplus \, \; 2 \cdot wr\), where \(rd = l'.\mathrm{read}.u'.R'\) (with \(R' {{{\mathop {=}\limits ^{\mathrm{def}}}}}l'.\mathrm{read}.u'.R'\)), \(lk = \overline{l}'.\overline{u}'.L'\) (with \(L' {{{\mathop {=}\limits ^{\mathrm{def}}}}}\overline{l'}.\overline{u'}.L'\)) and \(wr = \underline{l}'.\underline{l}'.l'.\mathrm{write}.\underline{u}'.\underline{u}'.u'.W'\) (with \(W' {{{\mathop {=}\limits ^{\mathrm{def}}}}}\underline{l'}.\underline{l'}.l'.\mathrm{write}.\underline{u'}.\underline{u'}.u'.W'\)).
One of the two possible initial transitions is \(wr \,\oplus \, 3 \cdot lk {{{\,\mathop {\longrightarrow }\limits ^{\tau }}}} wr' \,\oplus \, 3 \cdot lk'\), where \(wr' = \mathrm{write}.\underline{u}'.\underline{u}'.u'.W'\) and \(lk' = \overline{u}'.L'\). After such a transition, no reader can read, as all the locks are busy. The other possible initial transition is \(rd \,\oplus \, lk {{{\,\mathop {\longrightarrow }\limits ^{\tau }}}} rd' \,\oplus \, lk'\), where \(rd' = \mathrm{read}.u'.R'\). From place \(wr'\), one transition is derivable, namely \(wr' {{{\,\mathop {\longrightarrow }\limits ^{\mathrm{write}}}}} wr''\), where \(wr'' = \underline{u}'.\underline{u}'.u'.W'\). From place \(rd'\), one transition is derivable, namely \(rd' {{{\,\mathop {\longrightarrow }\limits ^{\mathrm{read}}}}} rd''\), where \(rd'' = u'.R'\). Finally, two further transitions are derivable: \(rd'' \,\oplus \, lk' {{{\,\mathop {\longrightarrow }\limits ^{\tau }}}} rd \,\oplus \, lk\) and \(wr'' \,\oplus \, 3 \cdot lk' {{{\,\mathop {\longrightarrow }\limits ^{\tau }}}} wr \,\oplus \, 3 \cdot lk\). The resulting P/T Petri net Net(CRW) is depicted in Fig. 2.
Fig. 2
The net for the concurrent readers/writers problem
×
5 Soundness
In this section, we prove that the operational net semantics is sound w.r.t. the operational LTS semantics: for any process \(p \in \mathcal {P}\), the LTS rooted in p is bisimilar to the rooted LTS \(\mathrm {IMG}(\mathrm{Net}({\mathrm{dec}}({ p})))\). First, some auxiliary lemmata.
Lemma 5
Transition \(t = (m, \sigma , m')\) is derivable by the rules in Table 9 if and only if transition \(t' = (m{\{a'/a\}}, \sigma {\{a'/a\}},\)\(m'{\{a'/a\}})\) is derivable by the rules.
Proof
By induction on the proof of t. \(\square \)
Lemma 6
Let \(t_1 = (m_1, \sigma , m_1')\) be derivable by the rules in Table 9, and let p be a process such that \({\mathrm{dec}}(p)[t_1\rangle {\mathrm{dec}}(p')\). If \(p \equiv q\), then there exists a transition \(t_2 = (m_2, \sigma , m_2')\) such that \({\mathrm{dec}}(q)[t_2\rangle {\mathrm{dec}}(q')\), with \(q' \equiv p'\).
Proof
By induction on the proof of \(q \equiv p\) and then on the proof of \(t_1\). The base cases are the three axioms in Table 4. For axiom E1 (associativity), we have that \({\mathrm{dec}}(p {\,|\,}(q {\,|\,}r)) = {\mathrm{dec}}(p) \,\oplus \, {\mathrm{dec}}(q) \,\oplus \, {\mathrm{dec}}(r) = {\mathrm{dec}}((p {\,|\,}q) {\,|\,}r)\), so that transition \(t_2\) is exactly \(t_1\). Similarly, \({\mathrm{dec}}(p {\,|\,}q) = {\mathrm{dec}}(p) \,\oplus \, {\mathrm{dec}}(q) = {\mathrm{dec}}(q {\,|\,}p)\) and \({\mathrm{dec}}(A) = {\mathrm{dec}}(q)\) if \(A {{{\mathop {=}\limits ^{\mathrm{def}}}}}q\). So, for the base cases, the thesis follows trivially. For substitutivity of prefixing, we assume that \(p = \mu .p_1\), \(q = \mu .q_1\) and \(p_1 \equiv q_1\); in such a case, \(t_1 = (\{\mu .p_1\}, \mu , {\mathrm{dec}}(p_1))\) is the only transition enabled at \({\mathrm{dec}}(p)\); the required transition \(t_2\) is \((\{\mu .q_1\}, \mu , {\mathrm{dec}}(q_1))\). For substitutivity of strong prefixing, we assume that \(p = \underline{\alpha }.p_1\), \(q = \underline{\alpha }.q_1\) and \(p_1 \equiv q_1\); in such a case, \(t_1 = (\{\underline{\alpha }.p_1\}, \alpha \diamond \sigma ', {\mathrm{dec}}(p'_1))\) is derivable if \(t'_1 = (\{p_1\}, \sigma ', {\mathrm{dec}}(p'_1))\) is derivable; by induction, as \(p_1 \equiv q_1\), there exists transition \(t'_2 = (\{q_1\}, \sigma ', {\mathrm{dec}}(q'_1))\), with \(p'_1 \equiv q'_1\); then, by (s-pref), also transition \(t_2 = (\{\underline{\alpha }.q_1\}, \alpha \diamond \sigma ', {\mathrm{dec}}(q'_1))\) is derivable, as required. For substitutivity of choice, we assume that \(p = p_1 + p_2\), \(q = q_1 + q_2\) and \(p_i \equiv q_i\), for \(i = 1, 2\); in such a case, \(t_1 = (\{p_1 + p_2\}, \sigma , {\mathrm{dec}}(p'_1))\) is derivable if (w.l.o.g., we assume \(p_1\) moves) \(t'_1 = (\{p_1\}, \sigma , {\mathrm{dec}}(p'_1))\) is derivable by (sum\(_1\)); by induction, as \(p_1 \equiv q_1\), there exists transition \(t'_2 = (\{q_1\}, \sigma , {\mathrm{dec}}(q'_1))\), with \(p'_1 \equiv q'_1\); then, by (sum\(_1\)), also transition \(t_2 = (\{q_1 + q_2\}, \sigma , {\mathrm{dec}}(q'_1))\) is derivable, as required.
For substitutivity of parallel composition, we assume that \(p = p_1 {\,|\,}p_2\), \(q = q_1 {\,|\,}q_2\), \(p_i \equiv q_i\) for \(i = 1, 2\), and \({\mathrm{dec}}(p)[t_1\rangle {\mathrm{dec}}(p')\). We have three subcases: (i) \({\mathrm{dec}}(p_1)[t_1\rangle {\mathrm{dec}}(p_1')\), with \(p' = p_1' {\,|\,}p_2\); or (ii) \({\mathrm{dec}}(p_2)[t_1\rangle {\mathrm{dec}}(p_2')\), with \(p' = p_1 {\,|\,}p_2'\); or (iii) neither of the previous two cases, i.e., \({^{\bullet }t}_1\) is not contained in \({\mathrm{dec}}(p_1)\) or \({\mathrm{dec}}(p_2)\). In the first case, by induction (since \(p_1 \equiv q_1\)), there exists \(t_2\) such that \({\mathrm{dec}}(q_1)[t_2\rangle {\mathrm{dec}}(q_1')\), with \(p'_1 \equiv q'_1\), and so \({\mathrm{dec}}(q)[t_2 \rangle {\mathrm{dec}}(q_1' {\,|\,}q_2)\), with \(q_1' {\,|\,}q_2 \equiv p_1' {\,|\,}p_2\); the second case is symmetric, hence omitted.
In the third case, there exist two transitions, say \(t'_1\) and \(t'_2\), with \(l(t'_1) = \sigma _1\), \(l(t'_2) = \sigma _2\) and \(\mathrm {Sync}(\sigma _1, \sigma _2, \sigma )\), such that, by rule (s-com), \(t_1\) is \(t'_1 | t'_2 = ({^{\bullet }t}'_1 \,\oplus \, {^{\bullet }t}'_2, \sigma , {t'_{1}}^{\bullet } \,\oplus \, {t'_{2}}^{\bullet })\). By using the three axioms of the structural congruence \(\equiv \) at the top level only (that we know can be used safely), we can find two processes \(\overline{p}_1, \overline{p}_2\) such that \(p \equiv \overline{p}_1 {\,|\,}\overline{p}_2\), \({\mathrm{dec}}(\overline{p}_1)[t'_1\rangle {\mathrm{dec}}(\overline{p}'_1)\), \({\mathrm{dec}}(\overline{p}_2)[t'_2\rangle {\mathrm{dec}}(\overline{p}_2')\). Since \(p \equiv q\), we can find two processes \(\overline{q}_1, \overline{q}_2\) such that \(q \equiv \overline{q}_1 {\,|\,}\overline{q}_2\) and \(\overline{p}_i \equiv \overline{q}_i\) for \(i = 1, 2\). Then, induction can be applied to conclude that there exist two transitions \(t''_1\) and \(t''_2\) such that \({\mathrm{dec}}(\overline{q}_1)[t''_1\rangle {\mathrm{dec}}(\overline{q}'_1)\), \({\mathrm{dec}}(\overline{q}_2)[t''_2\rangle {\mathrm{dec}}(\overline{q}'_2)\), with \(\overline{p}'_i \equiv \overline{q}'_i\) for \(i = 1, 2\). So, by rule (s-com), transition \(t_2 = t''_1 | t''_2 = ({^{\bullet }t}''_1 \,\oplus \, {^{\bullet }t}''_2, \sigma , {t''_{1}}^{\bullet } \,\oplus \, {t''_{2}}^{\bullet })\) is derivable; hence, \({\mathrm{dec}}(q) = {\mathrm{dec}}(\overline{q}_1) \,\oplus \, {\mathrm{dec}}(\overline{q}_2) [t_2\rangle {\mathrm{dec}}(\overline{q}'_1 {\,|\,}\overline{q}_2')\), with \(\overline{q}'_1 {\,|\,}\overline{q}_2' \equiv \overline{p}'_1 {\,|\,}\overline{p}_2' \equiv p'\).
For substitutivity of restriction, we assume that \(p ={(\mathbf{\nu } a)}p_1\), \(q = {(\mathbf{\nu } a)}q_1\), \(p_1 \equiv q_1\), and \({\mathrm{dec}}(p) [t_1\rangle \, {\mathrm{dec}}(p')\), with \(l(t_1) = \sigma \) and \(a, \bar{a} \not \in n(\sigma )\). Since \({\mathrm{dec}}(p) = {\mathrm{dec}}(p_1){\{a'/a\}}\), \(t_1\) has the form \((m_1{\{a'/a\}}, \sigma , m_1'{\{a'/a\}})\), and \(t'_1 = (m_1, \sigma , m_1')\) is derivable by Lemma 5; moreover, \({\mathrm{dec}}(p_1)[t'_1\rangle {\mathrm{dec}}(p_1')\), with \({\mathrm{dec}}(p') = {\mathrm{dec}}(p_1'){\{a'/a\}}\)\( = {\mathrm{dec}}({(\mathbf{\nu } a)}p_1')\). By induction, as \(p_1 \equiv q_1\), there exists \(t'_2 = (m_2, \sigma , m_2')\) such that \({\mathrm{dec}}(q_1)[t'_2\rangle {\mathrm{dec}}(q_1')\), with \(q'_1 \equiv p'_1\). By Lemma 5, also \(t_2 = (m_2{\{a'/a\}}, \sigma , m_2'{\{a'/a\}})\) is derivable, with \({\mathrm{dec}}(q) = {\mathrm{dec}}(q_1){\{a'/a\}} \,[t_2\rangle \, {\mathrm{dec}}(q_1'){\{a'/a\}} = {\mathrm{dec}}({(\mathbf{\nu } a)}q_1')\), where \({(\mathbf{\nu } a)}q_1' \equiv {(\mathbf{\nu } a)}p'_1\) as required. \(\square \)
Proposition 16
For any process \(p \in {\mathcal P}\), if \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\) then there exist \(t \in T_p\) and \(p'' \equiv p'\) such that \({\mathrm{dec}}(p)[t\rangle {\mathrm{dec}}(p'')\) with \(l(t) = \sigma \).
Proof
The proof is by induction on the proof of \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\). The base case is axiom (Pref), hence \(p = \mu .q\), \(\sigma = \mu \) and \(p' = q\). The thesis follows by noting that axiom (pref) ensures that \({\mathrm{dec}}(p) = \{\mu .q\} {{{\,\mathop {\longrightarrow }\limits ^{\mu }}}} {\mathrm{dec}}(q) = {\mathrm{dec}}(p')\) is in \(T_p\).
If rule (S-pref) is the last rule used to derive \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\), then \(p = \underline{\alpha }.q\), \(q {{{\,\mathop {\longrightarrow }\limits ^{\sigma '}}}} p'\) and \(\sigma = \alpha \diamond \sigma '\). The inductive hypothesis on the premise of rule (S-pref) ensures that there exist a transition \(t = (m, \sigma ', m')\) and a process \(p'' \equiv p'\) such that \({\mathrm{dec}}(q)[t\rangle {\mathrm{dec}}(p'')\) with \(l(t) = \sigma '\). Since q must be sequential, then \(m = {\mathrm{dec}}(q) = \{q\}\) and \(m' = {\mathrm{dec}}(p'')\). Hence the thesis follows by rule (s-pref): \(t = (\{q\}, \sigma ', {\mathrm{dec}}(p''))\) implies \({\mathrm{dec}}(p) = \{\underline{\alpha }.q \} {{{\,\mathop {\longrightarrow }\limits ^{\alpha \diamond \sigma '}}}} {\mathrm{dec}}(p'')\).
If rule (Sum\(_1\)) is the last rule applied to derive transition \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\), then \(p = p_1 + p_2\) and \(p_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\). The inductive hypothesis on the premise of rule (Sum\(_1\)) ensures that there exist a transition \(t = (m, \sigma ', m')\) and a process \(p'' \equiv p'\) such that \({\mathrm{dec}}(p_1)[t\rangle {\mathrm{dec}}(p'')\) with \(l(t) = \sigma \). Since \(p_1\) is sequential, \(m = {\mathrm{dec}}(p_1) = \{p_1\}\) and \(m' = {\mathrm{dec}}(p'')\). Hence, the thesis follows by rule (sum\(_1\)): t implies \({\mathrm{dec}}(p_1 + p_2) {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} {\mathrm{dec}}(p'')\). Symmetrically, if (Sum\(_2\)) is the last rule applied.
If rule (Par\(_1\)) is the last rule used to derive \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\), then \(p = p_1 {\,|\,}p_2\) and \(p_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'_1\). The inductive hypothesis on the premise of (Par\(_1\)) ensures that there exist a transition \(t = (m_1, \sigma , m_1')\) and a process \(p_1'' \equiv p'_1\) such that \({\mathrm{dec}}(p_1)[t\rangle {\mathrm{dec}}(p''_1)\) with \(l(t) = \sigma \). Hence, the thesis then follows by additivity: \({\mathrm{dec}}(p_1 {\,|\,}p_2) = {\mathrm{dec}}(p_1) \,\oplus \, {\mathrm{dec}}(p_2)[t\rangle {\mathrm{dec}}(p''_1) \,\oplus \, {\mathrm{dec}}(p_2) = {\mathrm{dec}}(p''_1 {\,|\,}p_2)\), with \(p''_1 {\,|\,}p_2 \equiv p'_1 {\,|\,}p_2\). Symmetrically, if rule (Par\(_2\)) is the last rule applied.
If rule (S-Com) is the last rule used to derive \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\), then \(p = p_1 {\,|\,}p_2\), \(p' = p'_1 {\,|\,}p'_2\), \(p_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma _1}}}} p'_1\), \(p_2 {{{\,\mathop {\longrightarrow }\limits ^{\sigma _2}}}} p'_2\) and \(\mathrm {Sync}(\sigma _1, \sigma _2, \sigma )\). The inductive hypothesis on the premises of (S-Com) ensures that there exist two transitions, \(t_1\) and \(t_2\), and two processes, \(p''_1 \equiv p'_1\) and \(p''_2 \equiv p'_2\), such that \({\mathrm{dec}}(p_1)[t_1\rangle {\mathrm{dec}}(p''_1)\) with \(l(t_1) = \sigma _1\), and \({\mathrm{dec}}(p_2)[t_2\rangle {\mathrm{dec}}(p''_2)\) with \(l(t_2) = \sigma _2\). Hence, by rule (s-com), \(t_1\) and \(t_2\) imply transition \(t_1 | t_2 = ({^{\bullet }t}_1 \,\oplus \, {^{\bullet }t}_2, \sigma , {t_1}^{\bullet } \,\oplus \, {t_2}^{\bullet })\); note that we are sure that the executability of \(t_1\) and \(t_2\) on their respective markings ensures that also the compound transition \(t_1 | t_2\) is executable on the union of the two markings, i.e., \({\mathrm{dec}}(p_1) \,\oplus \, {\mathrm{dec}}(p_2) [t_1 | t_2\rangle {\mathrm{dec}}(p''_1) \,\oplus \, {\mathrm{dec}}(p''_2)\). Hence: \({\mathrm{dec}}(p_1 {\,|\,}p_2) [t_1 | t_2\rangle {\mathrm{dec}}(p''_1 {\,|\,}p''_2)\), with \(p''_1 {\,|\,}p''_2 \equiv p'_1 {\,|\,}p'_2\).
If rule (S-Res) is the last rule used to derive \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\), then \(p = {(\mathbf{\nu } a)} p_1\), \(p' = {(\mathbf{\nu } a)}p'_1\), \(p_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'_1\) and \(a, \bar{a} \not \in n(\sigma )\). The inductive hypothesis on the premise of rule (S-Res) ensures that there exist a transition \(t = (m, \sigma , m')\) and a process \(p''_1 \equiv p'_1\) such that \({\mathrm{dec}}(p_1)[t\rangle {\mathrm{dec}}(p''_1)\) with \(l(t) = \sigma \). Note that \({\mathrm{dec}}({(\mathbf{\nu } a)} p_1) = {\mathrm{dec}}(p_1){\{a'/a\}}\) for \(a'\) restricted. Note also that, by Lemma 5, if t is derivable by the net rules, then also transition \(t' = (m{\{a'/a\}}, \sigma ,\)\(m'{\{a'/a\}})\) is derivable by the net rules. Therefore, since \(m{\{a'/a\}} \subseteq {\mathrm{dec}}(p_1){\{a'/a\}}\), we have that \({\mathrm{dec}}({(\mathbf{\nu } a)} p_1) = {\mathrm{dec}}(p_1){\{a'/a\}} \, [t'\rangle \, {\mathrm{dec}}(p''_1){\{a'/a\}} = {\mathrm{dec}}({(\mathbf{\nu } a)} p''_1)\), with \({(\mathbf{\nu } a)}p''_1 \equiv {(\mathbf{\nu } a)}p'_1\).
If rule (Cong) is the last rule used to derive \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\), then \(p \equiv q\), \(q {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} q'\) and \(q' \equiv p'\). The inductive hypothesis on the premise ensures the existence of a transition \(t' = (m', \sigma , m'')\) and a process \(q'' \equiv q'\) such that \({\mathrm{dec}}(q)[t'\rangle {\mathrm{dec}}(q'')\) with \(l(t') = \sigma \). By Lemma 6, there exists a transition t, with \(l(t) = \sigma \), such that \({\mathrm{dec}}(p)[t\rangle {\mathrm{dec}}(p'')\) and \(p'' \equiv q''\), hence, by transitivity, \(p'' \equiv p'\). \(\square \)
Proposition 17
For any process \(p \in {\mathcal P}\), if there exists \(t \in T_p\) such that \({\mathrm{dec}}(p)[t\rangle {\mathrm{dec}}(p')\) with \(l(t) = \sigma \), then \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\).
Proof
By induction on the definition of \({\mathrm{dec}}(p, I)\) and then by induction on the proof of t. The base cases are empty. The first base case is \({\mathrm{dec}}(\mathbf{0}, I) = \emptyset \) and so no transition t is enabled. Similarly, the second base case is \(p = A\), with \(A \in I\) (hence, \({\mathrm{dec}}(A, I) = \emptyset \)). The other cases follow.
\({\mathrm{dec}}(\mu .q, I) = \{\mu .q\}\). By axiom (pref), the only derivable transition is \(t = (\{\mu .q\}, \mu , {\mathrm{dec}}(q))\). By axiom (Pref), \(\mu .q {{{\,\mathop {\longrightarrow }\limits ^{\mu }}}} q\), and so the thesis follows trivially.
\({\mathrm{dec}}(\underline{\alpha }.q, I) = \{\underline{\alpha }.q\}\). By rule (s-pref), a transition \(t = (\{\underline{\alpha }.q\}, \alpha \diamond \sigma ', {\mathrm{dec}}(q'))\) is derivable only if a transition \(t' = (\{q\}, \sigma ', {\mathrm{dec}}(q'))\) is derivable. The inductive hypothesis on the premise \(t'\) of the rule (s-pref) ensures that \(q {{{\,\mathop {\longrightarrow }\limits ^{\sigma '}}}} q'\). By rule (S-Pref), \(\underline{\alpha }.q {{{\,\mathop {\longrightarrow }\limits ^{\alpha \diamond \sigma '}}}} q'\), as required.
\({\mathrm{dec}}(p_1 + p_2, I) = \{p_1 + p_2\}\). By rule (sum\(_1\)), transition \(t = (\{p_1 + p_2\}, \sigma , {\mathrm{dec}}(p'))\) is derivable only if transition \(t' = (\{p_1\}, \sigma , {\mathrm{dec}}(p'))\) is derivable. The inductive hypothesis on the premise \(t'\) of the rule (sum\(_1\)) ensures that \(p_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\). By rule (Sum\(_1\)), \(p_1 + p_2 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\), as required. Symmetrically, if rule (sum\(_2\)) is used.
\({\mathrm{dec}}(p_1 {\,|\,}p_2, I) = {\mathrm{dec}}(p_1, I) \,\oplus \, {\mathrm{dec}}(p_2, I)\). Given a transition t, with \(l(t) = \sigma \), such that \({\mathrm{dec}}(p_1 {\,|\,}p_2, I) [t\rangle {\mathrm{dec}}(p')\), three cases are possible. If t is enabled at \({\mathrm{dec}}(p_1, I)\) and so \({\mathrm{dec}}(p_1, I)[t\rangle {\mathrm{dec}}(p_1')\), then \(p' = p_1' {\,|\,}p_2\) and, by induction, we know that \(p_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'_1\). Hence the thesis follows by rule (Par). Symmetrically, if t is enabled at \({\mathrm{dec}}(p_2)\). The third case is when transition t is such that \({^{\bullet }t}\) is not contained in \({\mathrm{dec}}(p_1, I)\) or in \({\mathrm{dec}}(p_2, I)\). In such a case, there exist two transitions, say \(t_1\) and \(t_2\), with \(l(t_1) = \sigma _1\), \(l(t_2) = \sigma _2\) and \(\mathrm {Sync}(\sigma _1, \sigma _2, \sigma )\), such that, by rule (s-com), t is \(t_1 | t_2 = ({^{\bullet }t}_1 \,\oplus \, {^{\bullet }t}_2, \sigma , {t_{1}}^{\bullet } \,\oplus \, {t_{2}}^{\bullet })\). The marking \({\mathrm{dec}}(p_1, I) \,\oplus \, {\mathrm{dec}}(p_2, I)\) can be equivalently represented as \({\mathrm{dec}}(q_1, I) \,\oplus \, {\mathrm{dec}}(q_2, I)\) such that \(p_1 {\,|\,}p_2 \equiv q_1 {\,|\,}q_2\), \({\mathrm{dec}}(q_1, I)[t_1\rangle {\mathrm{dec}}(q'_1)\) and \({\mathrm{dec}}(q_2, I)[t_2\rangle {\mathrm{dec}}(q_2')\). Then, induction can be applied to conclude that \(q_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma _1}}}} q'_1\) and \(q_2 {{{\,\mathop {\longrightarrow }\limits ^{\sigma _2}}}} q_2'\); hence, by rule (S-Com), also \(q_1 {\,|\,}q_2 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} q_1' {\,|\,}q_2'\) is derivable, and by rule (Cong), \(p_1 {\,|\,}p_2 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} q_1' {\,|\,}q_2'\), as required.
\({\mathrm{dec}}({(\mathbf{\nu } a)}p_1, I) = {\mathrm{dec}}(p_1, I){\{a'/a\}}\). A transition t, with \(l(t) = \sigma \in \mathcal {A}\) and \(a, \bar{a} \not \in n(\sigma )\), is such that \({\mathrm{dec}}(p_1, I){\{a'/a\}} [t\rangle {\mathrm{dec}}(p_1'){\{a'/a\}}\) if transition t has the form \((m{\{a'/a\}}, \sigma , m'{\{a'/a\}})\); so transition \(t' = (m, \sigma , m')\) is derivable by Lemma 5 and \({\mathrm{dec}}(p_1, I) [t'\rangle {\mathrm{dec}}(p_1')\). By induction, we have \(p_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p_1'\), and so by rule (S-Res), also \({(\mathbf{\nu } a)}p_1 {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} {(\mathbf{\nu } a)}p_1'\) is derivable, as required.
\({\mathrm{dec}}(A, I) = {\mathrm{dec}}(p, I \cup \{A\})\) if \(A {{{\mathop {=}\limits ^{\mathrm{def}}}}}p\) and \(A \not \in I\). Then, if there exists t, with \(l(t) = \sigma \), such that \({\mathrm{dec}}(A, I)[t\rangle {\mathrm{dec}}(p')\), then also \({\mathrm{dec}}(p, I \cup \{A\}) [t\rangle {\mathrm{dec}}(p')\). By induction, we can assume that transition \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\) is derivable. Hence, by rule (Cong), also \(A {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\) is derivable, too. \(\square \)
We are now ready to state the soundness theorem: the interleaving marking graph associated to Net(p) is bisimilar to the LTS rooted in p.
Theorem 5
(Soundness) For any process \(p \in {\mathcal P}\), \(p \sim {\mathrm{dec}}(p)\).
Proof
If the relation \(R = \{(p, {\mathrm{dec}}(q)) \mid p, q \in {\mathcal P} \wedge p \equiv q\}\) is a bisimulation, then the thesis follows trivially, as \(p \equiv p\). On the one hand, if \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} p'\), then, by Proposition 16, there exist a transition t, with \(l(t) = \sigma \), and a process \(p''\), with \(p'' \equiv p'\), such that \({\mathrm{dec}}(p) [t\rangle {\mathrm{dec}}(p'')\), and \((p', {\mathrm{dec}}(p'')) \in R\). On the other hand, if \({\mathrm{dec}}(q)[t\rangle {\mathrm{dec}}(q')\), with \(l(t) = \sigma \), then, by Proposition 17, we have \(q {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} q'\); as \(p \equiv q\), by rule (Cong), \(p {{{\,\mathop {\longrightarrow }\limits ^{\sigma }}}} q'\), and \((q', {\mathrm{dec}}(q')) \in R\), as required.
6 A process term for any finite P/T net
In this section we address the following problem: given a finite, statically reduced, P/T Petri net system \(N(m_0)\), labeled on \(\mathcal {L} \cup \{\tau \}\), can we single out a finite-net multi-CCS process \(p_{N(m_0)}\) such that Net\((p_{N(m_0)})\) and \(N(m_0)\) are isomorphic? The answer to this question is positive; hence, finite-net multi-CCS can represent all finite, statically reduced, P/T Petri nets, up to net isomorphism.
The translation from nets to processes we are going to present defines a constant \(C_i\) in correspondence to each place \(s_i\); the definition of the constant \(C_i\) contains an addend composed of a new bound name \(y_i\), which is used in order to distinguish syntactically all the constants bodies, so that no fusion of two constants to the same place is possible when applying the reverse step from the generated process term to its associated net (see Example 8). Moreover, the translation considers a bound name \(x^j_i\) for each pair \((s_i, t_j)\), where \(s_i\) is a place and \(t_j\) is a transition; such bound names are used to synchronize all the components participating in transition \(t_j\). The constant \(C_i\), associated to place \(s_i\), has a summand \(c^j_i\) for each transition \(t_j\), which may be \(\mathbf{0}\) when \(s_i\) is not in the pre-set of \(t_j\). Among the many places in the pre-set of \(t_j\), the one with minimal index (as we assume that places are indexed) plays the role of leader of the multi-party synchronization (i.e., the process performing the atomic sequence of inputs \(x^j_i\) to be synchronized with single outputs \(\bar{x}^j_i\) performed by the other servant participants).
Definition 17
Let \(N(m_0) = (S, A, T, m_0)\)—with \(S = \{s_1, \ldots , s_n\}\), \(A \subseteq \mathcal {L} \cup \{\tau \}\), \(T = \{t_1, \ldots , t_k\}\), and \(l(t_j) = a_j\) for \(j = 1, \ldots , k\)—be a finite P/T net system. Function \(\mathrm{INet}(-)\), from finite P/T net systems to well-formed, finite-net multi-CCS processes is defined as
where each \(c_i^j\), for \(j = 1, \ldots , k\), is equal to
\(\mathbf{0}\), if \(s_i \not \in {^{\bullet }t}_j\);
\(a_{j}.\Pi _{j}\), if \({^{\bullet }t} _{j} = \{s_i\}\);
\(\overline{x}^j_{i}.\mathbf{0}\), if \({^{\bullet }t}_{j} (s_i) > 0\) and \({^{\bullet }t}_{j} (s_{i'}) > 0\) for some \(i' < i\) (i.e., \(s_i\) is not the leader for the synchronization on \(t_{j}\));
\(\underbrace{ \underline{x}^j_{i+1}. \cdots . \underline{x}^j_{i+1}}_{{^{\bullet }t}_j(s_{i+1})}. \cdots .\underbrace{ \underline{x}^j_{n}. \cdots .\underline{x}^j_{n}}_{{^{\bullet }t}_j(s_{n})}.a_{j}.\Pi _{j}\), if \({^{\bullet }t}_{j} (s_i) = 1\) and \(s_i\) is the leader of the synchronization (i.e., \({^{\bullet }t}_{j} (s_{i'}) > 0\) for no \(i' < i\), while \({^{\bullet }t}_{j} (s_{i'}) > 0\) for some \(i' > i\));
Finally, process \(\Pi _{j}\) is defined as \( \Pi _{j} = \underbrace{ C_1 | \cdots | C_1}_{ {t_{j}^{\bullet }} (s_1) } | \cdots | \underbrace{ C_n | \cdots | C_n}_{ {t_{j}^{\bullet }} (s_n) }\), meaning that \(\Pi _{j} = \mathbf{0}\) if \({t_j^{\bullet }} = \emptyset \).
Example 7
Consider the net \(N(m_0)\) of Fig. 3, where transition \(t_1\) is labeled with a, \(t_2\) with b and \(t_3\) with c. Applying the translation above, we obtain the well-formed, finite-net multi-CCS process
Note that \(\mathrm{INet}(N(m_0))\) is a finite-net multi-CCS process: in fact, the restriction operator occurs only at the top level, applied to the parallel composition of a number of constants; each constant has a body that is sequential and restriction-free. Note also that \(\mathrm{INet}(N(m_0))\) is a well-formed process: in fact, each strong prefix is an input \(x^j_i\), and any sequence ends with an action \(a_j \in A\) which is either an input or \(\tau \); hence, no synchronization of sequences is possible. Therefore, the following proposition holds by Theorem 4 and Proposition 12.
Proposition 18
For any finite P/T Petri net \(N(m_0) = (S, A, T, m_0)\), the net Net\((\mathrm{INet}(N(m_0)))\) is a finite, statically reduced, P/T net.
Example 8
In order to explain the role of addend \(y_i\) in the body of constant \(C_i\), for \(i = 1, \ldots , n\), let us assume that they are omitted in Definition 17. Now, let us consider the net \(N(\{s_1, s_2\}) =\)\((\{s_1, s_2, s_3, s_4\}, \{a\}, \{(s_1, a, s_3), (s_2, a, s_4)\},\)\(\{s_1, s_2\})\), which has four places and two transitions. The finite-net multi-CCS term \(\mathrm{INet}(N(\{s_1, s_2\}))\) would be \({(\mathbf{\nu } L)} (C_1 {\,|\,}C_2)\), where \(L = \{x^1_1, x^1_2, x^2_1, x^2_2\}\) and
but now Net\((\mathrm{INet}(N(\{s_1, s_2\})))\) is the net \((\{a.C_3 + \mathbf{0}, \mathbf{0}+ a.C_4, \mathbf{0}+ \mathbf{0}\}, \{a\},\)\(\{(a.C_3 + \mathbf{0}, a, \mathbf{0}+ \mathbf{0}), (\mathbf{0}+ a.C_4, a, \mathbf{0}+ \mathbf{0})\}, \{a.C_3 + \mathbf{0}, \mathbf{0}+ a.C_4\})\), which has three places only, as the two distinct places \(s_3\) and \(s_4\) are now mapped to the same place \(\mathbf{0}+ \mathbf{0}\). This fusion cannot happen when we include the additional addend \(y_i\) in the body of each constant \(C_i\).
Now we are ready to state our main result, the so-called representability theorem.
Theorem 6
(Representability theorem) Let \(N(m_0) = (S, A, T, m_0)\) be a finite, statically reduced, P/T net system such that \(A \subseteq \mathcal {L} \cup \{\tau \}\), and let \(p = \mathrm{INet}(N(m_0))\). Then, Net(p) is isomorphic to \(N(m_0)\).
Proof
Let \(N(m_0) = (S, A, T, m_0)\) be a finite, statically reduced, P/T net system, with \(S = \{s_1, \ldots , s_n\}\), \(A \subseteq \mathcal {L} \cup \{\tau \}\), \(T = \{t_1, \ldots , t_k\}\) and \(l(t_j) = a_j\) for \(j = 1, \ldots , k\). The associated finite-net multi-CCS process is
where \(L = \{y_1,\ldots , y_n\} \cup \{x^1_1,\ldots , x^1_n, x^2_1, \ldots , x^2_n, \ldots , x^k_1, \ldots ,x^k_n\}\), and for each place \(s_i\) we have a corresponding constant \(C_i {{{\mathop {=}\limits ^{\mathrm{def}}}}}(\sum _{j=1}^{k} c^j_i) + y_i.\mathbf{0}\), defined as in Definition 17. For notational convenience, \((\sum _{j=1}^{k} c^j_i) + y_i.\mathbf{0}\) is denoted by \(p_i\), i.e., \(C_i {{{\mathop {=}\limits ^{\mathrm{def}}}}}p_i\); for the same reason, we use p to denote \(\mathrm{INet}(N(m_0))\).
Let \(\rho = {\{L'/L\}}\) be a substitution that maps each bound name \(x^j_i\) (or \(y_i\)) to its corresponding restricted name \(x'^j_i\) (or \(y'_i\)) in \({\mathcal L}'\), for \(i = 1, \ldots , n\) and \(j = 1, \ldots , k\). Let Net\((p) = (S', A', T',m'_0)\). Then, \(m'_0 = {\mathrm{dec}}(p)\) is the multiset
because \(C_i {{{\mathop {=}\limits ^{\mathrm{def}}}}}p_i\) for \(i = 1, \ldots n\) and so \({\mathrm{dec}}(C_i) = \{p_i\}\). Hence, the initial places are all of the form \(p_i \rho \), where such a place is present in \(m'_0\) only if \(m_0(s_i) > 0\).
Note that, by Definition 17, any transition \(t' \in T'\) is such that \({t'^{\bullet }} = {\mathrm{dec}}(\Pi _j)\) for some suitable j, so that each statically reachable place \(s'_i\) in \(S'\) is of the form \(p_i\rho \), which are all distinct because each \(p_i\) contains one distinguishing summand \(y_i.\mathbf{0}\). Hence, there is a bijection \(f: S \rightarrow S'\) defined by \(f(s_i) = s'_i = p_i\rho \), which is the natural candidate isomorphism function. To prove that f is an isomorphism, we have to prove that:
1.
\(f(m_{0}) = m'_0\),
2.
\(t = (m, a, m') \in T\) implies \(f(t) = (f(m), a, f(m')) \in T'\), and
3.
\(t' = (m'_1, a, m_2') \in T'\) implies there exists \(t = (m_1, a, m_2) \in T\) such that \(f(t) = t'\), i.e., \(f(m_1) = m'_1\) and \(f(m_2) = m'_2\).
From items (2) and (3) above, it follows that \(A = A'\).
Proof of 2: we prove that, for \(j = 1, \ldots , k\), if \(t_j = (m, a, m') \in T\), then \(t'_j = (f(m), a, f(m')) \in T'\). From transition \(t_j\), we can derive the two processes \(\small P_j = (\underbrace{ C_1\rho | \cdots | C_1\rho }_{ {^{\bullet }t_j} (s_1) } | \cdots | \underbrace{ C_n\rho | \cdots | C_n\rho }_{ {^{\bullet }t_j} (s_n) })\) and \(\small P_j' = (\underbrace{ C_1\rho | \cdots | C_1\rho }_{ {t_j^{\bullet }} (s_1) } | \cdots | \underbrace{ C_n\rho | \cdots | C_n\rho }_{ {t_j^{\bullet }} (s_n)})\) such that \(f({^{\bullet }t_j}) = {\mathrm{dec}}(P_j)\) and \(f({t_j^{\bullet }} )= {\mathrm{dec}}(P_j')\). According to Definition 17, for each \(C_i = p_i\), we have a summand \(\small c_i^j\) in \(p_i\), with \(\small Q_j = (\underbrace{ c_1^j \rho | \cdots | c_1^j \rho }_{ {^{\bullet }t_j} (s_1) } | \cdots | \underbrace{ c_n^j \rho | \cdots | c_n^j \rho }_{ {^{\bullet }t_j} (s_n) })\). By inspecting the shape of \(t_j\) and the definition of the various \(c_i^j\)’s, one can get convinced that \(({\mathrm{dec}}(Q_j), l(t_j), {\mathrm{dec}}(P_j'))\) is a derivable transition. Hence, since each \(p_i\) is a summation containing the summand \(c_i^j\), also \(({\mathrm{dec}}(P_j), l(t_j), {\mathrm{dec}}(P_j'))\) is a derivable transition and belongs to \(T'\), as required.
Proof of 3: We prove that if \(t'_j = (m'_1, a, m'_2) \in T'\), then there exists a transition \(t_j = (m_1, a, m_2) \in T\) such that \(f(m_1) = m'_1\) and \(f(m_2) = m'_2\). This is proved by case analysis on the shape of the marking \(m'_1\).
If \(m_1'\) is a singleton, then \(m'_1 = \{p_i\rho \}\) for some \(i = 1, \ldots , n\), and so \(t'_j = \{p_i\rho \} {{{\,\mathop {\longrightarrow }\limits ^{a}}}} m_2'\). According to Definition 17, such a transition is derivable by the rules only if, among the many summands composing \(p_i\rho \), there exists a summand \(c^j_i \rho = a.\Pi _j\rho \), which is possible only if in \(N(m_0)\) we have a transition \(t_j\) with \({^{\bullet }t_j} = \{s_i\}\), \(f(\{s_i\}) = \{p_i\rho \}\), \(f({t_j^{\bullet }}) = {\mathrm{dec}}(\Pi _j\rho ) = m_2'\) and \(l(t_j) = a\), as required.
Otherwise, if \(m_1' = k_{1} \cdot p_1\rho \,\oplus \, \cdots \,\oplus \, k_n \cdot p_n\rho \) and i is the least index such that \(k_i > 0\), then in deriving transition \(t'_j = m_1' {{{\,\mathop {\longrightarrow }\limits ^{a}}}} m_2'\), one of the \(k_i\) processes \(p_i \rho \) acts as the leader of the synchronization, and all the other participants are servants. If \(k_i = 1\), then, by Definition 17, \(p_i\) has a summand \(c^j_i\) defined as \(\underbrace{ \underline{x}^j_{i+1}. \cdots . \underline{x}^j_{i+1}}_{k_{i+1}\, \mathrm{times}}. \cdots .\underbrace{ \underline{x}^j_{n}. \cdots .\underline{x}^j_{n}}_{k_n \, \mathrm{times}}.a_{j}.\Pi _{j}\), where \(\Pi _{j} = \underbrace{ C_1 | \cdots | C_1}_{h_1 \, \mathrm{times} } | \cdots | \underbrace{ C_n | \cdots | C_n}_{h_n \, \mathrm{times}}.\).
This summand \(c^j_i\) will synchronize with all the other components of \(m_1'\), as each other may only contribute with an action of the form \(\overline{x}^j_{k}\) for \(k = i+1, \ldots , n\), being the unique synchronizable summand of \(p_k\). Therefore, transition \(t'_j\) is possible only if transition \(t_j = (m_1 , a, m_2)\) is in T, where \(m_1 = k_{1} \cdot s_1 \,\oplus \, \cdots \,\oplus \, k_n \cdot s_n\), with \(f(m_1) = m_1'\), and \(m_2 = h_{1} \cdot s_1 \,\oplus \, \cdots \,\oplus \, h_n \cdot s_n\) is such that \(f(m_2) = \underbrace{ C_1\rho | \cdots | C_1\rho }_{h_1 \, times } | \cdots | \underbrace{ C_n\rho | \cdots | C_n\rho }_{ h_n \, times }\), as required. Similarly, if \(k_i \ge 2\), then \(p_i\) has a summand \(c^j_i\) defined as \({\overline{x}^j_{i}}.\mathbf{0}+ \underbrace{\underline{x}^j_{i}.{\cdots }. \underline{x}^j_{i}}_{k_i -1\, \mathrm{times}}. \underbrace{\underline{x}^j_{i+1}.{\cdots }. \underline{x}^j_{i+1}}_{k_{i+1}\, \mathrm{times}}.{\cdots }. {\underbrace{\underline{x}^j_{n}.{\cdots }. \underline{x}^j_{n}}_{k_{n}\, \mathrm{times}}.a_{j}.\Pi _{j}}\), such that the other \(k_i - 1\) instances of \(p_i\) can contribute to a synchronization with the first \(p_i\) by means of the summand \(\overline{x}^j_{i}.\mathbf{0}\) in \(c^j_i\). \(\square \)
Example 9
Function \(\mathrm{INet}(-)\) can be applied to any finite P/T net \(N(m_0)\). However, if \(N(m_0)\) is not statically reduced, the representability theorem does not hold. Let us consider the net \(N(\{s_1\}) = (\{s_1, s_2\}, \{a\},\)\(\{(s_1, a, \emptyset ), (s_2, a, \emptyset )\}, \{s_1\})\). Clearly such a net is not statically reduced because place \(s_2\) is not statically reachable from the initial marking. The finite-net multi-CCS term \(\mathrm{INet}(N(\{s_1\}))\) would be \({(\mathbf{\nu } L)}(C_1)\), where \(L = \{y_1, y_2\} \cup \{x^1_1, x^1_2, x^2_1, x^2_2\}\) and
but now Net\((\mathrm{INet}(N(\{s_1\})))\) is the net \((\{a.\mathbf{0}+ \mathbf{0}+ y_1.\mathbf{0}\}, \{a\},\)\(\{(a.\mathbf{0}+ \mathbf{0}+ y_1.\mathbf{0}, a, \emptyset )\}, \{a.\mathbf{0}+ \mathbf{0}+ y_1.\mathbf{0}\})\), which has one place and one transition only, i.e., it is isomorphic to the subnet of \(N(\{s_1\})\) statically reachable from the initial marking \(\{s_1\}\).
Remark 3
In the classic definition of Petri nets (see, e.g., [7, 30, 31]), the transition labeling is given with actions taken from a set A of unstructured actions; hence, our assumption that \(A \subseteq \mathcal {L} \cup \{\tau \}\) is in analogy with this tradition.
However, if we want to be more generous and consider Petri nets labeled over the set Act \( = \mathcal {L} \cup \overline{\mathcal {L}} \cup \{\tau \}\) of structured actions and co-actions, the extension of the representability theorem to this larger class of nets is not trivial. First of all, we note that the translation in Definition 17 is no longer accurate; consider the Petri net \(N(\{s_1, s_2\}) = (\{s_1, s_2\}, \{a, \bar{a}\}, \{(s_1, a, \emptyset ), (s_2, \bar{a}, \emptyset )\}, \{s_1, s_2\})\), then \(\mathrm{INet}(N(\{s_1, s_2\}))\) is \({(\mathbf{\nu } L)}(C_1 {\,|\,}C_2)\), with \(L = \{y_1, y_2\} \cup \{x^1_1, x^1_2, x^2_1, x^2_2\}\) and
but now Net\((\mathrm{INet}(N(\{s_1, s_2\})))\) contain also an additional synchronization transition \((\{a.\mathbf{0}+ \mathbf{0}+ y_1.\mathbf{0}, \mathbf{0}+ \bar{a}.\mathbf{0}+ y_2.\mathbf{0}\}, \tau , \emptyset )\), which has no counterpart in the original net \(N(\{s_1, s_2\})\). We conjecture that a possible solution is to be based on the introduction an additional operator in the language: the relabeling operator of CCS [25]—\([b_1/a_1, \ldots , b_n/a_n]\), which relabels each action \(a_i\) into \(b_i\)—to be used only at the top level. The procedure is as follows:
First, relabel each transition \(t_j\) of the original net \(N(m_0)\), labeled with an input action \(a_j\), to a new, not in use, input action \(a_j^j\), yielding a new renamed net \(N'(m_0)\).
Then, compute the associated process \(\mathrm{INet}(N'(m_0))\), according to Definition 17; note that in Net\((\mathrm{INet}(N'(m_0)))\) no additional synchronization transitions are introduced, because, by renaming, no pair of transitions in \(N'(m_0)\) are labeled with a matching pair of actions/co-actions.
Then, consider the process \(\mathrm{INet}(N'(m_0))[a_1/a_1^1, \ldots , a_k/a_k^k]\) and compute its associated net: it will be isomorphic to the original net \(N(m_0)\). \(\square \)
7 Conclusion
The class of finite-net multi-CCS processes represents a language for describing finite, statically reduced, P/T Petri nets. This is not the only language expressing finite P/T nets: the first (and only other) one is Mayr’s PRS [22], which however is rather far from a typical process algebra as its basic building blocks are rewrite rules (or net transitions) instead of actions and, for instance, it does not contain any scope operator like restriction.
A bit pretentiously, we claim that well-formed, finite-net Multi-CCS is the language for finite Petri nets. The main argument defending this claim is that the parallel operator \(- \parallel -\) of a language able to express Petri nets has to be
permissive: in a process \(p \parallel q\), the actions p can perform cannot be prevented by q. This requirement is necessary because P/T Petri nets are permissive as well, meaning that if a transition t is enabled at a marking m, then t is also enabled at a marking \(m' \supseteq m\); the parallel operator of Multi-CCS is permissive, while this is not the case for other parallel operators, such as the CSP one \(p \parallel _A q\) [20];
Moreover, the parallel operator \(- \parallel -\) is to be ACI (associative, commutative, with an identity), because the decomposition of a parallel process into a marking has to reflect that a marking is a (finite) multiset; also in this case, the parallel operator of Multi-CCS is ACI, while this is not the case for other parallel operators, notably the CSP one.
Moreover, the parallel operator should be able to express multi-party synchronization, because a net transition, which may have a preset of any size, can be generated by means of a synchronization among many participants, actually as many as are the tokens in its preset. The Multi-CCS parallel operator can model multi-party synchronization, by means of the interplay with the strong prefixing operator. Other process algebras offer parallel operators with multi-party synchronization capabilities, but in Multi-CCS multi-party synchronization is “programmable”, meaning that we can prescribe the order in which the various participants are to interact, independently of the syntactic position they occupy within the global term and without resorting to a global synchronization function, as in the case of some ACP dialects [2].
The multi-party synchronization discipline has been chosen as simple as possible: a sequence can synchronize with a complementary action at a time, in the exact order they occur in the sequence. About sequentialization operators, we note that prefixing cannot be replaced by ACP-like sequential composition, because a language with recursion and sequential composition can express all the context-free languages, while finite P/T nets cannot [19, 30]; hence, sequential composition is too powerful to express only finite P/T nets. As we have chosen a CCS-like naming convention, the scoping operator, which can occur syntactically only at the top level, is the CCS restriction operator.
Summing up, any other language, if any, able to represent all and only finite P/T Petri nets should possess these necessary features, which, altogether, seem to be exclusive of finite-net Multi-CCS, or that at least are very rare in the panorama of process algebras.
Our calculus is given a net semantics in terms of unsafe, finite P/T nets, improving over previous work. Degano et al. [8] and Olderog’s approach [28] is operational like ours, but somehow complementary in style, as it builds directly over the SOS semantics of CCS. Their construction generates safe P/T nets which are finite only for regular CCS processes (i.e., processes where restriction and parallel composition cannot occur inside recursion). On the contrary, here we give finite P/T net semantics to a calculus strictly larger than regular CCS, as parallel composition can occur in the body of recursively defined constants. Similar concerns are for PBC [4], whose semantics is given in terms of safe P/T nets only. Nonetheless, PBC can express multiway synchronization by means of its relabeling operators, and so, in principle, if equipped with an unsafe semantics, it might also serve as a language expressing all unsafe, finite P/T nets. The first paper defining a net semantics in terms of unsafe P/T nets is [13], where the approach is denotational and the considered language is limited to CCS without restriction. Our technique is somehow indebted to the earlier work of Busi and Gorrieri [5] on giving labeled net semantics to the \(\pi \)-calculus [26] in terms of P/T nets with inhibitor arcs; our solution simplifies their approach for finite-net Multi-CCS because we do not need inhibitors. In particular, already in that paper it is observed that finite-net \(\pi \)-calculus processes originate finite P/T net systems (with inhibitor arcs). Similar observations on the interplay between parallel composition and restriction in recursive definitions, in different contexts, has been done also by others, e.g., [1]. Also important is the work of Meyer [23, 24] in providing an unlabeled P/T net semantics for a fragment of the \(\pi \)-calculus; the main difference is that his semantics may offer a finite net representation also for some processes where restriction occurs inside recursion, but the price to pay is that the resulting net semantics may be incorrect from a causality point of view; for instance, in process \((\nu c) (a.c.\mathbf{0}{\,|\,}b.\bar{c}.\mathbf{0}) {\,|\,}(\bar{a}.\mathbf{0}{\,|\,}\bar{b}.\mathbf{0})\) the two synchronizations on a and b are causally dependent in his semantics.
Denotational net semantics for unsafe Petri nets are rare. Besides the work by Goltz [13] mentioned above, we know also of [3], where CSP [20] is given a denotational net semantics in terms of so-called open nets, a reactive extension of ordinary Petri nets, with the limitation that parallel composition is modeled by disjoint union and arc weight can only be 1. Future work will be devoted to define compositional (i.e., denotational in style) unsafe P/T net semantics for finite-net Multi-CCS, generalizing work of Goltz [13] and Taubner [33].
We conclude this overview of related literature by noting the differences of this paper with respect to its earlier version [18]. First, the definition of finite-net Multi-CCS is a bit simpler now, in order to capture the minimal language capable of representing all and only finite P/T nets. Second, the net Net(p) associated to a process p is statically reduced: this ensures that Net(p) and Net\((p{\,|\,}p)\) are the same unmarked net, but with a different initial marking; on the contrary, in [18] Net(p) was only dynamically reduced. Third, the finiteness theorem was wrongly stated in [18]: in fact, Net(p) is finite not for all finite-net processes, but only for well-formed finite-net processes. Fourth, the construction of the finite-net process \(p = \mathrm{INet}(N(m_0))\) from the finite P/T net system \(N(m_0)\) is inaccurate in [18], as Net(p) may have more transitions than \(N(m_0)\); as the previous construction used too few bound names, it was impossible to link precisely the tokens consumed by a transition to the actual place from which these tokens are to be consumed.
Finally, an open problem for future research. Compositional equivalence-checking on finite-state process algebras, such as regular CCS, is a viable technique because the used equivalence (typically, some form of bisimilarity over finite-state LTSs) is decidable and also a congruence for the operators of regular CCS. In desire of a similar technique for finite-net Multi-CCS, one has to find an equivalence relation which is decidable over finite P/T nets and a congruence for the operators of Multi-CCS. This is not easy. Let us examine three well-known equivalences over finite P/T nets: interleaving bisimilarity (Definition 7), step bisimilarity [27] and net isomorphism (Definition 5). On the one hand, only net isomorphism is decidable for finite P/T nets, while interleaving bisimilarity and step bisimilarity are undecidable [12, 21]. On the other hand, net isomorphism is not a congruence for \(+\): for instance, \(p = a.(\mathbf{0}+ \mathbf{0})\) and \(q = a.(\mathbf{0}+ \mathbf{0}+ \mathbf{0})\) are such that \(\mathrm{Net}(p) \cong \mathrm{Net}(q)\) (both nets have only two places and one transition), but Net\((p + p) \not \cong \mathrm{Net}(q + p)\), as Net\((p + p)\) is isomorphic to Net(p), while Net\((q + p)\) has three places and two transitions. Moreover, interleaving bisimilarity is not a congruence for Multi-CCS parallel composition [19], while step bisimilarity is a congruence for all the operators of Multi-CCS [19]. Summing up, none of these three equivalences satisfies both properties: being decidable and a congruence. Of course, if we restrict our attention to finite, bounded nets, the situation is much better and step bisimilarity can be used to this aim, being decidable and a congruence. However, for general, unbounded finite P/T nets it is a challenging open problem to find an equivalence relation which satisfies both properties.
Acknowledgments
The anonymous referees are thanked for their detailed comments and suggestions. Massimo Morara is thanked for pointing out the inaccuracy in the definition of the process \(\mathrm{INet}(N(m_0))\) in [18].
Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
