Taming Concurrency for Verification Using Multiparty Session Types (Technical Report)

Christoph Wagner; Kirstin Peters; Uwe Nestmann

REVIEW 3 major objections 6 minor 14 references

Taming Concurrency for Verification Using Multiparty Session Types (Technical Report)

T0 review · 3 major / 6 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves that every process well-typed against a multiparty session global type can be rewritten, following the global type's structure, into an interaction-free sequential program whose data evolution matches the original, making…

desk verdict A solid proof-rich companion to their ICALP paper, with a genuine sequentialisation result for well-typed MPST systems, but one load-bearing dependency relation is only described in prose. read the letter →

arxiv 1908.06510 v1 pith:YYOKVEXZ submitted 2019-08-18 cs.LO

Kirstin Peters , Christoph Wagner , Uwe Nestmann This is my paper · ORCID

classification cs.LO MSC 68Q8568Q6003B70

keywords multipartysessiontypesconcurrencyverificationsequentialisationglobalinteraction-freeabstractionoperationalcorrespondencedata-basedtermination

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Multiparty session types verify the communication structure of distributed processes cheaply, but they say nothing about the concrete values flowing through a run. This report claims that the global type of a well-typed system can be used as a schedule: a simple rewriting function sequentialises the system, replacing each communication by a variable assignment and erasing all interaction and name binders. The result, a sequential global process (SGP), is interaction-free, so its state space does not explode combinatorially over interleavings. The report proves that the rewriting always succeeds on well-typed systems and that the abstraction is correspondence-similar to the original, so data-dependent properties—such as whether a value-bounded loop terminates—can be checked on the abstraction instead. The intended benefit is that verification of such properties becomes significantly more efficient, and the report shows the whole pipeline through translation to the Spin model checker.

What carries the argument

The central object is the sequential global process (SGP), an interaction-free target language consisting of a vector of variables, assignments $\tilde x := \tilde e$, conditionals, recursion variables, and parallel composition over independent parts only. The carrying mechanism is the rewriting mapping $\text{SGP}'$ (Definitions 10 and 11), which consumes the global type's syntactic structure: communication becomes an assignment that updates the receiver's variables, session invitation becomes a silent $\tau$, recursion in the type becomes recursion in the SGP-process, and parallel global types become independent parallel branches. The work it does is to turn the already-verified communication structure into a schedule, so that the only remaining behaviour is the flow of data values.

What would settle it

Implement the mapping $\text{SGP}'$ together with the interaction type system described in Section 2.3, and search for a well-typed system with two interleaved sessions where the dependency relation claims a communication is independent but one of the two partners is actually blocked by a conditional waiting on a value from the other session; if the algorithm then gets stuck or produces an SGP-process whose data trace is not achievable by the original system, the central claim fails.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that a well-typed process $P$ w.r.t. a set of global types $\{(G_j,s_j)\}$ can be mapped by the algorithm $\text{SGP}^*(\{P\}, \{(G_j,s_j)\})$ to a process without any communication prefixes, restriction, or binders—only assignments, conditionals, recursion variables, and independent parallel composition. The mapping is guided by the structure of the global type: a communication prefix $r_1\to r_2:\{l_i\langle \tilde U_i\rangle.G_i\}_{i\in I}$ is resolved by unguarding the matching sender and receiver, substituting the receiver's variables with the sent expressions, and continuing with the chosen branch $G_m$. Theorem 2 establishes that the algorithm is defined and succeeds for every well-typed system; Theorems 3 and 4 establish that the abstraction is related to the original by reversed weak operational correspondence and hence by correspondence similarity, meaning every step of the abstraction can be matched by a completed sequence of steps of the original. The report also gives a simple translation of SGP-processes into Promela, so the interaction-free abstraction can be fed to Spin to verify properties that depend on concrete runs or values, such as data-based termination.

Load-bearing premise

The whole construction rests on the soundness of the adapted interaction type system that decides when one session's communication may depend on another's; the report specifies this adaptation only in prose, and if it misses a dependency the translation can fail to find the required communication partner.

Editorial extensions

If this is right

