Testing hennessy-milner logic with recursion?

Abstract

This study offers a characterization of the collection of properties expressible in Hennessy-Milner Logic (HML) with recursion that can be tested using finite LTSs. In addition to actions used to probe the behaviour of the tested 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 ϕ in HML with recursion iff it is passed by exactly the states that satisfy ϕ. 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.