Skip to main content
SpringerLink
Log in

Alternating Fixed Points in Boolean Equation Systems as Preferred Stable Models

  • Conference paper
  • First Online:
Logic Programming (ICLP 2001)

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

Included in the following conference series:

Abstract

We formally characterize alternating fixedp oints of boolean equation systems as models of (propositional) normal logic programs. To this end, we introduce the notion of a preferred stable model of a logic program, andd efine a mapping that associates a normal logic program with a boolean equation system such that the solution to the equation system can be “reado. ” the preferredstable model of the logic program. We also show that the preferredmo del cannot be calculateda-p osteriori (i.e. compute stable models andc hoose the preferredone) but rather must be computedin an intertwinedfashion with the stable model itself. The mapping reveals a natural relationship between the evaluation of alternating fixedp oints in boolean equation systems andthe Gelfond- Lifschitz transformation usedin stable-model computation.

For alternation-free boolean equation systems, we show that the logic programs we derive are stratified, while for formulas with alternation, the corresponding programs are non-stratified. Consequently, our mapping of boolean equation systems to logic programs preserves the computational complexity of evaluating the solutions of special classes of equation systems (e.g., linear-time for the alternation-free systems, exponential for systems with alternating fixed points).

Research supportedin part by NSF grants EIA-9705998, CCR-9876242, EIA- 9805735, CCR-9988155, andI IS-0072927, andAR O grants ARO DAAD190110003 andD AAD190110019.

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. G. Brewka and T. Eiter. Preferredansw er sets for extendedlogic programs. Arti-ficial Intelligence, 109(1–2)297–356.

    Google Scholar 

  2. E. M. Clarke and E. A. Emerson. Design andsyn thesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer Verlag, 1981.

    Chapter  Google Scholar 

  3. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.

    Google Scholar 

  4. E. M. Clarke and J. M. Wing. Formal methods: State of the art andfuture directions. ACM Computing Surveys, 28(4), December 1996.

    Google Scholar 

  5. R. Cleavelandand B. U. Steffen. A linear-time model checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design, 2:121–147, 1993.

    Article  Google Scholar 

  6. G. Delzanno and A. Podelski. Model checking in CLP. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 223–239, 1999.

    Google Scholar 

  7. M. Gelfondand V. Lifschitz. The stable model semantics for logic programming. In International Conference on Logic Programming, pages 1070–1080, 1988.

    Google Scholar 

  8. D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  9. K. Narayan Kumar, C.R. Ramakrishnan, and S. A. Smolka. Alternating fixed points in boolean equation systems as preferredstable models. Technical report, Department of Computer Science, SUNY at Stony Brook, Stony Brook, New York, 2001. Available from: http://www.cs.sunysb.edu/~cram/papers.

    Google Scholar 

  10. Xinxin Liu, C. R. Ramakrishnan, and Scott A. Smolka. Fully local andeficien t model checking of alternating fixed points. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of Lecture Notes in Computer Science, pages 56–70. Springer Verlag, 1998.

    Chapter  Google Scholar 

  11. A. Mader. Verification of Modal Properties using Boolean Equations. PhD thesis, Technical University of Munich, 1997.

    Google Scholar 

  12. I. Niemela and P. Simons. Efficient implementation of the well-foundedandstable model semantics. In Joint International Conference and Symposium on Logic Programming, pages 289–303, 1996.

    Google Scholar 

  13. V. R. Pratt. A decidable mu-calculus. In Proceedings of the 22nd IEEE Ann. Symp. on Foundations of Computer Science, Nashville, Tennessee, pages 421–427, 1981.

    Google Scholar 

  14. J. P. Queille and J. Sifakis. Specification andv erification of concurrent systems in Cesar. In Proceedings of the International Symposium in Programming, volume 137 of Lecture Notes in Computer Science, Berlin, 1982. Springer-Verlag.

    Google Scholar 

  15. Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. L. Swift, andD. S. Warren. Efficient model checking using tabledresolution. In Proceedings of the 9th International Conference on Computer-Aided Verification (CAV’ 97), Haifa, Israel, July 1997. Springer-Verlag.

    Google Scholar 

  16. C.R. Ramakrishnan, I.V. Ramakrishnan, S.A. Smolka, Y. Dong, X. Du, A. Roychoudhury, and V.N. Venkatakrishnan. XMC: A logic-programming-basedv eri.-cation toolset. In Computer Aided Verification (CAV), 2000.

    Google Scholar 

  17. C. Sakama and K. Inoue. Representing priorities in logic programs. In Joint International Conference/Symposium on Logic Programming, pages 82–96, 1996.

    Google Scholar 

  18. B. Vergauwen and J. Lewi. Efficient local correctness checking for single and alternating boolean equation systems. In Proceedings of ICALP’94, pages 304–315. LNCS 820, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, State University of New York at Stony Brook, Stony Brook, New York, USA

    K. Narayan Kumar, C. R. Ramakrishnan & S. A. Smolka

  2. Chennai Mathematical Institute, Chennai, India

    K. Narayan Kumar

Authors
  1. K. Narayan Kumar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. C. R. Ramakrishnan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. S. A. Smolka
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LIP6, case 169, University of Paris 6, 8 rue du Capitaine Scott, 75015, Paris, France

    Philippe Codognet

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Narayan Kumar, K., Ramakrishnan, C.R., Smolka, S.A. (2001). Alternating Fixed Points in Boolean Equation Systems as Preferred Stable Models. In: Codognet, P. (eds) Logic Programming. ICLP 2001. Lecture Notes in Computer Science, vol 2237. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45635-X_23

Download citation

  • DOI: https://doi.org/10.1007/3-540-45635-X_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42935-7

  • Online ISBN: 978-3-540-45635-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation