LAUSR

In this paper, we prove that Hennessy–Milner Logic (HML), despite its structural limitations, is sufficiently expressive to specify an initial property $$\varphi _0$$ φ 0 and a characteristic invariant $$\upchi _{_I}$$ χ I for an arbitrary finite-state process P such that $$\varphi _0 \wedge \mathbf{AG }(\upchi _{_I})$$ φ 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 \models \varphi _0 \wedge \mathbf{AG }(\upchi _{_I})$$ 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.