Off-the-shelf automated analysis of liveness properties for just paths

Mark Bouwman, Bas Luttik (Corresponding author), Tim Willemse

Research output: Contribution to journalArticleAcademicpeer-review

9 Citations (Scopus)


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 μ-calculus and their verification on process specifications with the mCRL2 toolset.

Original languageEnglish
Pages (from-to)551-590
Number of pages40
JournalActa Informatica
Issue number3-5
Publication statusPublished - 1 Oct 2020


Dive into the research topics of 'Off-the-shelf automated analysis of liveness properties for just paths'. Together they form a unique fingerprint.

Cite this