6  Spectroscopy for the Weak Silent-Step Spectrum

Todo

This section will be filled, once the journal version of One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics is ready.

6.1 Lifting to the Spectrum of Stable Equivalences

6.1.1 Stable Behavioral Equivalences

6.1.2 The Adapted Spectroscopy Game

6.2 The Weak Spectrum

6.2.1 Special Weak Equivalences

6.2.2 HML with Silent Behavior

6.2.3 Expressing the Weak Spectrum with Quantities

6.3 The Weak Spectroscopy Game

6.3.1 The Game

6.3.2 Correctness

6.4 Discussion

• Mention to add back in strong observations