Authors: | Jasper, Marc Schlüter, Maximilian Steffen, Bernhard |
Title: | Characteristic invariants in Hennessy-Milner logic |
Language (ISO): | en |
Abstract: | In this paper, we prove that Hennessy–Milner Logic (HML), despite its structural limitations, is sufficiently expressive to specify an initial property φ0 and a characteristic invariant χI for an arbitrary finite-state process P such that φ0∧AG(χI) is a characteristic formula for P. This means that a process Q, even if infinite state, is bisimulation equivalent to P iff Q⊨φ0∧AG(χI). It follows, in particular, that it is sufficient to check an HML formula for each state of a finite-state process to verify that it is bisimulation equivalent to P. In addition, more complex systems such as context-free processes can be checked for bisimulation equivalence with P using corresponding model checking algorithms. Our characteristic invariant is based on so called class-distinguishing formulas that identify bisimulation equivalence classes in P and which are expressed in HML. We extend Kanellakis and Smolka’s partition refinement algorithm for bisimulation checking in order to generate concise class-distinguishing formulas for finite-state processes. |
URI: | http://hdl.handle.net/2003/40062 http://dx.doi.org/10.17877/DE290R-21942 |
Issue Date: | 2020-05-06 |
Rights link: | https://creativecommons.org/licenses/by/4.0/ |
Appears in Collections: | LS 05 Programmiersysteme |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Jasper2020_Article_CharacteristicInvariantsInHenn.pdf | DNB | 392.65 kB | Adobe PDF | View/Open |
This item is protected by original copyright |
This item is licensed under a Creative Commons License