Pith. sign in

REVIEW 3 major objections 5 minor 37 references

Justness: A Completeness Criterion for Capturing Liveness Properties

T0 review · 3 major / 5 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 Justness becomes a precise, syntax-directed liveness criterion for CCS, ABC, and CCSS.

desk verdict Solid, careful formalization of justness for CCS and extensions; the load-bearing Lemma 6 is the one soft spot worth checking before relying on the closure property. read the letter →

arxiv 1909.00286 v2 pith:WB32IYXL submitted 2019-08-31 cs.LO

Rob van Glabbeek This is my paper · ORCID
classification cs.LO MSC 68Q8568Q60
keywords justnesslivenesscompletenesscriterionconcurrencyrelationprocessalgebraCCSbroadcastcommunicationsignals
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

The paper argues that a transition system only becomes a model of a distributed system once we decide which paths count as complete runs. It advocates justness as the right completeness criterion: stronger than progress, weaker than fairness, and warranted by default rather than assumed. The paper's technical contribution is a concurrency relation between transitions, built from 'synchrons'—paths in derivation trees—defined for CCS and its extensions with broadcast communication and signals. With that relation, justness becomes a precise, syntax-directed predicate on paths, and the paper proves it is feasible, meaning every finite path extends to a just path, and that five different formulations all define the same just paths.

What carries the argument

The load-bearing object is the synchron: a string of operator arguments leading from the root of a process to an atomic, unguarded subexpression, representing one leaf of a transition's derivation tree. Each transition derivation carries a set of necessary synchrons—all of them, except for broadcasts, where only the sending synchron is necessary. Two synchrons are concurrent when they sit on opposite sides of a parallel composition under the same prefix; the concurrency relation t ⌣ u holds when no active synchron of u interferes with a necessary synchron of t. This relation, extended to future variants, satisfies closure property (2), which is exactly what lets every finite path be extended to a just path.

What would settle it

Exhibit a transition pair t,u such that the synchron test says t is unaffected by u, yet performing u in the source state of t destroys every possible future variant of t through a conflict located below a static operator, such as a shared restriction \L that the synchron test ignores. A concrete search over small CCS processes for such a pair would settle whether the synchron-based concurrency relation faithfully captures interference: if one exists, the definition of justness classifies some genuinely blocked path as complete.

Watch

Extended reading notes

Core claim

The central discovery is that an asymmetric concurrency relation—'transition u does not interfere with t'—can be defined compositionally for CCS, ABC, and CCSS by treating transitions as derivation trees and locating the atomic leaves, called synchrons, that a transition synchronises. A non-blocking transition is then just if, whenever it becomes enabled, eventually some transition occurs that interferes with one of its necessary synchrons. The paper proves this definition satisfies the closure property needed for feasibility (Corollary 3 with Theorem 1), shows that static and dynamic component versions give the same justness (Theorem 2), and proves agreement with the earlier coinductive definitions of justness for CCS, ABC, and CCSS (Theorems 3, 4, and Propositions 13–15).

Load-bearing premise

The load-bearing premise is that all real interference between transitions is visible in the shape of their derivation trees: two transitions are concurrent exactly when their synchrons sit on opposite sides of a parallel composition, and if two transitions can interfere without sharing such a syntactic position, justness will call some stuck runs complete and some live runs incomplete.

Editorial extensions

If this is right

  • For CCS, ABC, and CCSS, justness is now a fully syntax-directed completeness criterion, not an informal slogan: it can be checked on individual paths.
  • Every finite path can be extended to a B-just path, even in CCS with infinitary choice, so liveness properties verified under justness are not vacuous.
  • The five candidate definitions—synchron-based, dynamic components, static components, and the two component variants—all induce the same set of just paths, so any of them may be used in proofs or tools.
  • The new definition agrees with the earlier coinductive justness of [16] and [7], so existing examples and verification results for mutual exclusion and broadcast protocols carry over unchanged.
  • Because broadcast reception is treated as a blocking action and broadcasts as non-blocking, justness yields faithful liveness guarantees for reactive systems where progress is too weak.

Reading between the lines

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

  • The synchron/derivation-tree method will likely transfer to other process algebras whose structural operational semantics fits the same rule format; the main design choice is deciding which operators count as static.
  • If justness is accepted as the default completeness criterion, liveness verification could model-check against just paths instead of fair paths, yielding stronger guarantees that do not assume away real interference.
  • A testable extension: instrument an implementation of CCS to record derivation-tree identities at runtime, then compare the paths the definition calls just against actual blocked runs in a distributed environment, especially under broadcast and signal extensions.
  • The asymmetry of the concurrency relation suggests a hierarchy of justness for broadcast systems: sends can ignore receivers, but receives depend on senders, which may explain why broadcast protocols often need weaker liveness assumptions than handshake-based protocols.
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.

