Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps
Logic in Computer Science
2024-10-08 v3 Computer Science and Game Theory
Abstract
We provide the first generalized game characterization of van Glabbeek's linear-time--branching-time spectrum with silent steps. Thereby, one multi-dimensional energy game can be used to characterize and decide a wide array of weak behavioral equivalences between stability-respecting branching bisimilarity and weak trace equivalence in one go. To establish correctness, we relate attacker-winning energy budgets and distinguishing sublanguages of Hennessy--Milner logic that we characterize by eight dimensions of formula expressiveness.
Cite
@article{arxiv.2305.17671,
title = {Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps},
author = {Benjamin Bisping and David N. Jansen},
journal= {arXiv preprint arXiv:2305.17671},
year = {2024}
}