All linear-time congruences for familiar operators
From MaRDI portal
Publication:2865064
DOI10.2168/LMCS-9(4:11)2013zbMATH Open1314.68201arXiv1310.8408MaRDI QIDQ2865064FDOQ2865064
Authors: Antti Valmari 
Publication date: 28 November 2013
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Abstract: The detailed behaviour of a system is often represented as a labelled transition system (LTS) and the abstract behaviour as a stuttering-insensitive semantic congruence. Numerous congruences have been presented in the literature. On the other hand, there have not been many results proving the absence of more congruences. This publication fully analyses the linear-time (in a well-defined sense) region with respect to action prefix, hiding, relational renaming, and parallel composition. It contains 40 congruences. They are built from the alphabet, two kinds of traces, two kinds of divergence traces, five kinds of failures, and four kinds of infinite traces. In the case of finite LTSs, infinite traces lose their role and the number of congruences drops to 20. The publication concentrates on the hardest and most novel part of the result, that is, proving the absence of more congruences.
Full work available at URL: https://arxiv.org/abs/1310.8408
Recommendations
- All Linear-Time Congruences for Familiar Operators Part 2: Infinite LTSs
- All congruences below stability-preserving fair testing or CFFD
- Structured operational semantics and bisimulation as a congruence
- On constructibility and unconstructibility of LTS operators from other LTS operators
- Congruence from the operator's point of view: compositionality requirements on process semantics
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cited In (3)
Uses Software
This page was built for publication: All linear-time congruences for familiar operators
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2865064)
