Skip to main content
SpringerLink
Log in

Combining Logic Programs and Monadic Second Order Logics by Program Transformation

  • Conference paper
  • First Online:
Logic Based Program Synthesis and Transformation (LOPSTR 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2664))

Abstract

We present a program synthesis method based on unfold/fold transformation rules which can be used for deriving terminating definite logic programs from formulas of the Weak Monadic Second Order theory of one successor (WS1S). This synthesis method can also be used as a proof method which is a decision procedure for closed formulas of WS1S. We apply our synthesis method for translating CLP(WS1S) programs into logic programs and we use it also as a proof method for verifying safety properties of infinite state systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K. R. Apt and R. N. Bol. Logic programming and negation: A survey. Journal of Logic Programming, 19, 20:9–71, 1994.

    Article  MathSciNet  Google Scholar 

  2. D. Basin and S. Friedrich. Combining WS1S and HOL. In D.M. Gabbay and M. de Rijke (eds.), Frontiers of Combining Systems 2, volume 7 of Studies in Logic and Computation, pp. 39–56. Research Studies Press/Wiley, 2000.

    Google Scholar 

  3. D. Basin and N. Klarlund. Automata based symbolic reasoning in hardware verification. The Journal of Formal Methods in Systems Design, 13(3):255–288, 1998.

    Article  Google Scholar 

  4. J. R. Büchi. Weak second order arithmetic and and finite automata. Z. Maath Logik Grundlagen Math, 6:66–92, 1960.

    Article  MATH  Google Scholar 

  5. W. Chen and D. S. Warren. Tabled evaluation with delaying for general logic programs. JACM, 43(1), 1996.

    Google Scholar 

  6. G. Delzanno and A. Podelski. Model checking in CLP. In R. Cleaveland (ed.), Proc. TACAS’99, LNCS 1579, pp. 223–239. Springer, 1999.

    Google Scholar 

  7. F. Fioravanti, A. Pettorossi, and M. Proietti. Verification of sets of infinite state systems using program transformation. In A. Pettorossi (ed.), Proc. LOPSTR 2001, LNCS 2372, pp. 111–128. Springer, 2002.

    Google Scholar 

  8. L. Fribourg and H. Olsén. Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In Proc. CONCUR’ 97, LNCS 1243, pp. 96–107. Springer, 1997.

    Google Scholar 

  9. J. G. Henriksen, J. L. Jensen, M. E. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In E. Brinksma et al. (eds.), Proc. TACAS’ 95, LNCS 1019, pp. 89–110. Springer, 1996.

    Google Scholar 

  10. J. Jaffar and M. Maher. Constraint logic programming: A survey. Journal of Logic Programming, 19/20:503–581, 1994.

    Article  MathSciNet  Google Scholar 

  11. N. Klarlund, M. Nielsen, and K. Sunesen. Automated logical verification based on trace abstraction. In Proc. 15th ACM Symposium on Principles of Distributed Computing, pp. 101–110. ACM, 1996.

    Google Scholar 

  12. L. Lamport. A new solution of Dijkstra’s concurrent programming problem. CACM, 17(8): 453–455, 1974.

    MATH  MathSciNet  Google Scholar 

  13. M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialization. In A. Bossi (ed.), Proc. LOPSTR’ 99, LNCS 1817, pp. 63–82. Springer, 1999.

    Google Scholar 

  14. J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987.

    MATH  Google Scholar 

  15. U. Nilsson and J. Lübcke. Constraint logic programming for local and symbolic model-checking. In J. W. Lloyd et al. (eds.), Proc. CL’2000, LNAI 1861, pp. 384–398, 2000.

    Google Scholar 

  16. A. Pettorossi and M. Proietti. Perfect model checking via unfold/fold transformations. In J. W. Lloyd et al. (eds.), Proc. CL’2000, LNAI 1861, pp. 613–628. Springer, 2000.

    Google Scholar 

  17. A. Pettorossi and M. Proietti. Program Derivation = Rules + Strategies. In A. Kakas and F. Sadri (eds.), Computational Logic: Logic Programming and Beyond (in honour of Bob Kowalski, Part I), LNCS 2407, pp. 273–309. Springer, 2002.

    Google Scholar 

  18. A. Pettorossi, M. Proietti, and S. Renault. Reducing nondeterminism while specializing logic programs. In Proc. 24-th POPL, pp. 414–427. ACM Press, 1997.

    Google Scholar 

  19. Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proc. CAV’ 97, LNCS 1254, pp. 143–154. Springer, 1997.

    Google Scholar 

  20. A. Roychoudhury and I.V. Ramakrishnan. Automated inductive verification of parameterized protocols. In Proc. CAV 2001, pp. 25–37, 2001.

    Google Scholar 

  21. K. Sagonas, T. Swift, D. S. Warren, J. Freire, P. Rao, B. Cui, and E. Johnson. The XSB system, version 2.2., 2000.

    Google Scholar 

  22. J.W. Thatcher and J.B. Wright. Generalized finite automata with an application to a decision problem of second-order logic. Mathematical System Theory, 2:57–82, 1968.

    Article  MathSciNet  Google Scholar 

  23. The MAP group. The MAP transformation system. Available from http://www.iasi.rm.cnr.it/~proietti/system.html, 1995–2002.

  24. W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa (eds.), Handbook of Formal Languages, volume 3, pp. 389–455. Springer, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IASI-CNR, Viale Manzoni 30, I-00185, Roma, Italy

    Fabio Fioravanti & Maurizio Proietti

  2. DISP, University of Roma Tor Vergata, I-00133, Roma, Italy

    Alberto Pettorossi

Authors
  1. Fabio Fioravanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alberto Pettorossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maurizio Proietti
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Electronics and Computer Science, University of Southampton, Highfield, Southampton, SO17 1BJ, UK

    Michael Leuschel

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fioravanti, F., Pettorossi, A., Proietti, M. (2003). Combining Logic Programs and Monadic Second Order Logics by Program Transformation. In: Leuschel, M. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2002. Lecture Notes in Computer Science, vol 2664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45013-0_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-45013-0_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40438-5

  • Online ISBN: 978-3-540-45013-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation