Ensuring Liveness Properties of Distributed Systems: Open Problems

Rob van Glabbeek

Ensuring Liveness Properties of Distributed Systems: Open Problems

T0 review · 0 major / 3 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 Under justness but not fairness, two strongly bisimilar programs differ in whether x necessarily reaches 1.

desk verdict A well-built agenda paper: no new theorem, but a clear and honest synthesis of the justness program, with a checkable P/Q example worth engaging. read the letter →

arxiv 1912.05616 v1 pith:QDQELEBI submitted 2019-08-04 cs.LO

Rob van Glabbeek This is my paper · ORCID

classification cs.LO MSC 68Q8568Q60

keywords livenessjustnessfairnessassumptionsprocessalgebratemporallogicstrongbisimilaritydistributedsystemsverification

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

This paper argues that the standard formal toolbox for distributed systems—process algebras, temporal logics, and the equivalences built on them—cannot certify certain liveness properties without assuming fairness, and that fairness assumptions are often unwarranted. It exhibits two simple programs, $P$ and $Q$, that are strongly bisimilar, i.e. indistinguishable by the standard behavioural equivalence used across process algebra, yet under justness $P$ guarantees that $x$ will eventually be set to $1$ while $Q$ does not. The reason is structural: in $P$ the action $x:=1$ belongs to an independent parallel component, so justness forces that component to act, whereas in $Q$ both actions are branches of one repeated nondeterministic choice that an environment may resolve the same way forever. The paper therefore sets out a research agenda for a concurrency theory that takes justness, not fairness, as its completeness criterion, requiring new equivalences, proof principles, axiomatisations, congruence formats, and models.

What carries the argument

The load-bearing object is justness, a completeness criterion formalised on component-labelled transition systems. A transition is labelled with the set of parallel components that participate in it, and a run is just if every non-blocking transition enabled at some point is eventually taken or interfered with by a transition sharing at least one component. Justness is stronger than progress—a system with an enabled non-blocking transition will not idle forever—but weaker than fairness, which additionally demands that perpetually or relentlessly enabled tasks eventually occur. The component labels are what separate $P$ and $Q$: in $P$, the $x:=1$ transition belongs to a component of its own, while in $Q$ it is a guarded alternative inside the component that also performs $y:=y+1$. The paper's interpretation of nondeterministic choice as demonic and external supplies the last step: an environment may forever resolve the repeated choice in $Q$ towards $y:=y+1$, making the run just.

What would settle it

Analyse the shared two-state transition system of $P$ and $Q$ with a justness-aware tool: the property 'eventually $x=1$' must hold for $P$ and fail for $Q$, because the infinite run that always chooses $y:=y+1$ in $Q$ is just. Any verification formalism that proves the property for both, or that declares $P$ and $Q$ equivalent while claiming to preserve liveness, contradicts the paper's central claim; exhibiting a standard equivalence that already separates them would falsify the claim that contemporary process algebras cannot.

Watch

Extended reading notes

Core claim

The paper's central claim is that contemporary process algebras and temporal logics fail to distinguish systems whose liveness behaviour differs, once justness is assumed and fairness is not. The counterexample is the pair $P = x:=1 \parallel \text{repeat } y:=y+1$ and $Q = \text{repeat }(\text{if True then } y:=y+1 \text{ else if } x=0 \text{ then } x:=1)$, both starting with $x=y=0$. $P$ and $Q$ are strongly bisimilar—both reduce to a state with two looping transitions, $y:=y+1$ and $x:=1$—so virtually every process-algebraic equivalence identifies them. Under justness, however, every run of $P$ must eventually perform $x:=1$, because that action is enabled in an independent component and justness demands that an enabled non-blocking transition of a component is eventually taken or interfered with. In $Q$, the same action is only one branch of a choice inside a single component, and the run that always picks $y:=y+1$ is just; hence $x=1$ is not guaranteed. Any formalism that equates strongly bisimilar systems must therefore either credit $Q$ with a liveness property it lacks under justness or remain unable to establish that property for $P$.

Load-bearing premise

The distinction between $P$ and $Q$ collapses unless nondeterministic choice is treated as demonic external choice—an environment may resolve the same branch forever—and unless justness is accepted as the right completeness criterion; both are assumptions about how systems behave, not theorems.

Editorial extensions

If this is right

Verification by strong bisimilarity or coarser equivalences can silently erase liveness distinctions: a system shown equivalent to a specification may inherit a guarantee it does not actually possess under justness.
Proof rules built on fair abstraction, such as the Koomen Fair Abstraction Rule, need to be re-examined because they can validate liveness conclusions that fail in reality when fairness is unwarranted.
New semantic equivalences, finer than or incomparable with strong bisimilarity, are needed; candidates named in the paper include justness-preserving bisimilarity and structure-preserving bisimilarity.
Basic verification infrastructure must be rebuilt: complete axiomatisations, induction principles such as the recursive specification principle, and congruence formats all need versions that respect justness.
Even simple systems such as fair schedulers and mutual exclusion protocols cannot be specified faithfully in standard CCS or Petri nets without fairness, motivating extensions such as broadcast, priorities, and signals.

Reading between the lines

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

A quick test for any proposed equivalence is whether it distinguishes $P$ and $Q$; any equivalence that identifies them cannot support justness-based liveness verification unless component information is added.
If the repeated choice in $Q$ carried a fixed positive lower probability, the run that always chooses $y:=y+1$ would have probability zero, suggesting that a probabilistic-justness hybrid could interpolate between the paper's demonic nondeterminism and full fairness.
The component-versus-choice distinction should transfer to real schedulers: an implementation that serialises two logically independent operations inside one scheduling decision silently loses the guarantee that the second operation will ever happen.
Temporal logics could be extended with a component-based modality expressing that every component eventually progresses, which might capture justness without abandoning standard model checking.

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

You should know: this is not a new-result paper. The load-bearing concepts—justness, the completeness hierarchy, the P/Q pair—come from van Glabbeek's earlier work with Hofner and others. What is new is the packaging: a ten-task research agenda plus a set of open problems. If you work on process algebra or liveness, this is a useful map of a serious program; if you don't, the main thing to know is that the claim "strongly bisimilar yet different liveness under justness" is real and works under the paper's explicit definitions.

What it does well: the P/Q example is the centerpiece and it holds up. Both programs have the same two-state LTS, so they are strongly bisimilar. Under the component-labelled transition system and the justness definition in the appendices, P's x:=1 belongs to a separate component that must eventually progress, while Q's x:=1 belongs to the same component as y:=y+1, so an infinite y-only run is just. The paper also records referee counterarguments honestly, including the alternative model in Figure 1(d), and defends its position rather than hiding it. Proposition 1 restates a known ordering, but cleanly. The appendices give enough formal detail that the definitions are checkable.

Soft spots: the central normative claim—that fairness assumptions are unwarranted by default and justness is the right completeness criterion—is a philosophical position, not a theorem. The whole distinction depends on interpreting nondeterministic choice as demonic and external (Section 2.2). If you adopt a probabilistic or fairness-flavored interpretation of choice, P and Q no longer differ. The author explicitly says this is the point under debate, so it is not a hidden flaw, but it means the paper argues a stance rather than proves it. The paper also leans heavily on the author's own prior work; that is natural for an agenda paper, but a reader new to the area will need to go to [GH18] and [Gla19a] for the full substance. The self-citation is transparent and the references are otherwise solid.

Who this is for: anyone in concurrency theory or formal verification interested in liveness with progress-like assumptions but without fairness. I would bring it to reading group, and I would cite it if I were writing about justness or liveness in process algebra. It deserves to be sent to referees: it is an invited open-problems article that clearly frames a research program with concrete, checkable examples, and the weaknesses are acknowledged modeling choices rather than errors.

Referee Report

0 major / 3 minor

Summary. This paper is a position/research-agenda article. It argues that global fairness assumptions are by default unwarranted for establishing liveness properties of distributed systems, and that justness—a progress property strictly weaker than fairness—is the appropriate default completeness criterion. The central technical demonstration is the pair of programs P and Q in Section 5: both have the same two-state labelled transition system and are strongly bisimilar, yet under justness P guarantees that x eventually becomes 1 whereas Q does not, because in Q the choice between y:=y+1 and x:=1 is made by the same component and may forever select y:=y+1. The paper then explains why standard process algebras and temporal logics fail to make this distinction, discusses the dangers of fair abstraction, and lays out a ten-task research agenda covering equivalences, axiomatisations, congruence formats, Petri nets, expressiveness, time, probability, and applications.

Significance. If the central claim is accepted, the paper identifies a real blind spot in interleaving-based verification: semantic equivalences no finer than strong bisimilarity collapse systems that differ in a crucial liveness property under justness. The P/Q example is small, self-contained, and checkable from the definitions in Appendices A and B, and the paper is commendably explicit about the modeling assumption on which it rests: nondeterministic choice is interpreted as external, demonic choice (Section 2.2). The hierarchy in Section 4, supported by Proposition 1 in Appendix C, is a useful contribution. The main limitation is that the normative conclusion—that fairness is unwarranted by default—is a modeling position rather than a theorem; readers who adopt a probabilistic or fairness-flavored interpretation of internal choice will not obtain the P/Q separation. The paper openly acknowledges this in the Figure 1 discussion, so the assumption is stated rather than hidden. As a research agenda, the paper gives the justness program a compact and testable form.

minor comments (3)

[Section 5, Figure 3] The row for 'progress' reports the liveness goal y=7 for Q as '−', but the text immediately above the table says that the progress assumption is sufficient to ensure that in P or Q the variable y will at some point reach the value 7; this row should presumably read '+ + − −' rather than '+ − − −'.
[Section 5, 'Variations on this example'] The CCS rendering of the example needs the defining equations of the process constants: as written, it is not clear what process b (or ¯b) denotes, and after the τ-step P=(Y|τ) leaves a residual Y|0 with an a-loop whereas the residual of Q depends on the unspecified definition of b; please provide the defining equations or state the intended convention so that the claim that both systems are represented by the same labelled transition system can be checked.
[Task 2 (RSP discussion)] The claim that P and Q are both solutions of the guarded recursion U = (y:=y+1).U + (x:=1).V, V = (y:=y+1).V up to justness-preserving strong bisimilarity needs clarification: under the component-labelled semantics of Appendix A, the top-level choice in the right-hand side is executed by the empty component sequence, so the infinite y-run is just in the right-hand side but unjust in P; please specify whether the equations are intended over component-enriched behaviours, or restrict the RSP-soundness remark to a coarser equivalence.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the P/Q distinction is a self-contained demonstration under the paper's explicitly stated justness and choice semantics.

full rationale

The paper's central claim—that P and Q are strongly bisimilar yet differ on the liveness property x=1 under justness—is not circular. P and Q are defined independently in Section 5 and explicitly exhibit the same two-state labelled transition system, so strong bisimilarity is verified by inspection rather than assumed. The justness criterion is not imported as an unexamined black box: Definition 5 in Appendix B states the formal condition, and Section 3 explains the component-based intuition; the P/Q analysis then applies that definition directly. In P, the x:=1 transition stems from a separate component whose inaction makes the infinite y-only run unjust; in Q, the same transition belongs to the looping component, so an infinite y-only run is just by Definition 5. The demonic interpretation of nondeterministic choice is presented and defended explicitly in Section 2.2, including the referee's counterexample, rather than being smuggled in. The paper does cite the author's own earlier work for justness ([GH18], [GH15b], [Gla19a]) and for the broader claim that semantic equivalences fail to respect inevitability ([Gla15]), but the relevant definitions are reproduced in the appendices and the P/Q construction is self-contained. These citations are transparent references, not load-bearing reductions of the argument to its conclusions. No fitted parameter is renamed as a prediction, and no derivation is equivalent to its inputs by construction. Accordingly, there is no significant circularity.

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

The paper introduces no fitted numerical constants. Its conclusions rest on the progress and justness assumptions, the demonic-choice interpretation of nondeterminism, and a structural independence property of components in the new component-labelled transition system model.

assumptions (5)

domain assumption A system in a state that admits a non-blocking transition will eventually progress, i.e., perform a transition.
Section 3 defines progress; the paper says 'without a progress assumption no meaningful liveness properties can be established.' This is an assumption about system behavior, not a theorem.
domain assumption Once a non-blocking transition is enabled that stems from a set of parallel components, one (or more) of these components will eventually partake in a transition.
Section 3 and Definition 5 in Appendix B. This is the justness criterion on which the whole agenda is built.
ad hoc to paper Nondeterministic choice is an external choice triggered by an aspect of the environment outside our grasp (demonic choice).
Section 2.2. Needed to justify that in program Q the same component may always choose y:=y+1, so x:=1 never occurs. This is a philosophical modeling decision, not derived.
domain assumption In a component-labelled transition system, if two enabled transitions have no common components, a transition enabled before one of them occurs remains enabled after it (property (1)).
Definition 1, Appendix B. This structural independence property is needed for the definition of justness and for Proposition 1.
domain assumption The set of blocking actions B is chosen by the modeler, with restrictions on restriction and relabelling operators.
Appendix B. The choice of B affects which runs count as just; different applications may require different choices.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Ensuring Liveness Properties of Distributed Systems: Open Problems." pith.science (2026). https://pith.science/paper/QDQELEBI

@misc{pith2026191205616,
  author       = {Pith},
  title        = {Pith review of: Ensuring Liveness Properties of Distributed Systems: Open Problems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QDQELEBI}},
  note         = {Machine review of arXiv:1912.05616}
}