Well-typedness guarantees the translation always succeeds: Theorem 2 states that for every well-typed $P$, $\text{SGP}^*(\{P\},\{(G_j,s_j)\})$ is defined and returns an SGP-process.
Because the SGP-abstraction is correspondence-similar to the original, data-evolution properties that hold on the abstraction (and are preserved by the relation) hold on the original; the report uses this to verify termination and bid-limit properties of an auctioneer system.
Properties that depend on concrete runs or values—which are outside the scope of plain MPST—can be checked on the interaction-free abstraction, avoiding the state-space explosion caused by interleaving concurrent communications.
Under the condition that conditionals only choose between labels of an immediately following send, the translation is linear in the size of the system together with its global types (Corollary 1).
SGP-systems contain no interaction or binders, so checking them with a model checker like Spin has a dramatically smaller state space; the report demonstrates the verification of six LTL properties on the auctioneer example.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The same trick should transfer to choreographic programming: since a global type completely fixes the communication structure, any implementation language for which well-typedness is decidable can in principle be compiled to a sequential data-flow program, making the approach a general verification strategy rather than a single algorithm.
The dependence on the prose-adapted interaction type system suggests that the theorems' practical scope is not yet settled: a proof or mechanisation of that dependency relation would turn the central statement from conditional on an informal argument to a fully verified result.
One can test the boundaries of the method by moving to asynchronous communication; the sequentialisation would then need to represent message queues as data structures, and it is not obvious that the correspondence-similarity result would survive unchanged.
The reported worst-case exponential blow-up for general conditionals means the efficiency claim is strongest for conditionals that only choose between sender labels; for other conditionals the translation itself may be the bottleneck.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Colleague — this is worth reading if you work on MPST-based verification. The core idea is simple and new as far as I can tell: take a system well-typed against a global type, walk the type, and replace each communication with a value update, producing an interaction-free SGP process that still tracks data flow. Theorems 2–4 are the heart: totality of SGP' plus a reversed weak operational correspondence / correspondence similarity between original and abstraction. The proofs are detailed and mostly convincing. They also give a small auction example and a Promela/Spin translation, plus a Needham-Schroeder sketch. The self-citation to their ICALP companion [13] is appropriate; this report supplies the proofs the ICALP version omits.

The soft spot is exactly where the reader and stress-test point. For interleaved sessions, totality rests on 'globally progressing' defined via an interaction type system from Bettini et al. [2], adapted in prose: dependencies must be collected for senders and invitations too. No formal rules for the adaptation, no definition of the dependency relation. Lemmas 16 and 19 and the recursion case in Theorem 2 all invoke independence conditions that can't be checked from the text. If that adaptation is unsound, SGP' can get stuck on a well-typed system. This is a real gap, but it is localized: the single-session version (Definition 10) and the correspondence theorems don't depend on that informal machinery. Also, the abstract claims efficient verification of data-dependent properties, but there is no empirical baseline and no theorem stating which properties are preserved by reversed weak correspondence. The recursion-case proof has an asserted existence of well-typed subprocesses without a full argument. These are fixable: formalize the adapted dependency typing, prove the recursion case, state and prove a property-preservation lemma, add a small benchmark.

Bottom line: this deserves a serious referee. Not desk-reject material. I would send it to a session-types or concurrency-theory reviewer, with instructions that the interleaved-session totality proof is the load-bearing part. I'd probably not cite it myself in the next year unless I was working on MPST verification, but it is a legitimate contribution and the main gap is repairable rather than fatal.

Referee Report

3 major / 6 minor

Summary. The paper defines a sequentialisation mapping SGP' that transforms well-typed multiparty session processes into interaction-free 'sequential global processes' (SGP-systems), guided by the structure of the global types. The central technical claims are Theorem 2 (totality: every well-typed process with respect to a set of global types is mapped to an SGP-process), Theorem 3 (the abstraction introduces no new behaviour), and Theorem 4 (every step of the original process can be completed to a sequence simulated by the abstraction). From these, the paper derives reversed weak operational correspondence and correspondence similarity between the original system and its abstraction. The report also contains a detailed proof of standard MPST properties for the single-session fragment, a Promela translation of SGP-systems, and two case studies: an auctioneer protocol and a Needham-Schroeder inspired example.

Significance. If the central theorems hold, the paper provides a principled method for reusing MPST well-typedness to reduce verification of data-dependent properties of concurrent systems to verification of interaction-free sequential programs. The single-session typing system is fully specified, and the auxiliary lemmas for each case of the mapping are proven in detail by structural induction, which is a solid foundation. The work is also refreshingly concrete: it gives a Promela translation and demonstrates the approach on a non-trivial example. The main caveat is that the extension to interleaved sessions relies on an interaction type system from [2] that is adapted in prose rather than formally defined; this is load-bearing for the totality and correspondence theorems. The paper does not claim any numerical fitting or parameter tuning, and the proofs are presented transparently.

major comments (3)

[Section 2.3 after Definition 9; Lemmas 16 and 19; Theorem 2] The dependency relation for synchronous communication is never formally defined. The text states that, compared to [2], 'we have to consider dependencies also for senders' and 'extend the collection of dependencies also to session invitations', but no adaptation of the typing rules or a formal definition of 'depends on' is given. Lemmas 16 and 19 and the proof of Theorem 2 rely crucially on the conditions 'this communication does not depend on another session' and 'this session initialisation does not depend on another session'. Without a formal relation, these conditions cannot be checked, and the totality proof for interleaved sessions is incomplete: if the synchronous adaptation of [2] is unsound, there may be well-typed processes for which no case of Definition 11 applies. Please provide the formal dependency relation, the adapted interaction typing rules, and proofs that the lemmas use only non-dependent communications.
[Theorem 2, recursion case (Section 3, 'Case of Gl = (μtl) G′l')] The proof of the recursion case asserts that 'there are P′i such that {P′i}i∈I is well-typed w.r.t. {(G′j, sj)}j∈J' and then asserts the equality SGP'({Pi}, {(G′j, sj)}) = SGP'({P′i}, {(G′j, sj)}). No construction of P′i is given, and the equality is not proved. This step is load-bearing because Case 8 applies to the unfolded global types while the process still contains recursion binders, and the proof needs to show that the mapping ignores the unneeded remainder of the process. Please supply the missing induction argument or a separate lemma that justifies the existence of P′i and the stated equality.
[Theorems 3 and 4 proofs] The proofs of Theorems 3 and 4 repeatedly invoke 'Theorem 1 of [13]' without stating it. Since this document is intended as the technical report providing the proofs for [13], the correspondence results are not self-contained: the definition of SGP* and its basic property used in the simulation arguments are not included here. Please state or prove the needed theorem in this report, or explicitly reference where it is proved.

minor comments (6)

[Lemma 21, Par-L case] The proof says 'By Theorem 5 and Figure 2' but the referenced result appears to be Lemma 5 (Subject Reduction). Please correct the cross-reference.
[Lemma 16 proof] In the sentence 'Γ ⊢ Qn {˜xn@sl[r2]/˜xn} ⊲ s[r2] : Gn ↾ r2', the type should be sl[r2] : Gl,n ↾ r2, not 'Gn ↾ r2'; please fix the notation so that the session channel and the global type continuation are unambiguous.
[Section 3, discussion after Definition 11, Case 7a] The sentence 'session invitations under recursion introduce only a single session w.r.t. well-typedness' is unclear; please elaborate on how recursive process definitions interact with session initialisation in the counting argument.
[Example 1] The resulting SGP-process is displayed as 'τ.if x1 > 5 then x2 := 42...' but the vector of variables for this SGP-system is not stated. Please add the vector, e.g. ⟨(x1, x2, x3, x4); S⟩, to make the example self-contained.
[Section 4.3, discussion of Property P3] The sentence 'bA is neither equal to bB2 (unless incB2 = 0) nor equal to bB2' repeats 'bB2'; the second occurrence should presumably be 'bB1'. Please fix the type.
[General] The manuscript contains several formatting artifacts (e.g., broken mathematical spacing, missing semicolons in Promela code, and unlabeled cases in Definition 10). These should be cleaned up in the final version, and the cases of Definitions 10 and 11 should be numbered consistently for easier reference.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the abstraction and its correctness proofs are self-contained; the main risk is an unformalized dependency adaptation from Bettini et al., which is a proof gap, not circularity.

full rationale

