Ordinal processes in comparative concurrency semantics

Abstract

When comparing concurrency semantics, one of the main difficulties is to find counter-examples to show that two equivalences do not coincide, which takes on considerable proportions if these equivalences coincide in the framework of finitely branching programs. The study of Ordinal Processes of Klop provides us with a wide family of simple counter-examples. The considered semantics are induced by temporal logics CTL, CTL* and Lµ. We pursue this approach by, in addition, considering CCS-like contexts built up from the lyft operators of Groote and Vaandrager.