read the original abstract

Often fairness assumptions need to be made in order to establish liveness properties of distributed systems, but in many situations they lead to false conclusions. This document presents a research agenda aiming at laying the foundations of a theory of concurrency that is equipped to ensure liveness properties of distributed systems without making fairness assumptions. This theory will encompass process algebra, temporal logic and semantic models. The agenda also includes the development of a methodology and tools that allow successful application of this theory to the specification, analysis and verification of realistic distributed systems. Contemporary process algebras and temporal logics fail to make distinctions between systems of which one has a crucial liveness property and the other does not, at least when assuming justness, a strong progress property, but not assuming fairness. Setting up an alternative framework involves giving up on identifying strongly bisimilar systems, inventing new induction principles, developing new axiomatic bases for process algebras and new congruence formats for operational semantics, and creating matching treatments of time and probability. Even simple systems like fair schedulers or mutual exclusion protocols cannot be accurately specified in standard process algebras (or Petri nets) in the absence of fairness assumptions. Hence the work involves the study of adequate language or model extensions, and their expressive power.

Figures

Figures reproduced from arXiv: 1912.05616 by the authors.

**Figure 2.** A hierarchy of completeness criteria In [Gla19a], assumptions like progress, justness and fairness are called completeness criteria. They serve to rule out certain runs of distributed systems that appear to be valid in their representations as transition systems, on grounds that such runs are assumed not to occur in practice. The completeness criterion “progress” for instance, applied to the transition system on p… view at source ↗

**Figure 3.** Liveness properties obtained as a function of assumptions made When assuming that parallel composition is implemented by means of a scheduler that arbitrarily interleaves actions from both processes, this conclusion for P appears plausible. However, when k denotes a true parallel composition, where the program P consists of two completely independent processes, it appears more reasonable to adopt the assumption of … view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

109 extracted references · 39 canonical work pages

[1]

Austry & author G