The report's central derivation—SGP' maps every well-typed system to an interaction-free abstraction and Theorems 2–4 relate it to the original by reversed weak operational correspondence—is proved in the report itself from the typing rules of Figure 2, projection (Definition 3), and the reduction semantics of Figure 1. No fitted parameter is renamed as a prediction, and no definition presupposes the result it is used to prove. The references to the authors' companion ICALP paper [13] concern theorems whose proofs are reproduced here (e.g., Theorem 2 of [13] is proved after Lemma 19; Theorem 1 of [13] is obtained as a special case of Lemma 5). The appeal to [12] for the transfer to correspondence similarity is an external criterion and is not needed for the main simulation theorems. The weakest point is the adaptation of Bettini et al.'s interaction type system to synchronous communication and session invitations, which is described only in prose in Section 2.3 and used in Lemmas 16 and 19; if that adaptation is unsound, the totality proof of Theorem 2 would have a gap. That is a correctness risk—not a circular derivation—so the circularity score is 0.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The central claim rests on the standard MPST framework (projection, typing rules, coherence) and on the interaction type system of [2] for global progress. The paper introduces no free parameters and no invented entities; the SGP-system is a defined syntactic artifact, not an unexplained postulate.

assumptions (3)

domain assumption Interaction type system of Bettini et al. [2], adapted to synchronous communication and session invitations, correctly captures global progress and dependency for interleaved sessions.
The adaptation is described in prose in Section 2.3 (after Definition 9); Lemmas 16, 17, 19 and the proof of Theorem 2 rely on it to ensure that communication partners can be unguarded in a suitable order.
ad hoc to paper No alpha-conversion is used to rename input binders during sequentialisation.
Stated before Lemma 20; the mapping's output can change under such renaming, so the equivalence and correspondence results are restricted to reduction sequences that avoid it.
domain assumption Well-typed processes are role-distributed, coherent, and globally progressing per Definitions 8 and 9.
This defines the input class of the method and is inherited from MPST theory [1,2,8]; the whole algorithm presupposes it.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Taming Concurrency for Verification Using Multiparty Session Types (Technical Report)." pith.science (2026). https://pith.science/paper/YYOKVEXZ

@misc{pith2026190806510,
  author       = {Pith},
  title        = {Pith review of: Taming Concurrency for Verification Using Multiparty Session Types (Technical Report)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YYOKVEXZ}},
  note         = {Machine review of arXiv:1908.06510}
}

read the original abstract

The additional complexity caused by concurrently communicating processes in distributed systems render the verification of such systems into a very hard problem. Multiparty session types were developed to govern communication and concurrency in distributed systems. As such, they provide an efficient verification method w.r.t. properties about communication and concurrency, like communication safety or progress. However, they do not support the analysis of properties that require the consideration of concrete runs or concrete values of variables. We sequentialise well-typed systems of processes guided by the structure of their global type to obtain interaction-free abstractions thereof. Without interaction, concurrency in the system is reduced to sequential and completely independent parallel compositions. In such abstractions, the verification of properties such as e.g. data-based termination that are not covered by multiparty session types, but rely on concrete runs or values of variables, becomes significantly more efficient.

Figures

Figures reproduced from arXiv: 1908.06510 by the authors.

**Figure 1.** Reduction Semantics of the Session Calculus. expressions e and conditions c to functions that are known by Promela, the input language of Spin. Promela captures a wide range of functions such as basic logical and arithmetical operators. With P1 | P2 the processes P1 and P2 are composed in parallel. Successful termination is denoted by 0. With (νs)P we restrict the scope of the session channel s to P. With (µX) P we … view at source ↗

**Figure 2.** Typing Rules. that the continuation P behaves as specified by the projection of G to role 1 in the session environment. Rule Acc is similar for a process that accepts to participate as role r in the invited session. Rule Send checks whether the process sends if its local type requires this, the roles of the process and the local type match, the transmitted label is one of the labels specified in the local type by j … view at source ↗

