A Game for Linear-time–Branching-time Spectroscopy

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 c...

Descripción completa

Detalles Bibliográficos
Autores principales: Bisping, Benjamin, Nestmann, Uwe
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2021
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979226/
http://dx.doi.org/10.1007/978-3-030-72016-2_1
_version_ 1783667242864476160
author Bisping, Benjamin
Nestmann, Uwe
author_facet Bisping, Benjamin
Nestmann, Uwe
author_sort Bisping, Benjamin
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7979226
institution National Center for Biotechnology Information
language English
publishDate 2021
record_format MEDLINE/PubMed
spelling pubmed-79792262021-03-23 A Game for Linear-time–Branching-time Spectroscopy Bisping, Benjamin Nestmann, Uwe Tools and Algorithms for the Construction and Analysis of Systems Article 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. 2021-03-01 /pmc/articles/PMC7979226/ http://dx.doi.org/10.1007/978-3-030-72016-2_1 Text en © The Author(s) 2021 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Bisping, Benjamin
Nestmann, Uwe
A Game for Linear-time–Branching-time Spectroscopy
title A Game for Linear-time–Branching-time Spectroscopy
title_full A Game for Linear-time–Branching-time Spectroscopy
title_fullStr A Game for Linear-time–Branching-time Spectroscopy
title_full_unstemmed A Game for Linear-time–Branching-time Spectroscopy
title_short A Game for Linear-time–Branching-time Spectroscopy
title_sort game for linear-time–branching-time spectroscopy
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7979226/
http://dx.doi.org/10.1007/978-3-030-72016-2_1
work_keys_str_mv AT bispingbenjamin agameforlineartimebranchingtimespectroscopy
AT nestmannuwe agameforlineartimebranchingtimespectroscopy
AT bispingbenjamin gameforlineartimebranchingtimespectroscopy
AT nestmannuwe gameforlineartimebranchingtimespectroscopy

Ejemplares similares