Abstract
We present a collection of command-line tools designed to generate, filter, convert, simplify, lists of Linear-time Temporal Logic formulas. These tools were introduced in the release 1.0 of Spot, and we believe they should be of interest to anybody who has to manipulate LTL formulas. We focus on two tools in particular: ltlfilt, to filter and transform formulas, and ltlcross to cross-check LTL-to-Büchi-Automata translators.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Property Specification Language Reference Manual v1.1. Accellera (June 2004), http://www.eda.org/vfv/
Ben Salem, A.-E., Duret-Lutz, A., Kordon, F.: Model checking using generalized testing automata. In: Jensen, K., van der Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency VI. LNCS, vol. 7400, pp. 94–122. Springer, Heidelberg (2012)
Dax, C., Eisinger, J., Klaedtke, F.: Mechanizing the powerset construction for restricted classes of ω-automata. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 223–236. Springer, Heidelberg (2007)
Duret-Lutz, A.: LTL translation improvements in Spot. In: Proc. of VECoS 2011. British Computer Society (September 2011), http://ewic.bcs.org/category/15853
Duret-Lutz, A., Poitrenaud, D.: SPOT: An Extensible Model Checking Library using Transition-based Generalized Büchi Automata. In: Proc. of MASCOTS 2004, pp. 76–83. IEEE Computer Society Press (October 2004)
Etessami, K.: A note on a question of Peled and Wilke regarding stutter-invariant LTL. Information Processing Letters 75(6), 261–263 (2000)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley (2003)
Klein, J., Baier, C.: Experiments with deterministic ω-automata for formulas of linear temporal logic. Theoretical Computer Science 363(2), 182–195 (2006)
Latvala, T.: Efficient model checking of safety properties. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 74–88. Springer, Heidelberg (2003)
Somenzi, F., Bloem, R.: Efficient Büchi automata for LTL formulæ. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 247–263. Springer, Heidelberg (2000)
Tauriainen, H., Heljanko, K.: Testing LTL formula translation into Büchi automata. International Journal on Software Tools for Technology Transfer 4(1), 57–70 (2002)
Tsay, Y.K., Chen, Y.F., Tsai, M.H., Wu, K.N., Chan, W.C., Luo, C.J., Chang, J.S.: Tool support for learning büchi automata and linear temporal logic. Formal Aspects of Computing 21(3), 259–275 (2009)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Duret-Lutz, A. (2013). Manipulating LTL Formulas Using Spot 1.0. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-02444-8_31
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02443-1
Online ISBN: 978-3-319-02444-8
eBook Packages: Computer ScienceComputer Science (R0)