Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Abstraction, Reformulation, and Approximation

SARA 2000: Abstraction, Reformulation, and Approximation pp 202–218Cite as

Reformulation and Approximation in Model Checking

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1864))

Abstract

Symbolic model checking of various important properties like reachability, containment and equivalence of constraint automata could be unsolvable problems in general. This paper identifies several classes of constraint automata for which these properties can be guaranteed to be solvable by reformulating them as the evaluation problem of solvable or approximately solvable classes of constraint logic problems. The paper also presents rewrite rules to simplify constraint automata and illustrates the techniques on several example control systems.

This research was supported in part by NSF grant IRI-9625055 and a Gallup Research Professorship.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995.

    Google Scholar 

  2. B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proc. Conf. on Computer-Aided Verification, pages 55–67, 1994.

    Google Scholar 

  3. J.-H. Byon and P.Z. Revesz. DISCO: A constraint database system with sets. In Proc. Workshop on Constraint Databases and Applications, number 1034 in LNCS, pages 68–83. Springer-Verlag, September 1995.

    Google Scholar 

  4. A. Cimatti, F. Giunchiglia, and M. Roveri. Abstraction in planning via model checking. In Proc. Symposium on Abstraction, Reformulation and Approximation, pages 37–41, 1998.

    Google Scholar 

  5. J.J. Comuzzi and J.M. Hart. Program slicing using weakest precondition. In Proc. Industrial Benefit and Advances in Formal Methods, number 1051 in LNCS. Springer-Verlag, 1996.

    Google Scholar 

  6. G. Delzanno and A. Podelski. Model checking in clp. In Second International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer LNCS, 1999.

    Google Scholar 

  7. L. Fribourg and H. Olsén. A decompositional approach for computing least fixed-points of datalog programs with z-counters. Constraints, 3–4:305–336, 1997.

    Article  Google Scholar 

  8. L. Fribourg and J.D.C. Richardson. Symbolic verification with gap-order constraints. In Prof. LOPSTR, 1996.

    Google Scholar 

  9. S. Graf and H. Saidi. Constructing abstract graphs using pvs. In Proc. Computer Aided Verification, number 1102 in LNCS. Springer-Verlag, 1996.

    Google Scholar 

  10. N. Halbwachs. Delay analysis in synchronous programs. In Proc. Conf. on Computer-Aided Verification, pages 333–346, 1993.

    Google Scholar 

  11. T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. In Proc. Computer Aided Verification, number 1254 in LNCS, pages 460–463. Springer-Verlag, 1997.

    Google Scholar 

  12. J. Jaffar and J.-L. Lassez. Constraint logic programming. In Proc. 14th ACM POPL, pages 111–119, 1987.

    Google Scholar 

  13. P.C. Kanellakis, G.M. Kuper, and P.Z. Revesz. Constraint query languages. In Proc. of the 9th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 299–313, New York, 1990. ACM Press.

    Google Scholar 

  14. P.C. Kanellakis, G.M. Kuper, and P.Z. Revesz. Constraint query languages. Journal of Computer and System Sciences, 51:26–52, 1995.

    Article  MathSciNet  Google Scholar 

  15. A. Kerbrat. Reachable state space analysis of lotos specifications. In Proc. 7th International Conference on Formal Description Techniques, pages 161–176, 1994.

    Google Scholar 

  16. R. Kosaraju. Decidability of reachability in vector addition systems. In Proc. of the 14th Annual ACM Symposium on Theory of Computing, pages 267–280, 1982.

    Google Scholar 

  17. M. Lowry and M. Subramaniam. Abstraction for analytic verification of concurrent software systems. In Proc. Symposium on Abstraction, Reformulation and Approximation, pages 85–94, 1998.

    Google Scholar 

  18. E. Mayr. An algorithm for the general petri net reachability problem. In Proc. of the 13th Annual ACM Symposium on Theory of Computing, pages 238–246, 1981.

    Google Scholar 

  19. K. McMillan. Symbolic Model Checking. Kluwer, 1993.

    Google Scholar 

  20. M.L. Minsky. Recursive unsolvability of post’s problem of ‘tag’ and other topics in the theory of turing machines. Annals of Mathematics, 74(3):437–455, 1961.

    Article  MathSciNet  Google Scholar 

  21. M. L. Minsky. Computation: Finite and Infinite Machines. Prentice Hall, 1967.

    Google Scholar 

  22. J. Peterson. Petri Net Theory and Modeling of Systems. Prentice-Hall,Inc., 1981.

    Google Scholar 

  23. R. Ramakrishnan. Database Management Systems. McGraw-Hill, 1998.

    Google Scholar 

  24. W. Reisig. Petri Nets: an Introduction. Springer, 1985.

    Google Scholar 

  25. P.Z. Revesz. Safe datalog queries with linear constraints. In M. Maher and J.-F. Puget, editors, Proc. Fourth International Conference on Principles and Practice of Constraint Programming, number 1520 in LNCS. Springer-Verlag, 1998.

    Google Scholar 

  26. P.Z. Revesz. Datalog programs with difference constraints. In Proc. Twelfth International Conference on Applications of Prolog, pages 69–76, September 1999.

    Google Scholar 

  27. P.Z. Revesz. A closed-form evaluation for Datalog queries with integer (gap)-order constraints. Theoretical Computer Science, 116:117–149, 1993.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Nebraska-Lincoln, Lincoln, NE, 68588, USA

    Peter Z. Revesz

Authors
  1. Peter Z. Revesz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, University of Nebraska - Lincoln, 115 Ferguson Hall, Lincoln, NE, 68588-0115

    Berthe Y. Choueiry

  2. Department of Computer Science, University of York, Heslington, York, Y010 5DD, UK

    Toby Walsh

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Revesz, P.Z. (2000). Reformulation and Approximation in Model Checking. In: Choueiry, B.Y., Walsh, T. (eds) Abstraction, Reformulation, and Approximation. SARA 2000. Lecture Notes in Computer Science(), vol 1864. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44914-0_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-44914-0_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-44914-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation