Characteristic invariants in Hennessy–Milner logic

• Published in: Acta informatica 2020-10, Vol.57 (3-5), p.671-687
• Main Authors: Jasper, Marc, Schlüter, Maximilian, Steffen, Bernhard
• Format: Article
• Language: English
• Subjects: Algorithms; Complex systems; Computer Science; Computer Systems Organization and Communication Networks; Data Structures and Information Theory; Equivalence; Information Systems and Communication Service; Invariants; Logics and Meanings of Programs; Original Article; Software Engineering/Programming and Operating Systems; Theory of Computation
• ISSN: 0001-5903; 1432-0525
• DOI: 10.1007/s00236-020-00376-5

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.