All linear-time congruences for familiar operators

DOI10.2168/LMCS-9(4:11)2013MaRDI QIDQ2865064zbMATH OpenFDO

Authors Antti Valmari

Publication date 28 November 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

verificationsemanticsprocess algebracompositionality

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

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

Cited in

(3)

• All Linear-Time Congruences for Familiar Operators Part 2: Infinite LTSs
• All congruences below stability-preserving fair testing or CFFD
• On constructibility and unconstructibility of LTS operators from other LTS operators

Describes a project that uses

Uses Software

• LOTOS

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)