Photo from archive.org
We enrich the operational semantics of a simple process calculus with ACP-style communication with a concurrency relation, so that for every process expression there exists an associated notion of just… Click to show full abstract
We enrich the operational semantics of a simple process calculus with ACP-style communication with a concurrency relation, so that for every process expression there exists an associated notion of just path . We then present sufficient conditions on the communication function and the syntax of process expressions that facilitate the formulation of justness on the level of labels rather than on individual transitions, taking a designated set of signals into account. This paves the way for the formulation of liveness properties under justness assumptions in the modal $$\mu $$ μ -calculus and their verification on process specifications with the mCRL2 toolset.
Journal Title: Acta Informatica
Year Published: 2020
Link to full text (if available)
Share on Social Media: Sign Up to like & get
recommendations!