Testing Hennessy-Milner Logic with Recursion

Luca Aceto
Anna Ingólfsdóttir

December 1998


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 tex2html_wrap_inline34 in HML with recursion iff it is passed by exactly the states that satisfy tex2html_wrap_inline34. 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.


Last modified: 2003-06-08 by webmaster.