Simplified Coalgebraic Trace Equivalence

TL;DR

This paper introduces a simplified coalgebraic framework for trace equivalence that unifies various existing approaches and extends to systems without explicit termination, including standard LTS and probabilistic systems.

Contribution

It presents a generalized coalgebraic approach to trace equivalence using embedding functors into a global monad, covering more system types than previous methods.

Findings

Unifies existing coalgebraic trace equivalence approaches

Extends applicability to systems without explicit termination

Includes standard LTS and probabilistic systems

Abstract

The analysis of concurrent and reactive systems is based to a large degree on various notions of process equivalence, ranging, on the so-called linear-time/branching-time spectrum, from fine-grained equivalences such as strong bisimilarity to coarse-grained ones such as trace equivalence. The theory of concurrent systems at large has benefited from developments in coalgebra, which has enabled uniform definitions and results that provide a common umbrella for seemingly disparate system types including non-deterministic, weighted, probabilistic, and game-based systems. In particular, there has been some success in identifying a generic coalgebraic theory of bisimulation that matches known definitions in many concrete cases. The situation is currently somewhat less settled regarding trace equivalence. A number of coalgebraic approaches to trace equivalence have been proposed, none of which however cover all cases of interest; notably, all these approaches depend on explicit termination, which is not always imposed in standard systems, e.g. LTS. Here, we discuss a joint generalization of these approaches based on embedding functors modelling various aspects of the system, such as transition and braching, into a global monad; this approach appears to cover all cases considered previously and some additional ones, notably standard LTS and probabilistic labelled transition systems.