Referee Report

3 major / 5 minor

Summary. The paper makes the completeness criterion of justness — intermediate between progress and fairness — available for the transition systems of CCS and its extensions with broadcast communication (ABC) and signals (CCSS). The earlier concurrency-relation-based definition of justness from [18] is turned into a concrete construction: the paper represents transitions as derivation trees, decomposes them into 'synchrons' (paths from root to leaf), and defines a concurrency relation ⌣• from synchron structure (Section 6, Definitions 10–12). The main results are: closure property (2) holds (Corollary 3), so the construction is an LTSC; B-justness is feasible (Theorem 1 with Section 10); dynamic and static component-based concurrency relations give the same justness (Theorem 2); and the concurrency-based justness coincides with the coinductive definitions of [16] and [7] (Theorems 3 and 4, Propositions 13–15). Section 13 lifts the results to abstract paths, recovering the original justness notions of [16, 7, 3].

Significance. If the construction is sound, this is a substantive contribution: it replaces the coinductive, operator-by-operator definitions of justness for ABC and CCSS with a uniform, syntax-directed concurrency relation, proves feasibility, and shows agreement with the earlier formalisations. The paper's strengths include the detailed theorem chain from closure property (2) to feasibility and equivalence; the honest v2 correction in footnote 5, which records and fixes a real type error in Propositions 11 and 12; the informative comparison of dynamic versus static components and of the dynamically sequential fragment (Sections 7–8); and the fact that the agreement theorems relate to independently defined prior notions rather than being circular. The principal limitation is that the adequacy of the synchron model of interference is an axiom: the equivalence results compare two versions of the same construction and presuppose closure property (2), so they cannot by themselves validate the claim that derivation-tree shape captures all interference.

major comments (3)
  1. [§6 (Lemma 6; Proposition 6; Corollary 3)] The proof of Lemma 6 is a sketch at the most load-bearing step of the paper: closure property (2), which turns the construction into an LTSC and makes Theorem 1 applicable, depends on Proposition 6, whose key step is Lemma 6. The assertion that the marking of deleted dynamic nodes is consistent is stated in prose rather than derived, and the treatment of altered broadcast partners consists of a single sentence. In view of footnote 5, which reports that an earlier version of exactly this synchron machinery contained a subtle type error, I ask for a complete proof of Lemma 6: an inductive definition of the deletion operation on derivation trees, a proof that all necessary synchrons of the same derivation agree on which dynamic nodes are deleted, and a full case analysis for receptive and discarding partners in broadcast communications. Since this is decidable on finite processes, an exhaustive check of closure property (2) on a bounded signature would also settle the correctness risk; I found no concrete counterexample.
  2. [§6 (Definition 14; Observation 1)] Two auxiliary steps of Proposition 6 are asserted without proof. First, Definition 14 chooses the active synchron of u that is 'closest' to ς without proving uniqueness; uniqueness does hold, because two distinct active synchrons of one derivation diverge at a first argument, so a single synchron ς can match at most one of them, but the argument should be spelled out. Second, Observation 1 ('if ς∈ς(P) and ς ⌣•d u with source(u)=P, then ς@u∈ς(target(u))') is the exact step that transfers a synchron into the target state's synchron set, and it is stated without proof; it needs a short structural induction on u, including the broadcast case in which the receiver side of u may change. Both points are load-bearing for Proposition 6 and hence for Corollary 3.
  3. [§6 (Definitions 10–12) and §§12–13] The central modelling axiom of the paper is that interference between transitions is captured exactly by the relative syntax of their derivation trees: concurrency is defined by where synchrons sit under parallel operators (Definitions 10 and 12), and the static and dynamic components of Section 7 inherit this shape. The equivalence theorems (Theorems 2–4, Proposition 13) compare versions of the same construction and presuppose closure property (2), so they cannot detect a failure of this premise. If two transitions interfere semantically without sharing a static operator position in their derivation trees, the criterion will classify some non-runs as complete or some runs as incomplete. I found no concrete counterexample; nevertheless, because this is the fragile premise of the whole development, I would welcome a test against an independent semantic model, for example an exhaustive finite-state validation of closure property (2) on a bounded signature, or a comparison with the Petri net or event structure semantics cited in Section 8.
