Abstract
We introduce a generalization of the bisimulation game that can be employed to find all relevant distinguishing Hennessy–Milner logic formulas for two compared finite-state processes. By measuring the use of expressive powers, we adapt the formula generation to just yield formulas belonging to the coarsest distinguishing behavioral preorders/equivalences from the linear-time–branching-time spectrum. The induced algorithm can determine the best fit of (in)equivalences for a pair of processes.
Author supplied keywords
Cite
CITATION STYLE
Bisping, B., & Nestmann, U. (2021). A Game for Linear-time–Branching-time Spectroscopy. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12651 LNCS, pp. 3–19). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-72016-2_1
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
