Deciding all behavioral equivalences at once: a game for linear-time-branching-time spectroscopy

MaRDI QIDQ5101352zbMATH OpenFDO

Authors Benjamin Bisping, David N. Jansen, Uwe Nestmann

Publication date 30 August 2022

Full work available at URL https://arxiv.org/abs/2109.15295, https://lmcs.episciences.org/9905

zbMATH Keywords

bisimulation gamedistinguishing formulasprocess equivalence spectrum

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• A game for linear-time-branching-time spectroscopy
• Process equivalence problems as energy games
• A Linear-Time–Branching-Time Spectrum of Behavioral Specification Theories
• A linear-time-branching-time spectrum for behavioral specification theories
• Explaining non-bisimilarity in a coalgebraic approach: games and distinguishing formulas

Cites work

• A game for linear-time-branching-time spectroscopy
• Algebraic laws for nondeterminism and concurrency
• Characteristic invariants in Hennessy-Milner logic
• Congruence from the operator's point of view. Syntactic requirements on modal characterizations
• Coupled similarity: the first 32 years
• Explaining non-bisimilarity in a coalgebraic approach: games and distinguishing formulas
• Finite model theory and its applications.
• Games for bisimulations and abstraction
• scientific article; zbMATH DE number 3688686 (Why is no real title available?)
• scientific article; zbMATH DE number 177532 (Why is no real title available?)
• scientific article; zbMATH DE number 1142329 (Why is no real title available?)
• scientific article; zbMATH DE number 1916666 (Why is no real title available?)
• scientific article; zbMATH DE number 1424056 (Why is no real title available?)
• scientific article; zbMATH DE number 7730634 (Why is no real title available?)
• Minimal separating sequences for all pairs of states
• Model-checking process equivalences
• Relating apartness and bisimulation
• Revivals, stuckness and the hierarchy of CSP models
• Simulation distances
• Testing equivalence as a bisimulation equivalence
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• Unifying the linear time-branching time spectrum of process semantics

Cited in

(10)

• A game for linear-time-branching-time spectroscopy
• Explaining non-bisimilarity in a coalgebraic approach: games and distinguishing formulas
• When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
• scientific article; zbMATH DE number 7730634 (Why is no real title available?)
• Process equivalence problems as energy games
• Characterizing contrasimilarity through games, modal logic, and complexity
• Preorder-constrained simulations for program refinement with effects
• One energy game for the spectrum between branching bisimilarity and weak trace semantics
• Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable
• Galois Energy Games

Describes a project that uses

Uses Software

• GitHub

This page was built for publication: Deciding all behavioral equivalences at once: a game for linear-time-branching-time spectroscopy

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