minor comments (5)
  1. [§5.4 (Table 4)] In Table 4, the rule for agent identifiers (P s̄−→P′ implies A s̄−→A) is surprising at first reading because the target is A rather than P′; a sentence explaining the persistent-signal reading, consistent with the self-loop Pˆs s̄−→Pˆs, would remove potential confusion.
  2. [§13 (Theorem 4)] The 'Only if' direction of Theorem 4 is delegated to [16, Proof of Proposition E.4], which is a technical report rather than a published article; since Theorem 4 is one of the headline agreement results, the proof should be included or summarised in the main text so that the journal version is self-contained.
  3. [§6 (Figure 1)] Figure 1's caption does not name Classes I–V or indicate which regions represent indicator transitions; the text introduces these labels only after the figure, so annotating the caption with the class names would help the reader.
  4. [§10] The extension to the infinitary choice operator in Section 10 is described in a few sentences, and the argument that the relevant ≡-equivalence classes are countable is compressed; adding the synchron clause for the new argument ∑j, alongside the existing clauses for +L and +R, would make the adaptation precise.
  5. [§7.3 (after Example 8)] The sentence after Example 8 ('it follows also that ⌣•c is incomparable with ⌣•') combines Example 8 with the earlier observation that some ⌣•-concurrent pairs are not ⌣•c-concurrent; stating this combination explicitly would aid readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the synchron-based concurrency relation is a genuinely new construction, and the agreements with the earlier coinductive definitions are proven equivalences rather than fitted inputs.

full rationale

The derivation chain is self-contained: synchrons (Definitions 8-14) define a concurrency relation ⌣• from the parse-tree shape of derivations, Properties (4)-(7) are proved as Propositions 3-5 and Proposition 6, and Corollary 3 derives the LTSC closure property (2). The later equivalence results (Theorems 2-4, Propositions 10 and 13) relate this synchron-based relation to independently defined component-based and coinductive notions from [16] and [7]; they are proven equivalences between distinct formalisms, not a prediction forced by construction. No parameter is fitted to a dataset, and no equation is assumed as its own conclusion. The main caveats are correctness issues rather than circularity: Lemma 6's deletion argument ('this marking of deleted nodes is consistent ... actually deleting the indicated nodes ... yields another derivation') is asserted in prose, and Proposition 5 gestures at 'changing some receptive or discarding partners in a broadcast communication'; these are the most load-bearing unverified steps, but they are proof gaps, not reductions to inputs. Footnote 5 discloses that an earlier version had a type error making Propositions 11 and 12 incorrect; this is a transparency note and does not make the current argument circular. Self-citations to [11,16,18,7] supply the concept and prior formalisations of justness, but the present construction and its proofs do not rely on those citations as their justification.

Assumptions & free parameters 0 free parameters · 4 assumptions · 2 invented entities

The ledger is clean of fitted numerical parameters. The axioms are mostly domain assumptions about how transition systems model liveness and how the environment can block actions; the one ad hoc element is the synchrons-based modelling of interference. Invented entities are internal mathematical devices with no independent evidence.

assumptions (4)
  • domain assumption Atomic actions always terminate.
    Section 2 adopts this as a partial completeness criterion; all paths and the justness definition inherit it. If atomic actions could be interrupted mid-execution, the liveness analysis would not apply.
  • domain assumption Transition systems require an external completeness criterion to model distributed systems.
    Section 1 poses this as the foundation; it justifies the entire project but is not proven.
  • ad hoc to paper Interference between transitions is exactly captured by the relative syntax of their derivations (synchrons).
    Section 6, Definitions 9-12 and Section 7. This is the load-bearing modelling choice behind the concurrency relation.
  • domain assumption Broadcast receptions are always blockable by the environment.
    Section 5 sets Rec:=B? for ABC/ABCd; all blocking sets B contain Rec. This is a semantic decision about the environment.
invented entities (2)
  • Synchrons
    purpose: Combinatorial representations of leaves in derivation trees, used to define future variants and the concurrency relation between transitions (Section 6).
    Internal construction with no empirical or external falsifiable handle; it is validated only by coherence and equivalence proofs.
  • Static and dynamic components
    purpose: Abstracted representations of synchrons used to give alternative characterizations of concurrency and to satisfy closure property (3) (Section 7).
    Internal bookkeeping devices; no independent evidence outside the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Justness: A Completeness Criterion for Capturing Liveness Properties." pith.science (2026). https://pith.science/paper/WB32IYXL

