Simplified coalgebraic trace equivalence

DOI10.1007/978-3-319-15545-6_8zbMATH Open1453.68112arXiv1410.2463OpenAlexW1951729275MaRDI QIDQ5256339FDOQ5256339

Authors: Stefan Milius, Dirk Pattinson, Lutz Schröder, Alexander Kurz 

Publication date: 22 June 2015

Published in: Software, Services, and Systems (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1410.2463

Recommendations

• A coalgebraic approach to process equivalence and a coinduction principle for traces
• Generic trace semantics and graded monads
• A coalgebraic view on decorated traces
• scientific article; zbMATH DE number 1497803
• Steps and traces

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Coequalizers and free triples
• Sound and complete axiomatizations of coalgebraic language equivalence
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Generic Trace Semantics via Coinduction
• On the final sequence of a finitary set functor
• Title not available (Why is that?)
• Reactive Systems
• Title not available (Why is that?)
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Title not available (Why is that?)
• An introduction to measure theory
• Generalizing the powerset construction, coalgebraically
• Generalizing determinization from automata to coalgebras
• Title not available (Why is that?)
• Trace semantics via determinization
• A coalgebraic approach to linear-time logics
• Final semantics for decorated traces

Cited In (10)

• Final semantics for decorated traces
• Iterated covariant powerset is not a monad
• Coalgebraic Infinite Traces and Kleisli Simulations
• A coalgebraic view on decorated traces
• Steps and traces
• Generic trace semantics and graded monads
• A coalgebraic approach to process equivalence and a coinduction principle for traces
• Coalgebraic trace semantics for combined possibilitistic and probabilistic systems
• Graded semantics and graded logics for Eilenberg-Moore coalgebras
• Coalgebraic trace semantics via forgetful logics

This page was built for publication: Simplified coalgebraic trace equivalence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5256339)