Abstract
The IEEE standard Property Specification Language (PSL) allows to express all ω-regular properties mixing Linear Temporal Logic (LTL) with Sequential Extended Regular Expressions (SEREs), and is increasingly used in many phases of the hardware design cycle, from specification to verification.
In recent works, we propose a modular and symbolic PSL compilation that is extremely fast in conversion time and outperforms by several orders of magnitude translators based on the explicit construction and minimization of automata. Unfortunately, our approach creates rather redundant automata, which result in a penalty in verification time.
In this paper, we propose a set of syntactic simplifications that enable to significantly improve the verification time without paying the price of automata simplifications. A thorough experimental analysis over large sets of paradigmatic properties shows that our approach drastically reduces the overall verification time.
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.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
IEEE: IEEE standard 1850 – Property Specification Language (PSL) (2005)
Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE Symp. on Foundation of Computer Science, pp. 46–57 (1977)
Ben-David, S., et al.: Automata Construction Algorithms Optimized for PSL. PROSYD deliverable D 3.2/4 (2005), http://www.prosyd.org
Heljanko, K., et al.: Bounded Model Checking for Weak Alternating Büchi Automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 95–108. Springer, Heidelberg (2006)
Bloem, R., et al.: Symbolic Implementation of Alternating Automata. In: Ibarra, O.H., Yen, H.-C. (eds.) CIAA 2006. LNCS, vol. 4094, pp. 208–218. Springer, Heidelberg (2006)
Cimatti, A., et al.: From PSL to NBA: a Modular Symbolic Encoding. In: Procs. of FMCAD06 (2006)
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)
Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321–330 (1984)
Vardi, M.Y., Sebastiani, R., Tonetta, S.: Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 350–363. Springer, Heidelberg (2005)
David, S.B., Orni, A.: Property-by-Example guide: a handbook of PSL/Sugar examples. PROSYD deliverable D 1.1/3 (2005), http://www.prosyd.org
Beer, I., et al.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)
Vardi, M.Y., et al.: Resets vs. Aborts in Linear Temporal Logic. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 65–80. Springer, Heidelberg (2003)
Somenzi, F., Bloem, R.: Efficient Büchi Automata from LTL Formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 247–263. Springer, Heidelberg (2000)
Etessami, K., Holtzmann, G.: Optimizing Büchi Automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, Springer, Heidelberg (2000)
Clarke, E., et al.: NUSMV: A New Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Heljanko, K., Junttila, T.A., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98–111. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Cimatti, A., Roveri, M., Tonetta, S. (2007). Syntactic Optimizations for PSL Verification. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_39
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)