Testing Hennessy-Milner Logic with Recursion

This study offers a characterization of the collection of propertiesexpressible in Hennessy-Milner Logic (HML) with recursion that can be testedusing finite LTSs. In addition to actions used to probe the behaviour of thetested system, the LTSs that we use as tests will be able to perform a distinguished action nok to signal their dissatisfaction during the interaction with the tested process. A process s passes the test T iff T does not perform the action nok when it interacts with s. A test T tests for a property phi in HML with recursion iff it is passed by exactly the states that satisfy phi. The paper gives an expressive completeness result offering a characterization of the collection of properties in HML with recursion that are testable in the above sense