**Figure 3.** Reduction Rules of Global Types. P 7−→ P ′ = (ν˜s)(P ′ 1 | P2), where we do not alpha-convert input bounded names. By the Lemmata 5, 12, and 13, then P ′ is well-typed w. r. t. G ′ = G ′ 1 ∪ G′ j ,sj j∈J2 . By Definition 11 and Theorem 1 of [13], then SGP∗ ({P ′} , G ′ ) ≡S S ′ . Case of Rule If-T: In this case we have S = hV; if c then S1 else S2i and S ′ = hV; S1i. By Definition 11, then P ≡ (ν˜s)(if c then P1 … view at source ↗

Figures from the paper (3 more)

**Figure 4.** Figure 4: Promela Implementation preamble a c t i v e p r o c t yp e Model ( ) { atom i c { s e l e c t ( in cB1 : 1 . . 1 0 ) ; s e l e c t ( in cB2 : 1 . . 1 0 ) ; s e l e c t (maxB1 : 5 0 . . 1 0 0 ) ; s e l e c t (maxB2 : 5 0 . . 1 0 0 ) ; } s k i p ; bA = in cB1 + 0 ; bB2 =…

**Figure 5.** Figure 5: Promela Implementation of the Auctioneer System implementation and verification of the LTL-Formula that specify the properties we want to check. We provide in [13] an algorithm for the translation of SGP-processes into Promela but expect that the desired properties are…

**Figure 6.** Figure 6: Promela LTL Formulae 4.3 Analysing the Properties of Implementations Finally, the developer has to add to the Promela program the LTL-formula for the properties that he or she is interested in. We add the following six LTL-formulae, where [PITH_FULL_IMAGE:figures/full…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

14 extracted references · 4 canonical work pages

[13]

In: Proceedings of ICALP (2019), to appear

Peters, K., Wagner, C., Nestmann, U.: Taming Concurrenc y for Veriﬁcation Using Multiparty Session Types. In: Proceedings of ICALP (2019), to appear

work page 2019
[2]

In: Proceedin gs of CONCUR

Bettini, L., Coppo, M., D Antoni, L., De Luca, M., Dezani-C iancaglini, M., Yoshida, N.: Global Progress in Dy- namically Interleaved Multiparty Sessions. In: Proceedin gs of CONCUR. LNCS, vol. 5201, pp. 418–433 (2008). https://doi.org/10.1007/978-3-540-85361-9 33

doi:10.1007/978-3-540-85361-9 2008
[1]

Electronic Notes in Theoretical Computer Science 241, 3–33 (2009)

Bejleri, A., Yoshida, N.: Synchronous Multiparty Sessio n Types. Electronic Notes in Theoretical Computer Science 241, 3–33 (2009). https://doi.org/10.1016/j.entcs.2009.06.002 32 K. Peters, C. Wagner, and U. Nestmann

work page doi:10.1016/j.entcs.2009.06.002 2009
[3]

In: Proceedings of FORTE

Bocchi, L., Chen, T.C., Demangeon, R., Honda, K., Yoshida , N.: Monitoring networks through multiparty session types. In: Proceedings of FORTE. pp. 50–65. No. 7892 in LNCS ( 2013). https://doi.org/10.1007/978-3-642-38592-6 5

work page doi:10.1007/978-3-642-38592-6 2013
[4]

In: Proceedings of CONCUR

Demangeon, R., Honda, K.: Nested Protocols in Session Typ es. In: Proceedings of CONCUR. LNCS, vol. 7454, pp. 272–286 (2012). https://doi.org/10.1007/978-3-642-32940-1 20

doi:10.1007/978-3-642-32940-1 2012
[5]

Information and Computation 208(9), 1031–1053 (2010)

Gorla, D.: Towards a Uniﬁed Approach to Encodability and S eparation Results for Process Calculi. Information and Computation 208(9), 1031–1053 (2010). https://doi.org/10.1016/j.ic.2010.05.002

doi:10.1016/j.ic.2010.05.002 2010
[6]

Prentice Hall (1991)

Holzmann, G.J.: Design and Validation of Computer Protoc ols. Prentice Hall (1991)

work page 1991
[7]

IEEE Transaction s on software engineering 23(5), 279–295 (1997)

Holzmann, G.J.: The model checker SPIN. IEEE Transaction s on software engineering 23(5), 279–295 (1997). https://doi.org/10.1109/32.588521

doi:10.1109/32.588521 1997

Show all 14 references

[8]

In: Proceedings of POPL

Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchro nous Session Types. In: Proceedings of POPL. vol. 43, pp. 273–284. ACM (2008). https://doi.org/10.1145/1328438.1328472

2008
[9]

Journal of the ACM (JACM) 63(1) (2016)

Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchro nous Session Types. Journal of the ACM (JACM) 63(1) (2016). https://doi.org/10.1145/2827695

2016 doi
[10]

Information and Computation 100(1), 1–77 (1992)

Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile P rocesses. Information and Computation 100(1), 1–77 (1992). https://doi.org/10.1016/0890-5401(92)90008-4

1992 doi
[11]

In: Proceedings of CONCUR

Parrow, J., Sj¨ odin, P.: Multiway synchronization veri ﬁed with coupled simulation. In: Proceedings of CONCUR. pp. 518–533. No. 630 in LNCS (1992). https://doi.org/10.1007/BFb0084813

1992 doi
[12]

In: Proceedings of EXPRESS/SOS

Peters, K., van Glabbeek, R.: Analysing and Comparing En codability Criteria. In: Proceedings of EXPRESS/SOS. EPTCS, vol. 190, pp. 46–60 (2015). https://doi.org/10.4204/EPTCS.190.4

2015 doi
[14]

In: Proceedings of FoSS aCS

Yoshida, N., Deni´ elou, P.M., Bejleri, A., Hu, R.: Parameterised Multiparty Session Types. In: Proceedings of FoSS aCS. LNCS, vol. 6014, pp. 128–145 (2010). https://doi.org/10.1007/978-3-642-12032-9 10

2010 doi

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [13]

In: Proceedings of ICALP (2019), to appear

Peters, K., Wagner, C., Nestmann, U.: Taming Concurrenc y for Veriﬁcation Using Multiparty Session Types. In: Proceedings of ICALP (2019), to appear

work page 2019

[2] [2]

In: Proceedin gs of CONCUR

Bettini, L., Coppo, M., D Antoni, L., De Luca, M., Dezani-C iancaglini, M., Yoshida, N.: Global Progress in Dy- namically Interleaved Multiparty Sessions. In: Proceedin gs of CONCUR. LNCS, vol. 5201, pp. 418–433 (2008). https://doi.org/10.1007/978-3-540-85361-9 33

doi:10.1007/978-3-540-85361-9 2008

[3] [1]

Electronic Notes in Theoretical Computer Science 241, 3–33 (2009)

Bejleri, A., Yoshida, N.: Synchronous Multiparty Sessio n Types. Electronic Notes in Theoretical Computer Science 241, 3–33 (2009). https://doi.org/10.1016/j.entcs.2009.06.002 32 K. Peters, C. Wagner, and U. Nestmann

work page doi:10.1016/j.entcs.2009.06.002 2009

[4] [3]

In: Proceedings of FORTE

Bocchi, L., Chen, T.C., Demangeon, R., Honda, K., Yoshida , N.: Monitoring networks through multiparty session types. In: Proceedings of FORTE. pp. 50–65. No. 7892 in LNCS ( 2013). https://doi.org/10.1007/978-3-642-38592-6 5

work page doi:10.1007/978-3-642-38592-6 2013

[5] [4]

In: Proceedings of CONCUR

Demangeon, R., Honda, K.: Nested Protocols in Session Typ es. In: Proceedings of CONCUR. LNCS, vol. 7454, pp. 272–286 (2012). https://doi.org/10.1007/978-3-642-32940-1 20

doi:10.1007/978-3-642-32940-1 2012

[6] [5]

Information and Computation 208(9), 1031–1053 (2010)

Gorla, D.: Towards a Uniﬁed Approach to Encodability and S eparation Results for Process Calculi. Information and Computation 208(9), 1031–1053 (2010). https://doi.org/10.1016/j.ic.2010.05.002

doi:10.1016/j.ic.2010.05.002 2010

[7] [6]

Prentice Hall (1991)

Holzmann, G.J.: Design and Validation of Computer Protoc ols. Prentice Hall (1991)

work page 1991

[8] [7]

IEEE Transaction s on software engineering 23(5), 279–295 (1997)

Holzmann, G.J.: The model checker SPIN. IEEE Transaction s on software engineering 23(5), 279–295 (1997). https://doi.org/10.1109/32.588521

doi:10.1109/32.588521 1997