Abstract
The paper discusses the merits of temporal testers, which can serve as a compositional basis for automata construction corresponding to temporal formulas in the context of ltl, psl, and mitl logics. Temporal testers can be viewed as (non-deterministic) transducers that, at any point, output a boolean value which is 1 iff the corresponding temporal formula holds starting at the current position.
The main advantage of testers, compared to acceptors (such asBüchi automata) is their compositionality. Namely, a tester for a compound formula can be constructed out of the testers for its sub-formulas. Besides providing the construction of testers for formulas specified in ltl, psl, and mitl, the paper also presents a general overview of the tester methodology, and highlights some of the unique features and applications of transducers including compositional deductive verification of ltl properties.
This research was supported in part by the European community project Prosyd, ONR grant N00014-99-1-0131, and SRC grant 2004-TJ-1256.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Accellera Organization, Inc. Property Specification Language Reference Manual, Version 1.01 (2003), http://www.accellera.org/
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. In: Symposium on Principles of Distributed Computing, pp. 139–152 (1991)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press (2000)
Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. Journal of the ACM 49(2), 172–206 (2002)
Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of ACM 28(1), 114–133 (1981)
Cimatti, A., Roveri, M., Semprini, S., Tonetta, S.: From PSL to NBA: a modular symbolic encoding, pp. 125–133 (2006)
Bustan, D., Fisman, D., Havlicek, J.: Automata Construction for PSL (2005), http://www.wisdom.weizmann.ac.il/~dana/publicat/automta_constructionTR.pdf
Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata, pp. 73–81
Eisner, C., Fisman, D., Havlicek, J., Gordon, M., McIsaac, A., Van Campenhout, D.: Formal Syntax and Semantics of PSL (2003), http://www.wisdom.weizmann.ac.il/~dana/publicat/formal_semantics_standalone.pdf
Gabbay, D.: The declarative past and imperative future. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification, vol. 398, pp. 407–448 (1987)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison Wesley, Reading (1979)
Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 1–16. Springer, Heidelberg (1998)
Kesten, Y., Pnueli, A.: A compositional approach to CTL* verification. Theoretical Computer Science 331, 397–428 (2005)
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL 1985: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 97–107. ACM Press, New York (1985)
Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006)
Manna, Z., Pnueli, A.: Completing the temporal picture. Theoretical Computer Science 83(1), 97–130 (1991)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification, New York (1991)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)
Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)
Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)
Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. Technical Report, Dept. of Computer Science, New York University (2006)
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking for Real-Time Systems. In: 7th. Symposium of Logics in Computer Science, Santa-Cruz, California, pp. 394–406. IEEE Computer Scienty Press (1992)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. Proc. First IEEE Symp. Logic in Comp. Sci., 332–344 (1986)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Pnueli, A., Zaks, A. (2008). On the Merits of Temporal Testers. In: Grumberg, O., Veith, H. (eds) 25 Years of Model Checking. Lecture Notes in Computer Science, vol 5000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69850-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-69850-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69849-4
Online ISBN: 978-3-540-69850-0
eBook Packages: Computer ScienceComputer Science (R0)