Abstract
Proof planning is an automated reasoning technique which improves proof search by raising it to a meta-level. In this paper we apply proof planning to First-Order Linear Temporal Logic (FOLTL), which can be seen as a quantified version of Linear Temporal Logic, overcoming its finitary limitation. Automated reasoning in FOLTL is hard, since it is non-recursively enumerable; but its expressiveness can be exploited to precisely model the behaviour of complex, infinite-state systems. In order to demonstrate the potentiality of our technique, we introduce a case-study inspired by the Feature Interactions problem and we model it in FOLTL; we then describe a set of methods which tackle and solve the validation problem for a number of properties of the model; and lastly we present a set of experimental results showing that the methods we propose capture the common patterns in the proofs presented, guide the search at the object level and let the overall system build large and highly structured proofs. This paper to some extent improves over previous work that showed how proof planning can be used to detect such interactions.
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
Abadí, M., Manna, Z.: Nonclausal deduction in first-order temporal logic. Journal of the ACM 37(2), 279–317 (1990)
Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, R., Overbeek, R. (eds.) 9th International Conference on Automated Deduction, pp. 111–120. Springer, Heidelberg (1988); Longer version available from Edinburgh as DAI Research Paper No. 349
Bundy, A.: Proof planning. In: Drabble, B. (ed.) Proceedings of the 3rd International Conference on AI Planning Systems (AIPS) 1996, pp. 261–267 (1996); also available as DAI Research Report 886
Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence 62, 185–253 (1993); Also available from Edinburgh as DAI Research Paper No. 567.
Calder, M., Magill, E.: Feature Interactions in Telecommunications and Software Systems, vol. VI. IOS Press, Amsterdam (2000)
Calder, M., Miller, A.: Automated verification of any number of concurrent, communicating processes. In: Proceedings of the 17th IEEE Automated Software Engineering (ASE 2002), pp. 227–230 (2002)
Calder, M., Kolberg, M., Magill, E.H., Reiff-Marganiec, S.: Feature interaction: A critical review and considered forecast. Computer Networks (2002)
Calder, M., Miller, A.: Using SPIN for feature interaction analysis - A case study. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 143–162. Springer, Heidelberg (2001)
Calder, M., Miller, A.: Feature interaction detection by pairwise analysis of LTL properties. Submitted to FMSD - Formal Methods in Software Development. Still under review at the time of writing (2005) (April 2002)
Castellini, C.: Automated reasoning in quantified modal and temporal logics. PhD thesis, School of Informatics, University of Edinburgh, UK (2005)
Castellini, C., Smaill, A.: Proof planning for feature interactions: a preliminary report. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 102–114. Springer, Heidelberg (2002)
Castellini, C., Smaill, A.: A systematic presentation of quantified modal logics. Logic Journal of the IGPL 10(6), 571–599 (2002)
Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. In: Baader, F. (ed.) Proceedings of CADE-19, International Conference on Automated Deduction, Miami, FL, USA (2003)
Cantu, F.J., Bundy, A., Smaill, A., Basin, D.: Experiments in automating hardware verification using inductive proof planning. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 94–108. Springer, Heidelberg (1996)
Felty, A.: Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning 11(1), 43–81 (1993)
Felty, A.: Temporal logic theorem proving and its application to the feature interaction problem. In: E. Giunchiglia and F. Massacci, editors, Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, number D11 14/01 in Technical Report, University of Siena (2001)
Felty, A.P., Namjoshi, K.S.: Feature specification and automated conflict detection. In: Feature Interactions Workshop, IOS Press, Amsterdam (2000)
Griffeth, N., Blumenthal, R., Gregoire, J.-C., Ohta, T.: A feature interaction benchmark for the first feature interaction detection contest. Computer Networks 1999 32(4), 389–418 (2000)
Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable fragments of first order temporal logics. Annals of Pure and Applied Logic 106, 85–134 (2000)
Holzmann, G.J.: Design and validation of protocols: a tutorial. Computer Networks and ISDN Systems 25(9), 981–1017 (1993); also in: Proc. 11th PSTV 1991, INWG/IFIP, Stockholm, Sweden
Holzmann, G.J.: The model checker spin. IEEE Trans. on Software Engineering 23(5), 279–295 (1997); Special issue on Formal Methods in Software Practice.
Kerber, M.: Proof planning: A practical approach to mechanized reasoning in mathematics. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction, a Basis for Application – Handbook of the German Focus Programme on Automated Deduction, ch. III.4, pp. 77–95. Kluwer Academic Publishers, Dordrecht (1998)
Maclean, E., Fleuriot, J., Smaill, A.: Proof-planning non-standard analysis. In: Proceedings of the Seventh International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida (2002)
Melis, E., Siekmann, J.: Knowledge-based proof planning. Artificial Intelligence 115(1), 65–105 (1999)
Nadathur, G., Miller, D.: Higher-order logic programming. In: Gabbay, D., Hogger, C., Robinson, A. (eds.) Handbook of Logic in AI and Logic Programming. Logic Programming, vol. 5, Springer Verlag, Oxford (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Castellini, C., Smaill, A. (2005). Proof Planning for First-Order Temporal Logic. In: Nieuwenhuis, R. (eds) Automated Deduction – CADE-20. CADE 2005. Lecture Notes in Computer Science(), vol 3632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11532231_17
Download citation
DOI: https://doi.org/10.1007/11532231_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28005-7
Online ISBN: 978-3-540-31864-4
eBook Packages: Computer ScienceComputer Science (R0)