@misc{pith2026190900286,
  author       = {Pith},
  title        = {Pith review of: Justness: A Completeness Criterion for Capturing Liveness Properties},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WB32IYXL}},
  note         = {Machine review of arXiv:1909.00286}
}
read the original abstract

This paper poses that transition systems constitute a good model of distributed systems only in combination with a criterion telling which paths model complete runs of the represented systems. Among such criteria, progress is too weak to capture relevant liveness properties, and fairness is often too strong; for typical applications we advocate the intermediate criterion of justness. Previously, we proposed a definition of justness in terms of an asymmetric concurrency relation between transitions. Here we define such a concurrency relation for the transition systems associated to the process algebra CCS as well as its extensions with broadcast communication and signals, thereby making these process algebras suitable for capturing liveness properties requiring justness.

Figures

Figures reproduced from arXiv: 1909.00286 by the authors.

Figure 1
Figure 1. Indicators and transitions In classical process algebra, and in Section 5, a transi￾tion is a formula of the form P ` −→ Q. The CCS process P = A|(c¯+τ) for instance, where the agent identifier A has the defining equation A def = c.A, has 3 outgoing tran￾sitions: P c −→ P, P c¯ −→ A|0 and P τ −→ A|0. The last of these transitions can be derived in two different ways: through a synchronisation between c and ¯c, or th… view at source ↗
Figure 2
Figure 2. Overview of the various notions of justness defined in this paper Proof: “If”: It suffices to show that the family of predicates B-justness on abstract paths according to Definition 22 satisfies the five requirements of Definition 20. This is straightforward to check, and spelled out in [16, Proof of Proposition E.4]. “Only if”: Let ρ be an abstract path that is B-just in the sense of Definition 20. By Proposition 1… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

37 extracted references · 19 canonical work pages

  1. [18]

    van Glabbeek & P

    R.J. van Glabbeek & P. H ¨ofner (2019): Progress, Justness, and Fairness. ACM Computing Surveys 52(4), pp. 69:1–69:38, doi:10.1145/3329125

    doi:10.1145/3329125 2019

  2. [16]

    Progress, Fairness and Justness in Process Algebra

    R.J. van Glabbeek & P. H¨ofner (2015): Progress, Fairness and Justness in Process Algebra. Technical Report 8501, NICTA. Available at http://arxiv.org/abs/1501.03268

    work page Pith review arXiv 2015

  3. [7]

    Dyseryn, R.J

    V . Dyseryn, R.J. van Glabbeek & P. H¨ofner (2017): Analysing Mutual Exclusion using Process Algebra with Signals. In K. Peters & S. Tini, editors: Proc. Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop onStructural Operational Semantics, Electronic Proceedings in Theoretical Computer Science 255, Open Publishing Ass...

    doi:10.4204/eptcs.255.2 2017

  4. [1]

    K.R. Apt, N. Francez & S. Katz (1988): Appraising Fairness in Languages for Distributed Programming . Distributed Computing 2(4), pp. 226–241, doi:10.1007/BF01872848

    doi:10.1007/bf01872848 1988

  5. [2]

    Bednarczyk (1987): Categories of asynchronous systems

    M. Bednarczyk (1987): Categories of asynchronous systems. Ph.D. thesis, Computer Science, University of Sussex, Brighton

    work page 1987

  6. [3]

    Bouwman (2018): Liveness analysis in process algebra: simpler techniques to model mutex algorithms

    M.S. Bouwman (2018): Liveness analysis in process algebra: simpler techniques to model mutex algorithms. Technical Report, Eindhoven University of Technology. Available at http://www.win.tue.nl/~timw/ downloads/bouwman_seminar.pdf

    work page 2018

  7. [4]

    Coppo, M

    M. Coppo, M. Dezani-Ciancaglini, L. Padovani & N. Yoshida (2013): Inference of Global Progress Proper- ties for Dynamically Interleaved Multiparty Sessions. In: Proc. Coordination’13, LNCS 7890, Springer, pp. 45–59, doi:10.1007/978-3-642-38493-6 4

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

  8. [5]

    De Nicola & F.W

    R. De Nicola & F.W. Vaandrager (1995): Three Logics for Branching Bisimulation . Journal of the ACM 42(2), pp. 458–487, doi:10.1145/201019.201032

    arXiv 1995

Show all 37 references
  1. [6]

    Degano, R

    P. Degano, R. De Nicola & U. Montanari (1987): CCS is an (Augmented) Contact Free C/E System . In M.V . Zilli, editor:Mathematical Models for the Semantics of Parallelism, LNCS 280, Springer, pp. 144–165, doi:10.1007/3-540-18419-8 13

    1987 doi

  2. [8]

    Emerson & E.M

    E.A. Emerson & E.M. Clarke (1982): Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Science of Computer Programming 2(3), pp. 241–266, doi:10.1016/0167-6423(83)90017-5

    1982 doi

  3. [9]

    Emerson & J.Y

    E.A. Emerson & J.Y . Halpern (1986): ‘Sometimes’ and ‘Not Never’ revisited: on branching time versus linear time temporal logic. Journal of the ACM 33(1), pp. 151–178, doi:10.1145/4904.4999

    1986

  4. [10]

    Fehnker, R.J

    A. Fehnker, R.J. van Glabbeek, P. H¨ofner, A.K. McIver, M. Portmann & W.L. Tan (2012):A Process Algebra for Wireless Mesh Networks . In H. Seidl, editor: Proc. ESOP’12, LNCS 7211, Springer, pp. 295–315, doi:10.1007/978-3-642-28869-2 15

    2012 doi

  5. [11]

    Fehnker, R.J

    A. Fehnker, R.J. van Glabbeek, P. H¨ofner, A.K. McIver, M. Portmann & W.L. Tan (2013):A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV . Technical Report 5513, NICTA. Available at http://arxiv.org/abs/1312.7645

    2013 arXiv

  6. [12]

    van Glabbeek (2015): Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP

    R.J. van Glabbeek (2015): Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP. In R. Meyer, A. Platzer & H. Wehrheim, editors: ProceedingsCorrect System Design - Symposium in Honor of Ernst-R ¨udiger Olderog on the Occasion of His 60th Birt...

    2015 arXiv

  7. [13]

    van Glabbeek (2016): Ensuring Liveness Properties of Distributed Systems (A Research Agenda)

    R.J. van Glabbeek (2016): Ensuring Liveness Properties of Distributed Systems (A Research Agenda). Posi- tion paper. Available at https://arxiv.org/abs/1711.04240

    2016 arXiv

  8. [14]

    van Glabbeek, U

    R.J. van Glabbeek, U. Goltz & J.-W. Schicke (2008): On Synchronous and Asynchronous Interaction in Distributed Systems. In E. Ochma´nski & J. Tyszkiewicz, editors: Proceedings 33rd International Symposium Rob van Glabbeek 33 on Mathematical Foundations of Computer Science (MFC...

    2008 doi

  9. [15]

    van Glabbeek, U

    R.J. van Glabbeek, U. Goltz & J.-W. Schicke-Uffmann (2013): On Characterising Distributability. Logical Methods in Computer Science 9(3):17, doi:10.2168/LMCS-9(3:17)2013

    2013 doi

  10. [17]

    van Glabbeek & P

    R.J. van Glabbeek & P. H ¨ofner (2015): CCS: It’s not fair! Acta Informatica 52(2-3), pp. 175–205, doi:10.1007/s00236-015-0221-6

    2015 doi

  11. [19]

    van Glabbeek, P

    R.J. van Glabbeek, P. H ¨ofner & W. Wang (2021):Enabling Preserving Bisimulation Equivalence. In S. Had- dad & D. Varacca, editors: Proc. CONCUR’21, LIPIcs 203, Schloss Dagstuhl - Leibniz-Zentrum f ¨ur Infor- matik, pp. 33:1–33:20, doi:10.4230/LIPIcs.CONCUR.2021.33

    2021 doi

  12. [20]

    van Glabbeek & F.W

    R.J. van Glabbeek & F.W. Vaandrager (1987): Petri net models for algebraic theories of concurrency (ex- tended abstract). In J.W.d. Bakker, A.J. Nijman & P.C. Treleaven, editors: Proceedings PARLE, Parallel Architectures and Languages Europe, Eindhoven, The Netherlands, June 1...

    1987 doi

  13. [21]

    Kuiper & W.-P

    R. Kuiper & W.-P. de Roever (1983): Fairness Assumptions for CSP in a Temporal Logic Framework . In D. Bjørner, editor: Formal Description of Programming Concepts II , North-Holland, pp. 159–170

    1983

  14. [22]

    Lamport (1977): Proving the correctness of multiprocess programs

    L. Lamport (1977): Proving the correctness of multiprocess programs . IEEE Transactions on Software Engineering 3(2), pp. 125–143, doi:10.1109/TSE.1977.229904

    1977

  15. [23]

    Lamport (2000): Fairness and hyperfairness

    L. Lamport (2000): Fairness and hyperfairness. Distr. Comp. 13(4), pp. 239–245, doi:10.1007/PL00008921

    2000 doi

  16. [24]

    Milner (1990): Operational and algebraic semantics of concurrent processes

    R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science , chapter 19, Elsevier Science Publishers B.V . (North-Holland), pp. 1201–1242

    1990

  17. [25]

    Milner (1980): A Calculus of Communicating Systems

    R. Milner (1980): A Calculus of Communicating Systems. LNCS 92, Springer, doi:10.1007/3-540-10235-3

    1980 doi

  18. [26]

    Misra (1988): A Rebuttal of Dijkstra’s Position on Fairness

    J. Misra (1988): A Rebuttal of Dijkstra’s Position on Fairness. Available at http://www.cs.utexas.edu/ users/misra/Notes.dir/fairness.pdf

    1988

  19. [27]

    Misra (2001): A Discipline of Multiprogramming — Programming Theory for Distributed Applications

    J. Misra (2001): A Discipline of Multiprogramming — Programming Theory for Distributed Applications . Springer, doi:10.1007/978-1-4419-8528-6

    2001 doi

  20. [28]

    Olderog (1987): Operational Petri net semantics for CCSP

    E.-R. Olderog (1987): Operational Petri net semantics for CCSP. In G. Rozenberg, editor: Advances in Petri Nets 1987, covers the 7th European Workshop on Applications and Theory of Petri Nets, Oxford, UK, June 1986, LNCS 266, Springer, pp. 196–223, doi:10.1007/3-540-18086-9 27

    1987 doi

  21. [29]

    Olderog (1991): Nets, Terms and Formulas: Three Views of Concurrent Processes and their Relation- ship

    E.-R. Olderog (1991): Nets, Terms and Formulas: Three Views of Concurrent Processes and their Relation- ship. Cambridge Tracts in Theor. Comp. Sc. 23, Cambridge University Press

    1991

  22. [30]

    Owicki & L

    S.S. Owicki & L. Lamport (1982): Proving Liveness Properties of Concurrent Programs. ACM TOPLAS 4(3), pp. 455–495, doi:10.1145/357172.357178

    1982

  23. [31]

    Pnueli (1977): The Temporal Logic of Programs

    A. Pnueli (1977): The Temporal Logic of Programs. In: Proc. 18th Annual Symposium on Foundations of Computer Science (FOCS’77), IEEE, pp. 46–57, doi:10.1109/SFCS.1977.32

    1977 doi

  24. [32]

    Prasad (1991): A Calculus of Broadcasting Systems

    K.V .S. Prasad (1991): A Calculus of Broadcasting Systems . In S. Abramsky & T.S.E. Maibaum, editors: TAPSOFT’91: Proceedings of the International Joint Conference onTheory and Practice of Software Devel- opment, V olume 1: Colloquium on Trees in Algebra and Programming (CAAP’...

    1991 doi

  25. [33]

    Reisig (2013): Understanding Petri Nets — Modeling Techniques, Analysis Methods, Case Studies

    W. Reisig (2013): Understanding Petri Nets — Modeling Techniques, Analysis Methods, Case Studies . Springer, doi:10.1007/978-3-642-33278-4

    2013 doi

  26. [34]

    Shields (1985): Concurrent machines

    M.W. Shields (1985): Concurrent machines. The Computer Journal 28(5), pp. 449–465, doi:10.1093/comjnl/28.5.449. 34 Justness

    1985 doi

  27. [35]

    Stark (1989): Concurrent transition systems

    E.W. Stark (1989): Concurrent transition systems . Theoretical Computer Science 64(3), pp. 221–269, doi:10.1016/0304-3975(89)90050-9

    1989 doi

  28. [36]

    Winskel (1987): Event structures

    G. Winskel (1987): Event structures. In W. Brauer, W. Reisig & G. Rozenberg, editors: Petri Nets: Applica- tions and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, Bad Honnef, September 1986, LNCS 255, Spr...

    1987 doi

  29. [37]

    Winskel & M

    G. Winskel & M. Nielsen (1995): Models for Concurrency . In S. Abramsky, D. Gabbay & T. Maibaum, editors: Handbook of Logic in Computer Science , chapter 1, 4: Semantic Modelling, Oxford University Press, pp. 1–148

    1995

Pith tools

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