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.
The work reported in this paper was mostly carried out during the authors’ stay at the Dipartimento di Sistemi ed Informatica, Università di Firenze, Italy.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
L. Aceto, P. Bouyer, A. BurgueÑo, and K. G. Larsen, The power of reachability testing for timed automata, in Proceedings of the Eighteenth Conference on the Foundations of Software Technology and Theoretical Computer Science, V. Arvind and R. Ramanujam, eds., Lecture Notes in Computer Science, Springer-Verlag, December 1998.
L. Aceto, A. BurgueÑo, and K. G. Larsen, Model checking via reachability testing for timed automata, in Proceedings of TACAS’ 98, Lisbon, B. Steffen, ed., vol. 1384 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 263–280.
H. R. Andersen, Partial model checking (extended abstract), in Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science, San Diego, California, 26-29 June 1995, IEEE Computer Society Press, pp. 398–407.
R. De Nicola and M. Hennessy, Testing equivalences for processes, Theoretical Comput. Sci., 34 (1984), pp. 83–133.
D. M. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, On the temporal basis of fairness, in Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, Jan. 1980, pp. 163–173.
M. Hennessy, Algebraic Theory of Processes, MIT Press, Cambridge, Massachusetts, 1988.
M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach., 32 (1985), pp. 137–161.
R. Keller, Formal verification of parallel programs, Comm. ACM, 19 (1976), pp. 371–384.
S. Kleene, Representation of events in nerve nets and finite automata, in Automata Studies, C. Shannon and J. McCarthy, eds., Princeton University Press, 1956, pp. 3–41.
D. Kozen, Results on the propositional mu-calculus, Theoretical Comput. Sci., 27 (1983), pp. 333–354.
F. Laroussinie, K. G. Larsen, and C. Weise, From timed automata to logic-and back, in Mathematical Foundations of Computer Science 1995, 20th International Symposium, J. Wiedermann and P. Hájek, eds., vol. 969 of Lecture Notes in Computer Science, Prague, Czech Republic, 28 Aug.-1 Sept. 1995, Springer-Verlag, pp. 529–539.
K. G. Larsen and L. Xinxin, Compositionality through an operational semantics of contexts, Journal of Logic and Computation, 1 (1991), pp. 761–795.
R. Milner, Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.
D. Park, Concurrency and automata on infinite sequences, in 5th GI Conference, Karlsruhe, Germany, P. Deussen, ed., vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167–183.
A. Stoughton, Substitution revisited, Theoretical Comput. Sci., 59 (1988), pp. 317–325.
A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, 5 (1955), pp. 285–309.
M. Y. Vardi and P. Wolper, Reasoning about infinite computations, Information and Computation, 115 (1994), pp. 1–37.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., Ingólfsdóttir, A. (1999). Testing Hennessy-Milner Logic with Recursion. In: Thomas, W. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 1999. Lecture Notes in Computer Science, vol 1578. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49019-1_4
Download citation
DOI: https://doi.org/10.1007/3-540-49019-1_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65719-4
Online ISBN: 978-3-540-49019-7
eBook Packages: Springer Book Archive