The Weak Spectroscopy Game to Characterize Behavioral Equivalences (Q7361664)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Weak_Spectroscopy
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | The Weak Spectroscopy Game to Characterize Behavioral Equivalences |
AFP entry Weak_Spectroscopy |
Statements
17 November 2025
0 references
Lisa A. Barthel
0 references
Leonard M. Hübner
0 references
Caroline Lemke
0 references
Karl P. P. Mattes
0 references
Lenard Mollenkopf
0 references
Benjamin Bisping
0 references
The Weak Spectroscopy Game to Characterize Behavioral Equivalences (English)
0 references
We provide an Isabelle/HOL formalization of Bisping and Jansen's weak spectroscopy game (2024), which can be used to simultaneously characterize and decide a hierarchy of behavioral equivalences for systems with internal behavior. This is valuable for applications in concurrency theory and formal verification where equivalences and distinctions of the “linear-time–branching-time spectrum” are a recurring topic. This entry contains a game characterization of most behavioral equivalences from stability-respecting branching bisimilarity to weak trace equivalence. Technically, the results link distinguishing sublanguages of Hennessy–Milner logic to winning attacker budgets in an energy game through an eight-dimensional measurement of syntactic features appearing in formulas.
0 references
0 references
0 references
