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.
Issue Date: 2020-05-06
Rights link:
Appears in Collections:LS 05 Programmiersysteme

Files in This Item:
File Description SizeFormat 
Jasper2020_Article_CharacteristicInvariantsInHenn.pdfDNB392.65 kBAdobe PDFView/Open

This item is protected by original copyright

This item is licensed under a Creative Commons License Creative Commons