Email Gateway (Nov 22 2025 at 09:28): Email Gateway (Nov 22 2025 at 09:28):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
A new entry that increases the number of authors on our statistics page by 4. Unlike the short title suggests, the entry is more computer science than physics. In particular, it is not formalizing a method for detecting oxygen on exoplanets (https://xkcd.com/1517):
The Weak Spectroscopy Game to Characterize Behavioral Equivalences
by Lisa A. Barthel, Leonard M. Hübner, Caroline Lemke, Karl P. P. Mattes, Lenard Mollenkopf, and Benjamin Bisping
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.
https://www.isa-afp.org/entries/Weak_Spectroscopy.html
Enjoy!
Last updated: Dec 02 2025 at 16:32 UTC