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 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.