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
Available as PostScript, PDF, DVI.