Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-05T16:34:14.145Z Has data issue: false hasContentIssue false
  • English
  • Français

Transformations of logic programs on infinite lists

Published online by Cambridge University Press:  09 July 2010

ALBERTO PETTOROSSI ,
MAURIZIO PROIETTI  and
VALERIO SENNI
ALBERTO PETTOROSSI
Affiliation:
DISP, University of Rome Tor Vergata, Via del Politecnico 1, I-00133 Rome, Italy (e-mail: [email protected])
MAURIZIO PROIETTI
Affiliation:
IASI-CNR, Viale Manzoni 30, I-00185 Rome, Italy (e-mail: [email protected])
VALERIO SENNI
Affiliation:
DISP, University of Rome Tor Vergata, Via del Politecnico 1, I-00133 Rome, Italy (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

We consider an extension of logic programs, called ω-programs, that can be used to define predicates over infinite lists. ω-programs allow us to specify properties of the infinite behavior of reactive systems and, in general, properties of infinite sequences of events. The semantics of ω-programs is an extension of the perfect model semantics. We present variants of the familiar unfold/fold rules which can be used for transforming ω-programs. We show that these new rules are correct, that is, their application preserves the perfect model semantics. Then we outline a general methodology based on program transformation for verifying properties of ω-programs. We demonstrate the power of our transformation-based verification methodology by proving some properties of Büchi automata and ω-regular languages.

Keywords

program transformationprogram verificationinfinite lists
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 10 , Special Issue 4-6: 26th International Conference on Logic Programming , July 2010 , pp. 383 - 399
Copyright
Copyright © Cambridge University Press 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M. and Manna, Z. 1989. Temporal logic programming. Journal of Symbolic Computation 8, 3, 277–295.CrossRefGoogle Scholar
Apt, K. R. and Bol, R. N. 1994. Logic programming and negation: A survey. Journal of Logic Programming 19, 20, 9–71.CrossRefGoogle Scholar
Burstall, R. M. and Darlington, J. 1977. A transformation system for developing recursive programs. Journal of the ACM 24, 1 (January), 44–67.CrossRefGoogle Scholar
Clarke, E. M., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press.Google Scholar
Colmerauer, A. 1982. Prolog and infinite trees. In Logic Programming, Clark, K. L. and Tärnlund, S.-Å., Eds. Academic Press, 231–251.Google Scholar
Delzanno, G. and Podelski, A. 2001. Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer 3, 3, 250–270.CrossRefGoogle Scholar
Etalle, S., Gabbrielli, M., and Meo, M. C. 2001. Transformations of CCP programs. ACM Transactions on Programming Languages and Systems 23, 3, 304–395.CrossRefGoogle Scholar
Fioravanti, F., Pettorossi, A., and Proietti, M. 2004. Transformation rules for locally stratified constraint logic programs. In Program Development in Computational Logic, Lau, K.-K. and Bruynooghe, M., Eds. Lecture Notes in Computer Science, vol. 3049. Springer, 292–340.Google Scholar
Fribourg, L. and Olsén, H. 1997. A decompositional approach for computing least fixed-points of Datalog programs with Z-counters. Constraints 2, 3/4, 305–335.CrossRefGoogle Scholar
Gupta, G., Bansal, A., Min, R., Simon, L., and Mallya, A. 2007. Coinductive logic programming and its applications. In Proceedings ICLP'07, Porto, Portugal, Dahl, V. and Niemelä, I., Eds. Lecture Notes in Computer Science, vol. 4670. Springer, 27–44.Google Scholar
Jaffar, J., Santosa, A. E., and Voicu, R. 2004. A CLP proof method for timed automata. In The 25th IEEE International Real-Time Systems Symposium, Anderson, J. and Sztipanovits, J., Eds. IEEE Computer Society, 175–186.CrossRefGoogle Scholar
Leuschel, M. and Massart, T. 2000. Infinite state model checking by abstract interpretation and program specialization. In Proceedings LOPSTR'99, Venezia, Italy, Bossi, A., Ed. Lecture Notes in Computer Science, vol. 1817. Springer, 63–82.Google Scholar
Lloyd, J. W. 1987. Foundations of Logic Programming, 2nd ed.Springer, Berlin.CrossRefGoogle Scholar
Min, R. and Gupta, G. 2010. Coinductive logic programming with negation. In Proc. LOPSTR'09, Coimbra, Portugal, De Schreye, D., Ed. Lecture Notes in Computer Science, vol. 6037. Springer, 97–112.Google Scholar
Nilsson, U. and Lübcke, J. 2000. Constraint logic programming for local and symbolic model-checking. In Proceedings CL 2000, London, UK, Lloyd, J. W., Ed. Lecture Notes in Artificial Intelligence, vol. 1861. Springer, 384–398.Google Scholar
Pettorossi, A. and Proietti, M. 2000. Perfect model checking via unfold/fold transformations. In Proceedings CL 2000, London, UK, Lloyd, J. W., Ed. Lecture Notes in Artificial Intelligence, vol. 1861. Springer, 613–628.Google Scholar
Pettorossi, A., Proietti, M., and Senni, V. 2010. Deciding full branching time logic by program transformation. In Proc. LOPSTR'09, Coimbra, Portugal, De Schreye, D., Ed. Lecture Notes in Computer Science, vol. 6037. Springer, 5–21.Google Scholar
Pettorossi, A., Proietti, M., and Senni, V. 2010. Transformations of logic programs on infinite lists. Technical Report R. 10-04, IASI-CNR, Roma, Italy.CrossRefGoogle Scholar
Proietti, M. and Pettorossi, A. 1995. Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theoretical Computer Science 142, 1, 89–124.CrossRefGoogle Scholar
Ramakrishna, Y. S., Ramakrishnan, C. R., Ramakrishnan, I. V., Smolka, S. A., Swift, T., and Warren, D. S. 1997. Efficient model checking using tabled resolution. In Proc. CAV'97. Lecture Notes in Computer Science, vol. 1254. Springer, 143–154.Google Scholar
Roychoudhury, A., Kumar, K. N., Ramakrishnan, C. R., and Ramakrishnan, I. V. 2002. Beyond Tamaki-Sato style unfold/fold transformations for normal logic programs. International Journal on Foundations of Computer Science 13, 3, 387–403.CrossRefGoogle Scholar
Seki, H. 1991. Unfold/fold transformation of stratified programs. Theoretical Computer Science 86, 107–139.CrossRefGoogle Scholar
Seki, H. 2010. On inductive and coinductive proofs via unfold/fold transformations. In Proc. LOPSTR'09, Coimbra, Portugal, De Schreye, D., Ed. Lecture Notes in Computer Science, vol. 6037. Springer, 82–96.Google Scholar
Simon, L., Mallya, A., Bansal, A., and Gupta, G. 2006. Coinductive logic programming. In Proceedings ICLP'06, Seattle, USA, Etalle, S. and Truszczyński, M., Eds. Lecture Notes in Computer Science, vol. 4079. Springer, 330–345.Google Scholar
Staiger, L. 1997. ω-Languages. In Handbook of Formal Languages, Rozenberg, G. and Salomaa, A., Eds, vol. 3. Springer, Berlin, 339–387.CrossRefGoogle Scholar
Tamaki, H. and Sato, T. 1984. Unfold/fold transformation of logic programs. In Proceedings ICLP'84, Tärnlund, S.-Å., Ed. Uppsala University, Uppsala, Sweden, 127–138.Google Scholar
Thomas, W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, Van Leeuwen, J., Ed. Vol. B. Elsevier, Amsterdam, 135–191.Google Scholar
Ueda, K. and Furukawa, K. 1988. Transformation rules for GHC programs. In Proceedings International Conference on Fifth Generation Computer Systems, ICOT, Tokyo, Japan, 582–591.Google Scholar