author D. Austry & author G. Boudol ( year 1984 ): title Alg\` e bre de processus et synchronisations . journal Theoretical Computer Science volume 30 ( number 1 ), pp. pages 91--131 , doi:10.1016/0304-3975(84)90067-7. article AFK88

doi:10.1016/0304-3975(84)90067-7 1984
[2]

Apt , author N

author K.R. Apt , author N. Francez & author S. Katz ( year 1988 ): title Appraising Fairness in Languages for Distributed Programming . journal Distributed Computing volume 2 ( number 4 ), pp. pages 226--241 , doi:10.1007/BF01872848. book Ba90

doi:10.1007/bf01872848 1988
[3]

Baeten , editor ( year 1990 ): title Applications of Process Algebra

editor J.C.M. Baeten , editor ( year 1990 ): title Applications of Process Algebra . series Cambridge Tracts in Theoretical Computer Science 17 , publisher Cambridge University Press . article BBK87a

1990
[4]

Baeten , author J.A

author J.C.M. Baeten , author J.A. Bergstra & author J.W. Klop ( year 1987 ): title On the Consistency of Koomen's Fair Abstraction Rule . journal Theoretical Computer Science volume 51 ( number 1/2 ), pp. pages 129--176 , doi:10.1016/0304-3975(87)90052-1. book BBR10

work page doi:10.1016/0304-3975(87)90052-1 1987
[5]

Baeten , author T

author J.C.M. Baeten , author T. Basten & author M.A. Reniers ( year 2010 ): title Process Algebra: Equational Theories of Communicating Processes . publisher Cambridge University Press . inproceedings EPTCS54.4

2010
[6]

Buti , author M

author F. Buti , author M. Callisto De Donato , author F. Corradini , author M.R. Di Berardini & author W. Vogler ( year 2011 ): title Automated Analysis of MUTEX Algorithms with FASE . In editor G. D'Agostino & editor S. La Torre , editors: booktitle Proc. GandALF '11 , series EPTCS volume 54 , publisher Open Publishing Association , pp. pages 45--59 , d...

work page doi:10.4204/eptcs.54.4 2011
[7]

Boudol , author I

author G. Boudol , author I. Castellani , author M. Hennessy & author A. Kiehn ( year 1994 ): title A Theory of Processes with Localities . journal Formal Aspects of Computing volume 6 ( number 2 ), pp. pages 165--200 , doi:10.1007/BF01221098. inproceedings BDL04

doi:10.1007/bf01221098 1994
[8]

Behrmann , author A

author G. Behrmann , author A. David & author K.G. Larsen ( year 2004 ): title A Tutorial on Uppaal . In editor M. Bernardo & editor F. Corradini , editors: booktitle Revised Lectures on Formal Methods for the Design of Real-Time Systems , series LNCS volume 3185 , publisher Springer , pp. pages 200--236 , doi:10.1007/978-3-540-30080-9_7. article BFG04

doi:10.1007/978-3-540-30080-9_7 2004

Show all 109 references

[9]

Bloom , author W.J

author B. Bloom , author W.J. Fokkink & author R.J. van Glabbeek ( year 2004 ): title Precongruence Formats for Decorated Trace Semantics . journal Transactions on Computational Logic volume 5 ( number 1 ), pp. pages 26--78 , doi:10.1145/963927.963929. article BolG96

2004
[10]

Bol & author J.F

author R.N. Bol & author J.F. Groote ( year 1996 ): title The meaning of negative premises in transition system specifications . journal Journal of the ACM volume 43 ( number 5 ), pp. pages 863--914 , doi:10.1145/234752.234756. article BGRV15

1996
[11]

Borgstr \" o m , author R

author J. Borgstr \" o m , author R. Gutkovas , author I. Rodhe & author B. Victor ( year 2015 ): title The Psi-Calculi Workbench: A Generic Tool for Applied Process Calculi . journal ACM Transactions on Embedded Computing Systems volume 14 ( number 1 ), pp. pages 9:1--9:25 , ...

2015 doi
[12]

Brookes , author C.A.R

author S.D. Brookes , author C.A.R. Hoare & author A.W. Roscoe ( year 1984 ): title A theory of communicating sequential processes . journal Journal of the ACM volume 31 ( number 3 ), pp. pages 560--599 , doi:10.1145/828.833. article BIM95

1984 doi
[13]

Bloom , author S

author B. Bloom , author S. Istrail & author A.R. Meyer ( year 1995 ): title Bisimulation Can't be Traced . journal Journal of the ACM volume 42 ( number 1 ), pp. pages 232--268 , doi:10.1145/200836.200876. article BJPV11

1995
[14]

Bengtson , author M

author J. Bengtson , author M. Johansson , author J. Parrow & author B. Victor ( year 2011 ): title Psi-calculi: a framework for mobile processes with nominal data and logic . journal Logical Methods in Computer Science volume 7 ( number 1 ), doi:10.2168/LMCS-7(1:11)2011. inco...

2011 doi
[15]

Bergstra & author J.W

author J.A. Bergstra & author J.W. Klop ( year 1986 ): title Algebra of communicating processes . In editor J.W. de Bakker , editor M. Hazewinkel & editor J.K. Lenstra , editors: booktitle Mathematics and Computer Science , series CWI Monograph 1 , publisher North-Holland , ad...

1986
[16]

Bergstra & author J.W

author J.A. Bergstra & author J.W. Klop ( year 1986 ): title Verification of an alternating bit protocol by means of process algebra . In editor W. Bibel & editor K.P. Jantke , editors: booktitle Mathematical Methods of Specification and Synthesis of Software Systems '85 , ser...

1986 doi
[17]

Baier & author J

author C. Baier & author J. Katoen ( year 2008 ): title Principles of model checking . publisher MIT Press . article Bl95

2008
[18]

Bloom ( year 1995 ): title Structural operational semantics for weak bisimulations

author B. Bloom ( year 1995 ): title Structural operational semantics for weak bisimulations . journal Theoretical Computer Science volume 146 , pp. pages 25--68 , doi:10.1016/0304-3975(94)00152-9. incollection Bo85

1995 doi
[19]

Boudol ( year 1985 ): title Notes on algebraic calculi of processes

author G. Boudol ( year 1985 ): title Notes on algebraic calculi of processes . In editor K. Apt , editor: booktitle Logics and Models of Concurrent Systems , series NATO ASI Series F13 , publisher Springer , pp. pages 261--303 , doi:10.1007/978-3-642-82453-1_9. inproceedings BRV95

1985 doi
[20]

Brinksma , author A

author E. Brinksma , author A. Rensink & author W. Vogler ( year 1995 ): title Fair Testing . In editor I. Lee & editor S. Smolka , editors: booktitle Proceedings 6th International Conference on Concurrency Theory ( CONCUR '95) , series LNCS volume 962 , publisher Springer , p...

1995 doi
[21]

Brinksma , author A

author E. Brinksma , author A. Rensink & author W. Vogler ( year 1996 ): title Applications of Fair Testing . In editor R. Gotzhein & editor J. Bredereke , editors: booktitle Proceedings IFIP TC6 WG6.1 International Conference on Formal Description Techniques IX: Theory, appli...

1996
[22]

Bartlett , author R.A

author K.A. Bartlett , author R.A. Scantlebury & author P.T. Wilkinson ( year 1969 ): title A note on reliable full-duplex transmission over half-duplex links . journal CACM volume 12 , pp. pages 260--261 , doi:10.1145/362946.362970. book BW90

1969
[23]

Baeten & author W.P

author J.C.M. Baeten & author W.P. Weijland ( year 1990 ): title Process Algebra . series Cambridge Tracts in Theoretical Computer Science 18 , publisher Cambridge University Press , doi:10.1017/CBO9780511624193. article CDV06a

1990 doi
[24]

Corradini , author M.R

author F. Corradini , author M.R. Di Berardini & author W. Vogler ( year 2006 ): title Fairness of Actions in System Computations . journal Acta Informatica volume 43 ( number 2 ), pp. pages 73--130 , doi:10.1007/s00236-006-0011-2. article CDV06c

2006 doi
[25]

Corradini , author M.R

author F. Corradini , author M.R. Di Berardini & author W. Vogler ( year 2006 ): title Fairness of Components in System Computations . journal Theoretical Computer Science volume 356 ( number 3 ), pp. pages 291--324 , doi:10.1016/j.tcs.2006.02.011. article CorradiniEtAl09

2006 doi
[26]

Corradini , author M.R

author F. Corradini , author M.R. Di Berardini & author W. Vogler ( year 2009 ): title Liveness of a Mutex Algorithm in a Fair Process Algebra . journal Acta Informatica volume 46 ( number 3 ), pp. pages 209--235 , doi:10.1007/s00236-009-0092-9. inproceedings CDV09

2009 doi
[27]

Corradini , author M.R

author F. Corradini , author M.R. Di Berardini & author W. Vogler ( year 2009 ): title Time and Fairness in a Process Algebra with Non-blocking Reading . In editor M. Nielsen , editor A. Kucera , editor P.B. Miltersen , editor C. Palamidessi , editor P. Tuma & editor F.D. Vale...

2009 doi
[28]

Cleaveland , author G

author R. Cleaveland , author G. L \"u ttgen & author V. Natarajan ( year 2001 ): title Priority in Process Algebra . In editor J.A. Bergstra , editor A. Ponse & editor S.A. Smolka , editors: booktitle Handbook of Process Algebra , chapter chapter 12 , publisher Elsevier , pp....

2001 doi
[29]

Costa & author C

author G. Costa & author C. Stirling ( year 1984 ): title A Fair Calculus of Communicating Systems . journal Acta Informatica volume 21 , pp. pages 417--441 , doi:10.1007/BF00271640. article CS87

1984 doi
[30]

Costa & author C

author G. Costa & author C. Stirling ( year 1987 ): title Weak and Strong Fairness in CCS . journal Information and Computation volume 73 ( number 3 ), pp. pages 207--244 , doi:10.1016/0890-5401(87)90013-7. incollection CS01

1987 doi
[31]

Cleaveland & author O

author R. Cleaveland & author O. Sokolsky ( year 2001 ): title Equivalence and Preorder Checking for Finite-State Systems . In editor J.A. Bergstra , editor A. Ponse & editor S.A. Smolka , editors: booktitle Handbook of Process Algebra , chapter chapter 6 , publisher Elsevier ...

2001 doi
[32]

Dyseryn , author R.J

author V. Dyseryn , author R.J. van Glabbeek & author P. H\"ofner ( year 2017 ): title Analysing Mutual Exclusion using Process Algebra with Signals . In editor K. Peters & editor S. Tini , editors: booktitle Proceedings Combined 24th International Workshop on Expressiveness i...

2017 doi
[33]

Deng , author R.J

author Y. Deng , author R.J. van Glabbeek , author M. Hennessy & author C.C. Morgan ( year 2008 ): title Characterising Testing Preorders for Finite Probabilistic Processes . journal Logical Methods in Computer Science volume 4 ( number 4 ): eid 4 , doi:10.2168/LMCS-4(4:4)2008...

2008 doi
[34]

De Nicola & author M

author R. De Nicola & author M. Hennessy ( year 1984 ): title Testing equivalences for processes . journal Theoretical Computer Science volume 34 , pp. pages 83--133 , doi:10.1016/0304-3975(84)90113-0. article EC82

1984 doi
[35]

Emerson & author E.M

author E.A. Emerson & author E.M. Clarke ( year 1982 ): title Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. journal Science of Computer Programming volume 2 ( number 3 ), pp. pages 241--266 , doi:10.1016/0167-6423(83)90017-5. inproceedings FGHMPT12a

1982 doi
[36]

Fehnker , author R.J

author A. Fehnker , author R.J. van Glabbeek , author P. H \"o fner , author A.K. McIver , author M. Portmann & author W. Tan ( year 2012 ): title A Process Algebra for Wireless Mesh Networks . In editor H. Seidl , editor: booktitle Programming Languages and Systems: Proceedin...

2012 doi
[37]

Fehnker , author R.J

author A. Fehnker , author R.J. van Glabbeek , author P. H \" o fner , author A.K. McIver , author M. Portmann & author W.L. Tan ( year 2013 ): title A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV . type Technical Report number 55...

2013 arXiv
[38]

Fokkink , author R.J

author W.J. Fokkink , author R.J. van Glabbeek & author P. de Wind ( year 2012 ): title Divide and congruence: From decomposition of modal formulas to preservation of branching and -bisimilarity . journal Information and Computation volume 214 , pp. pages 59--85 , doi:10.1016/...

2012 doi
[39]

Fokkink ( year 2000 ): title Introduction to Process Algebra

author W.J. Fokkink ( year 2000 ): title Introduction to Process Algebra . series Texts in Theoretical Computer Science, An EATCS Series , publisher Springer , doi:10.1007/978-3-662-04293-9. article Fok00b

2000 doi
[40]

Fokkink ( year 2000 ): title Rooted branching bisimulation as a congruence

author W.J. Fokkink ( year 2000 ): title Rooted branching bisimulation as a congruence . journal Journal of Computer and System Sciences volume 60 ( number 1 ), pp. pages 11--27 , doi:10.1006/jcss.1999.1663. inproceedings GRABR14

2000
[41]

Gibson - Robinson , author P.J

author T. Gibson - Robinson , author P.J. Armstrong , author A. Boulgakov & author A.W. Roscoe ( year 2014 ): title FDR3 - A Modern Refinement Checker for CSP . In editor E. \' A brah \' a m & editor K. Havelund , editors: booktitle Proceedings 20th International Conference on...

2014 doi
[42]

van Glabbeek & author U

author R.J. van Glabbeek & author U. Goltz ( year 2001 ): title Refinement of Actions and Equivalence Notions for Concurrent Systems . journal Acta Informatica volume 37 , pp. pages 229--327 , doi:10.1007/s002360000041. article GGS13

2001 doi
[43]

van Glabbeek , author U

author R.J. van Glabbeek , author U. Goltz & author J.-W. Schicke - Uffmann ( year 2013 ): title On Characterising Distributability . journal Logical Methods in Computer Science volume 9 ( number 3 ): eid 17 , doi:10.2168/LMCS-9(3:17)2013. article GH15b

2013 doi
[44]

van Glabbeek & author P

author R.J. van Glabbeek & author P. H \" o fner ( year 2015 ): title CCS: It's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions . journal Acta Informatica volume 52 ( number 2-3 ), pp. pages 175--205 , ...

2015 doi
[45]

van Glabbeek & author P

author R.J. van Glabbeek & author P. H \"o fner ( year 2015 ): title Progress, Fairness and Justness in Process Algebra . type Technical Report number 8501 , institution NICTA , address Sydney, Australia . ://arxiv.org/abs/1501.03268. techreport GH18

2015 arXiv
[46]

van Glabbeek & author P

author R.J. van Glabbeek & author P. H \"o fner ( year 2018 ): title Progress, Justness and Fairness . type Survey paper , institution Data61, CSIRO , address Sydney, Australia . ://arxiv.org/abs/1810.07414. note To appear in ACM Computing Surveys . misc vG91

2018 arXiv
[47]

van Glabbeek ( year 1991 ): title Bisimulations for higher dimensional automata

author R.J. van Glabbeek ( year 1991 ): title Bisimulations for higher dimensional automata . howpublished Email message, July 7, 1991 . ://theory.stanford.edu/ rvg/hda. inproceedings vG93

1991
[48]

van Glabbeek ( year 1993 ): title The Linear Time -- Branching Time Spectrum II ; The semantics of sequential systems with silent moves (extended abstract)

author R.J. van Glabbeek ( year 1993 ): title The Linear Time -- Branching Time Spectrum II ; The semantics of sequential systems with silent moves (extended abstract) . In editor E. Best , editor: booktitle Proceedings CONCUR'93, 4 ^ th International Conference on Concurrency...

1993 doi
[49]

van Glabbeek ( year 1994 ): title On the expressiveness of ACP (extended abstract)

author R.J. van Glabbeek ( year 1994 ): title On the expressiveness of ACP (extended abstract) . In editor A. Ponse , editor C. Verhoef & editor S.F.M. van Vlijmen , editors: booktitle Proceedings First Workshop on the Algebra of Communicating Processes (ACP'94) , series Works...

1994 doi
[50]

van Glabbeek ( year 2001 ): title The Linear Time -- Branching Time Spectrum I ; The Semantics of Concrete, Sequential Processes

author R.J. van Glabbeek ( year 2001 ): title The Linear Time -- Branching Time Spectrum I ; The Semantics of Concrete, Sequential Processes . In editor J.A. Bergstra , editor A. Ponse & editor S.A. Smolka , editors: booktitle Handbook of Process Algebra , chapter chapter 1 , ...

2001 doi
[51]

van Glabbeek ( year 2010 ): title The Coarsest Precongruences Respecting Safety and Liveness Properties

author R.J. van Glabbeek ( year 2010 ): title The Coarsest Precongruences Respecting Safety and Liveness Properties . In editor C.S. Calude & editor V. Sassone , editors: booktitle Proceedings 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS 2...

2010 doi
[52]

van Glabbeek ( year 2011 ): title Bisimulation

author R.J. van Glabbeek ( year 2011 ): title Bisimulation . In editor D. Padua , editor: booktitle Encyclopedia of Parallel Computing , publisher Springer , pp. pages 136--139 , doi:10.1007/978-0-387-09766-4\_149. article vG11

2011 doi
[53]

van Glabbeek ( year 2011 ): title On Cool Congruence Formats for Weak Bisimulations

author R.J. van Glabbeek ( year 2011 ): title On Cool Congruence Formats for Weak Bisimulations . journal Theoretical Computer Science volume 412 ( number 28 ), pp. pages 3283--3302 , doi:10.1016/j.tcs.2011.02.036. inproceedings vG12

2011 doi
[54]

van Glabbeek ( year 2012 ): title Musings on Encodings and Expressiveness

author R.J. van Glabbeek ( year 2012 ): title Musings on Encodings and Expressiveness . In editor B. Luttik & editor M.A. Reniers , editors: booktitle Proceedings EXPRESS/SOS'19 , series EPTCS volume 89 , publisher Open Publishing Association , pp. pages 81--98 , doi:10.4204/E...

2012 doi
[55]

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

author R.J. van Glabbeek ( year 2015 ): title Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP . In editor R. Meyer , editor A. Platzer & editor H. Wehrheim , editors: booktitle Proceedings Correct System Design - Symposium in Honor of E...

2015 doi
[56]

van Glabbeek ( year 2017 ): title Lean and Full Congruence Formats for Recursion

author R.J. van Glabbeek ( year 2017 ): title Lean and Full Congruence Formats for Recursion . In: booktitle Proceedings 32^ nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 , publisher IEEE Computer Society Press , doi:10.1109/LICS.2017.8005142. techreport vG19

2017
[57]

van Glabbeek ( year 2019 ): title Justness: A Completeness Criterion for Capturing Liveness Properties

author R.J. van Glabbeek ( year 2019 ): title Justness: A Completeness Criterion for Capturing Liveness Properties . type Technical Report , institution Data61, CSIRO , address Sydney, Australia . ://theory.stanford.edu/ rvg/abstracts.html#133. note Extended abstract in M. Boj...

2019 doi
[58]

van Glabbeek ( year 2019 ): title Reward Testing Equivalences for Processes

author R.J. van Glabbeek ( year 2019 ): title Reward Testing Equivalences for Processes . In: M. Boreale, F. Corradini, M. Loreti & R. Pugliese, editors: booktitle Models, Languages, and Tools for Concurrent and Distributed Programming, Essays Dedicated to Rocco De Nicola on t...

2019 doi
[59]

Garavel , author F

author H. Garavel , author F. Lang , author R. Mateescu & author W. Serwe ( year 2011 ): title CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes . In editor P.A. Abdulla & editor K.R.M. Leino , editors: booktitle Proceedings 17th International Con...

2011 doi
[60]

van Glabbeek , author B

author R.J. van Glabbeek , author B. Luttik & author N. Tr c ka ( year 2009 ): title Branching Bisimilarity with Explicit Divergence . journal Fundamenta Informaticae volume 93 ( number 4 ), pp. pages 371--392 , doi:10.3233/FI-2009-109. inproceedings GM84

2009 doi
[61]

Goltz & author A

author U. Goltz & author A. Mycroft ( year 1984 ): title On the relationship of CCS and Petri nets . In editor J. Paredaens , editor: booktitle Proceedings 11^ th ICALP , series LNCS volume 172 , publisher Springer , pp. pages 196--208 , doi:10.1007/3-540-13345-3_18. book GM14

1984 doi
[62]

Groote & author M.R

author J.F. Groote & author M.R. Mousavi ( year 2014 ): title Modeling and Analysis of Communicating Systems . publisher MIT Press . article GMR06

2014
[63]

Groote , author M.R

author J.F. Groote , author M.R. Mousavi & author M.A. Reniers ( year 2006 ): title A Hierarchy of SOS Rule Formats . journal Electronic Notes in Theoretical Computer Science volume 156 ( number 1 ), pp. pages 3--25 , doi:10.1016/j.entcs.2005.11.077. article Gorla10a

2006 doi
[64]

Gorla ( year 2010 ): title Towards a unified approach to encodability and separation results for process calculi

author D. Gorla ( year 2010 ): title Towards a unified approach to encodability and separation results for process calculi . journal Information and Computation volume 208 ( number 9 ), pp. pages 1031--1053 , doi:10.1016/j.ic.2010.05.002. article Gr93

2010 doi
[65]

Groote ( year 1993 ): title Transition System Specifications with Negative Premises

author J.F. Groote ( year 1993 ): title Transition System Specifications with Negative Premises . journal Theoretical Computer Science volume 118 ( number 2 ), pp. pages 263--299 , doi:10.1016/0304-3975(93)90111-6. inproceedings GV87

1993 doi
[66]

van Glabbeek & author F.W

author R.J. van Glabbeek & author F.W. Vaandrager ( year 1987 ): title Petri net models for algebraic theories of concurrency (extended abstract) . In editor J.W. de Bakker , editor A.J. Nijman & editor P.C. Treleaven , editors: booktitle Proceedings PARLE, Parallel Architectu...

1987 doi
[67]

Groote & author F.W

author J.F. Groote & author F.W. Vaandrager ( year 1992 ): title Structured Operational Semantics and Bisimulation as a Congruence . journal Information and Comp. volume 100 ( number 2 ), pp. pages 202--260 , doi:10.1016/0890-5401(92)90013-6. article GV93

1992 doi
[68]

van Glabbeek & author F.W

author R.J. van Glabbeek & author F.W. Vaandrager ( year 1993 ): title Modular Specification of Process Algebras . journal Theoretical Computer Science volume 113 ( number 2 ), pp. pages 293--348 , doi:10.1016/0304-3975(93)90006-F. article GW96

1993 doi
[69]

van Glabbeek & author W.P

author R.J. van Glabbeek & author W.P. Weijland ( year 1996 ): title Branching Time and Abstraction in Bisimulation Semantics . journal Journal of the ACM volume 43 ( number 3 ), pp. pages 555--600 , doi:10.1145/233551.233556. note Available in part at http://Theory.Stanford.E...

1996
[70]

Hoare ( year 1985 ): title Communicating S equential P rocesses

author C.A.R. Hoare ( year 1985 ): title Communicating S equential P rocesses . publisher Prentice-Hall , address Englewood Cliffs . book SPIN

1985
[71]

Holzmann ( year 2004 ): title The SPIN Model Checker - primer and reference manual

author G.J. Holzmann ( year 2004 ): title The SPIN Model Checker - primer and reference manual . publisher Addison-Wesley . inproceedings HR00

2004
[72]

Henzinger & author S.K

author T.A. Henzinger & author S.K. Rajamani ( year 2000 ): title Fair Bisimulation . In editor S. Graf & editor M.I. Schwartzbach , editors: booktitle Proceedings 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems ( TACAS '00) , seri...

2000 doi
[73]

Kant , author A

author G. Kant , author A. Laarman , author J. Meijer , author J. van de Pol , author S. Blom & author T. van Dijk ( year 2015 ): title LTSmin: High-Performance Language-Independent Model Checking . In editor C. Baier & editor C. Tinelli , editors: booktitle Proceedings 21st I...

2015 doi
[74]

Kwiatkowska , author G

author M. Kwiatkowska , author G. Norman & author D. Parker ( year 2010 ): title Advances and Challenges of Probabilistic Model Checking . In: booktitle Proc. 48th Annual Allerton Conference on Communication, Control and Computing , publisher IEEE Press , pp. pages 1691--1698 ...

2010
[75]

Kuiper & author W.-P

author R. Kuiper & author W.-P. de Roever ( year 1983 ): title Fairness Assumptions for CSP in a Temporal Logic Framework . In editor D. Bj rner , editor: booktitle Formal Description of Programming Concepts II , publisher North-Holland , pp. pages 159--170 . article KW97

1983
[76]

Kindler & author R

author E. Kindler & author R. Walter ( year 1997 ): title Mutex Needs Fairness . journal Information Processing Letters volume 62 ( number 1 ), pp. pages 31--39 , doi:10.1016/S0020-0190(97)00033-1. article Lam77

1997 doi
[77]

Lamport ( year 1977 ): title Proving the correctness of multiprocess programs

author L. Lamport ( year 1977 ): title Proving the correctness of multiprocess programs . journal IEEE Transactions on Software Engineering volume 3 ( number 2 ), pp. pages 125--143 , doi:10.1109/TSE.1977.229904. book La02

1977
[78]

Lamport ( year 2002 ): title Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers

author L. Lamport ( year 2002 ): title Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers . publisher Addison-Wesley . inproceedings LPS81

2002
[79]

Lehmann , author A

author D.J. Lehmann , author A. Pnueli & author J. Stavi ( year 1981 ): title Impartiality, Justice and Fairness: The Ethics of Concurrent Termination . In editor S. Even & editor O. Kariv , editors: booktitle Automata, Languages and Programming (ICALP) , series LNCS volume 11...

1981 doi
[80]

Lynch ( year 1968 ): title Reliable full-duplex file transmission over half-duplex telephone line

author W.C. Lynch ( year 1968 ): title Reliable full-duplex file transmission over half-duplex telephone line . journal CACM volume 11 ( number 6 ), pp. pages 407--410 , doi:10.1145/363347.363366. book Ly96

1968
[81]

Lynch ( year 1996 ): title Distributed Algorithms

author N.A. Lynch ( year 1996 ): title Distributed Algorithms . publisher Morgan Kaufmann . book Mi89

1996
[82]

Milner ( year 1989 ): title Communication and concurrency

author R. Milner ( year 1989 ): title Communication and concurrency . series PHI Series in computer science , publisher Prentice Hall . book Mi99

1989
[83]

Milner ( year 1999 ): title Communicating and mobile systems - the Pi-calculus

author R. Milner ( year 1999 ): title Communicating and mobile systems - the Pi-calculus . publisher Cambridge University Press . article MM01

1999
[84]

McIver & author C

author A.K. McIver & author C. Morgan ( year 2001 ): title Demonic, angelic and unbounded probabilistic choices in sequential programs . journal Acta Informatica volume 37 ( number 4/5 ), pp. pages 329--354 , doi:10.1007/s002360000046. article MOP89

2001 doi
[85]

Mazurkiewicz , author E

author A.W. Mazurkiewicz , author E. Ochmanski & author W. Penczek ( year 1989 ): title Concurrent Systems and Inevitability . journal Theoretical Computer Science volume 64 ( number 3 ), pp. pages 281--304 , doi:10.1016/0304-3975(89)90052-2. book Mor94

1989 doi
[86]

Morgan ( year 1994 ): title Programming from specifications , edition 2nd edition

author C. Morgan ( year 1994 ): title Programming from specifications , edition 2nd edition. series Prentice Hall International series in computer science , publisher Prentice Hall . inproceedings NC95

1994
[87]

Natarajan & author R

author V. Natarajan & author R. Cleaveland ( year 1995 ): title Divergence and Fair Testing . In editor Z. F \" u l \" o p & editor F. G \' e cseg , editors: booktitle Proceedings 22nd International Colloquium on Automata, Languages and Programming (ICALP'95) , series LNCS vol...

1995 doi
[88]

Olderog ( year 1991 ): title Nets, Terms and Formulas: Three Views of Concurrent Processes and their Relationship

author E.-R. Olderog ( year 1991 ): title Nets, Terms and Formulas: Three Views of Concurrent Processes and their Relationship . series Cambridge Tracts in Theoretical Computer Science volume 23 , publisher Cambridge University Press , doi:10.1017/CBO9780511526589. misc rfc3561

1991 doi
[89]

Perkins , author E.M

author C.E. Perkins , author E.M. Belding-Royer & author S. Das ( year 2003 ): title Ad hoc On-Demand Distance Vector (AODV) Routing . howpublished RFC 3561, Network Working Group . At\ http://www.ietf.org/rfc/rfc3561.txt. inproceedings Pn77

2003
[90]

Pnueli ( year 1977 ): title The Temporal Logic of Programs

author A. Pnueli ( year 1977 ): title The Temporal Logic of Programs . In: booktitle Foundations of Computer Science (FOCS'77) , publisher IEEE , pp. pages 46--57 , doi:10.1109/SFCS.1977.32. inproceedings Pr91a

1977 doi
[91]

Pratt ( year 1991 ): title Modeling Concurrency with Geometry

author V.R. Pratt ( year 1991 ): title Modeling Concurrency with Geometry . In: booktitle Proc. 18th Annual ACM Symposium on Principles of Programming Languages , pp. pages 311--322 , doi:10.1145/99583.99625. book Rei13

1991
[92]

Reisig ( year 2013 ): title Understanding Petri Nets --- Modeling Techniques, Analysis Methods, Case Studies

author W. Reisig ( year 2013 ): title Understanding Petri Nets --- Modeling Techniques, Analysis Methods, Case Studies . publisher Springer , doi:10.1007/978-3-642-33278-4. book Ros97

2013 doi
[93]

Roscoe ( year 1997 ): title The Theory and Practice of Concurrency

author A.W. Roscoe ( year 1997 ): title The Theory and Practice of Concurrency . publisher Prentice-Hall . ://www.comlab.ox.ac.uk/bill.roscoe/publications/68b.pdf. inproceedings Seg96

1997
[94]

Segala ( year 1996 ): title Testing Probabilistic Automata

author R. Segala ( year 1996 ): title Testing Probabilistic Automata . In: booktitle Proceedings of the 7th International Conference on Concurrency Theory (CONCUR'96) , series LNCS volume 1119 , publisher Springer , pp. pages 299--314 , doi:10.1007/3-540-61604-7_62. article dS85

1996 doi
[95]

de Simone ( year 1985 ): title Higher-level synchronising devices in Meije -SCCS

author R. de Simone ( year 1985 ): title Higher-level synchronising devices in Meije -SCCS . journal Theoretical Computer Science volume 37 , pp. pages 245--267 , doi:10.1016/0304-3975(85)90093-3. book SW01

1985 doi
[96]

Sangiorgi & author D

author D. Sangiorgi & author D. Walker ( year 2001 ): title The -calculus: A Theory of Mobile Processes . publisher Cambridge University Press . inproceedings Ul92

2001
[97]

Ulidowski ( year 1992 ): title Equivalences on Observable Processes

author I. Ulidowski ( year 1992 ): title Equivalences on Observable Processes . In: booktitle Proc.\ Seventh Annual Symposium on Logic in Computer Science (LICS '92) , publisher IEEE Computer Society , pp. pages 148--159 , doi:10.1109/LICS.1992.185529. article Ul00

1992
[98]

Ulidowski ( year 2000 ): title Finite axiom systems for testing preorder and De Simone process languages

author I. Ulidowski ( year 2000 ): title Finite axiom systems for testing preorder and De Simone process languages . journal Theoretical Computer Science volume 239 ( number 1 ), pp. pages 97--139 , doi:10.1016/S0304-3975(99)00214-5. article UP02

2000 doi
[99]

Ulidowski & author I.C.C

author I. Ulidowski & author I.C.C. Phillips ( year 2002 ): title Ordered SOS Process Languages for Branching and Eager Bisimulations . journal Information and Computation volume 178 ( number 1 ), pp. pages 180--213 , doi:10.1006/inco.2002.3161. inproceedings UY00

2002
[100]

Ulidowski & author S

author I. Ulidowski & author S. Yuen ( year 2000 ): title Process Languages for Rooted Eager Bisimulation . In editor C. Pala\-midessi , editor: booktitle Proceedings 11th International Conference on Concurrency Theory ( CONCUR '00) , series LNCS volume 1877 , publisher Spring...

2000 doi
[101]

Verhoef ( year 1995 ): title A Congruence Theorem for Structured Operational Semantics with Predicates and Negative Premises

author C. Verhoef ( year 1995 ): title A Congruence Theorem for Structured Operational Semantics with Predicates and Negative Premises . journal Nord. J. Comput. volume 2 ( number 2 ), pp. pages 274--302 . book Vo92

1995
[102]

Vogler ( year 1992 ): title Modular Construction and Partial Order Semantics of Petri Nets

author W. Vogler ( year 1992 ): title Modular Construction and Partial Order Semantics of Petri Nets . series LNCS volume 625 , publisher Springer , doi:10.1007/3-540-55767-9. article Vo02

1992 doi
[103]

Vogler ( year 2002 ): title Efficiency of asynchronous systems, read arcs, and the MUTEX -problem

author W. Vogler ( year 2002 ): title Efficiency of asynchronous systems, read arcs, and the MUTEX -problem . journal Theoretical Computer Science volume 275 ( number 1-2 ), pp. pages 589--631 , doi:10.1016/S0304-3975(01)00300-0. article Wa90

2002 doi
[104]

Walker ( year 1990 ): title Bisimulation and divergence

author D.J. Walker ( year 1990 ): title Bisimulation and divergence . journal Information and Computation volume 85 ( number 2 ), pp. pages 202--241 , doi:10.1016/0890-5401(90)90048-M. inproceedings Wi84

1990 doi
[105]

Winskel ( year 1984 ): title A new definition of morphism on Petri nets

author G. Winskel ( year 1984 ): title A new definition of morphism on Petri nets . In editor M. Fontet & editor K. Mehlhorn , editors: booktitle Proceedings STACS 84 , series LNCS volume 166 , publisher Springer , pp. pages 140--150 , doi:10.1007/3-540-12920-0_13. inproceedings Wi87a

1984 doi
[106]

Winskel ( year 1987 ): title Event structures

author G. Winskel ( year 1987 ): title Event structures . In editor W. Brauer , editor W. Reisig & editor G. Rozenberg , editors: booktitle Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II , series LNCS volume 255 ...

1987 doi
[107]

Larsen ( year 1992 ): title Testing Probabilistic and Nondeterministic Processes

author Wang Yi & author K.G. Larsen ( year 1992 ): title Testing Probabilistic and Nondeterministic Processes . In: booktitle Proceedings of the IFIP TC6/WG6.1 Twelfth International Symposium on Protocol Specification, Testing and Verification , series IFIP Transactions volume...

1992
[108]

, " * write output.state after.block = add.period write newline

ENTRY address author booktitle chapter doi edition editor eid howpublished institution journal key note number organization pages publisher school series title type url ee volume year label extra.label sort.label INTEGERS output.state before.all mid.sentence after.sentence aft...
[109]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

Pith tools

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

[1] [1]

Austry & author G

author D. Austry & author G. Boudol ( year 1984 ): title Alg\` e bre de processus et synchronisations . journal Theoretical Computer Science volume 30 ( number 1 ), pp. pages 91--131 , doi:10.1016/0304-3975(84)90067-7. article AFK88

doi:10.1016/0304-3975(84)90067-7 1984

[2] [2]

Apt , author N

author K.R. Apt , author N. Francez & author S. Katz ( year 1988 ): title Appraising Fairness in Languages for Distributed Programming . journal Distributed Computing volume 2 ( number 4 ), pp. pages 226--241 , doi:10.1007/BF01872848. book Ba90

doi:10.1007/bf01872848 1988

[3] [3]

Baeten , editor ( year 1990 ): title Applications of Process Algebra

editor J.C.M. Baeten , editor ( year 1990 ): title Applications of Process Algebra . series Cambridge Tracts in Theoretical Computer Science 17 , publisher Cambridge University Press . article BBK87a

1990

[4] [4]

Baeten , author J.A

author J.C.M. Baeten , author J.A. Bergstra & author J.W. Klop ( year 1987 ): title On the Consistency of Koomen's Fair Abstraction Rule . journal Theoretical Computer Science volume 51 ( number 1/2 ), pp. pages 129--176 , doi:10.1016/0304-3975(87)90052-1. book BBR10

work page doi:10.1016/0304-3975(87)90052-1 1987

[5] [5]

Baeten , author T

author J.C.M. Baeten , author T. Basten & author M.A. Reniers ( year 2010 ): title Process Algebra: Equational Theories of Communicating Processes . publisher Cambridge University Press . inproceedings EPTCS54.4

2010

[6] [6]

Buti , author M

author F. Buti , author M. Callisto De Donato , author F. Corradini , author M.R. Di Berardini & author W. Vogler ( year 2011 ): title Automated Analysis of MUTEX Algorithms with FASE . In editor G. D'Agostino & editor S. La Torre , editors: booktitle Proc. GandALF '11 , series EPTCS volume 54 , publisher Open Publishing Association , pp. pages 45--59 , d...

work page doi:10.4204/eptcs.54.4 2011

[7] [7]

Boudol , author I

author G. Boudol , author I. Castellani , author M. Hennessy & author A. Kiehn ( year 1994 ): title A Theory of Processes with Localities . journal Formal Aspects of Computing volume 6 ( number 2 ), pp. pages 165--200 , doi:10.1007/BF01221098. inproceedings BDL04

doi:10.1007/bf01221098 1994

[8] [8]

Behrmann , author A

author G. Behrmann , author A. David & author K.G. Larsen ( year 2004 ): title A Tutorial on Uppaal . In editor M. Bernardo & editor F. Corradini , editors: booktitle Revised Lectures on Formal Methods for the Design of Real-Time Systems , series LNCS volume 3185 , publisher Springer , pp. pages 200--236 , doi:10.1007/978-3-540-30080-9_7. article BFG04

doi:10.1007/978-3-540-30080-9_7 2004