The Weak Spectroscopy Game to Characterize Behavioral Equivalences

Lisa A. Barthel, Leonard M. Hübner, Caroline Lemke 📧, Karl P. P. Mattes, Lenard Mollenkopf and Benjamin Bisping 🌐

November 17, 2025

Abstract

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.

License

GNU Lesser General Public License (LGPL)

Topics

Related publications

  • Bisping, B., & Jansen, D. N. (2024). One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics. Electronic Proceedings in Theoretical Computer Science, 412, 71–88. https://doi.org/10.4204/eptcs.412.6
  • Bisping, B., & Jansen, D. N. (2023). Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps (Version 3). arXiv. https://doi.org/10.48550/ARXIV.2305.17671
  • Bisping, B. (2023). Process Equivalence Problems as Energy Games. Computer Aided Verification, 85–106. https://doi.org/10.1007/978-3-031-37706-8_5
  • van Glabbeek, R. J. (1990). The linear time - branching time spectrum. CONCUR ’90 Theories of Concurrency: Unification and Extension, 278–297. https://doi.org/10.1007/bfb0039066
  • Benjamin Bisping. Generalized Equivalence Checking of Concurrent Programs. PhD thesis, Technische Universität Berlin, 2025. https://generalized-equivalence-checking.equiv.io/

Session Weak_Spectroscopy

Cite

× 
@article{Weak_Spectroscopy-AFP,
  author  = {Lisa A. Barthel and Leonard M. Hübner and Caroline Lemke and Karl P. P. Mattes and Lenard Mollenkopf and Benjamin Bisping},
  title   = {The Weak Spectroscopy Game to Characterize Behavioral Equivalences},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/Weak_Spectroscopy.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download