Skip to main content
SpringerLink
Log in

Challenges in Constraint-Based Analysis of Hybrid Systems

  • Conference paper
Recent Advances in Constraints (CSCLP 2008)

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

Abstract

In the analysis of hybrid discrete-continuous systems, rich arithmetic constraint formulae with complex Boolean structure arise naturally. The iSAT algorithm, a solver for such formulae, is aimed at bounded model checking of hybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhance the iSAT algorithm. First, we propose an extension of iSAT to directly handle ordinary differential equations as constraints. Second, we outline the recently introduced generalization of the iSAT algorithm to deal with probabilistic hybrid systems and some open research issues in that context. Third, we present ideas on how to move from bounded to unbounded model checking by using the concept of interpolation. Finally, we discuss the adaption of some parallelization techniques to the iSAT case, which will hopefully lead to performance gains in the future. By presenting these open research questions, this paper aims at fostering discussions on these extensions of constraint solving.

This work has been partially supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, www.avacs.org).

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. Fränzle, M.: Analysis of hybrid systems: An ounce of realism can save an infinity of states. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 126–140. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: Proc. of the 27th Annual Symposium on Theory of Computing, pp. 373–382. ACM Press, New York (1995)

    Google Scholar 

  3. Groote, J.F., Koorn, J.W.C., van Vlijmen, S.F.M.: The Safety Guaranteeing System at Station Hoorn-Kersenboogerd. In: Conference on Computer Assurance, pp. 57–68. National Institute of Standards and Technology (1995)

    Google Scholar 

  4. Biere, A., Cimatti, A., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying industrial hybrid systems with MathSAT. In: Bounded Model Checking (BMC 2004). ENTCS, vol. 119, pp. 17–32 (2005)

    Google Scholar 

  6. Fränzle, M., Herde, C.: HySAT: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design 30(3), 179–198 (2007)

    Article  MATH  Google Scholar 

  7. Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming. Foundations of Artificial Intelligence, pp. 571–603. Elsevier, Amsterdam (2006)

    Chapter  Google Scholar 

  8. Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability Modulo Theories. In: Handbook on Satisfiability, February 2009. Frontiers in Artificial Intelligence and Applications, vol. 185. IO Press (2009), ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BarSST-09.pdf

  9. Bauer, A., Pister, M., Tautschnig, M.: Tool-support for the analysis of hybrid systems and models. In: Design, Automation and Test in Europe. IEEE, Los Alamitos (2007)

    Google Scholar 

  10. Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure. JSAT Special Issue on SAT/CP Integration 1, 209–236 (2007)

    MATH  Google Scholar 

  11. Tseitin, G.: On the complexity of derivations in propositional calculus. Studies in Constructive Mathematics and Mathematical Logics (1968)

    Google Scholar 

  12. Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. Journal of the ACM 7(3), 201–215 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  13. Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM 5, 394–397 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  14. Moore, R.E.: Automatic local coordinate transformation to reduce the growth of error bounds in interval computation of solutions of ordinary differential equations. In: Ball, L.B. (ed.) Error in Digital Computation, vol. II, pp. 103–140. Wiley, New York (1965)

    Google Scholar 

  15. Lohner, R.: Einschließung der Lösung gewöhnlicher Anfangs- und Randwertaufgaben. PhD thesis, Fakultät für Mathematik der Universität Karlsruhe, Karlsruhe (1988)

    Google Scholar 

  16. Stauning, O.: Automatic Validation of Numerical Solutions. PhD thesis, Technical University of Denmark, Lyngby (1997)

    Google Scholar 

  17. Berz, M., Makino, K.: Verified Integration of ODEs and Flows Using Differential Algebraic Methods on High-Order Taylor Models. Reliable Computing 4(4), 361–369 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  18. Henzinger, T.A., Horowitz, B., Majumdar, R., Wong-Toi, H.: Beyond HYTECH: Hybrid systems analysis using interval numerical methods. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 130–144. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Hickey, T., Wittenberg, D.: Rigorous modeling of hybrid systems using interval arithmetic constraints. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 402–416. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  20. Eggers, A., Fränzle, M., Herde, C.: SAT modulo ODE: A direct SAT approach to hybrid systems. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171–185. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Fränzle, M., Hermanns, H., Teige, T.: Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 172–186. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Papadimitriou, C.H.: Games against nature. J. Comput. Syst. Sci. 31(2), 288–301 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  23. Schmitt, C.: Bounded Model Checking of Probabilistic Hybrid Automata. Master’s thesis, Carl von Ossietzky University, Dpt. of Computing Science, Oldenburg, Germany (March 2008)

    Google Scholar 

  24. Teige, T., Fränzle, M.: Stochastic Satisfiability modulo Theories for Non-linear Arithmetic. In: Perron, L., Trick, M.A. (eds.) CPAIOR 2008. LNCS, vol. 5015, pp. 248–262. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  25. Craig, W.: Linear reasoning: A new form of the Herbrand-Gentzen theorem. Journal of Symbolic Logic 22(3), 250–268 (1957)

    Article  MathSciNet  MATH  Google Scholar 

  26. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  27. McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101–121 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  28. Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast: Applications to software engineering. International Journal on Software Tools for Technology Transfer (STTT) 9(5-6), 505–525 (2007) (invited to special issue of selected papers from FASE 2004/2005)

    Article  Google Scholar 

  29. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  30. Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 397–412. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  31. Pudlák, P.: Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Journal of Symbolic Logic 62(3), 981–998 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  32. Böhm, M., Speckenmeyer, E.: A fast parallel SAT-solver - efficient workload balancing. Annals of Mathematics and Artificial Intelligence 17(3-4), 381–400 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  33. Sinz, C., Blochinger, W., Küchlin, W.: PaSAT - parallel SAT-checking with lemma exchange: Implementation and applications. In: Kautz, H., Selman, B. (eds.) LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001), June 2001. Electronic Notes in Discrete Mathematics, vol. 9. Elsevier Science Publishers, Boston (2001)

    Google Scholar 

  34. Schubert, T., Lewis, M., Becker, B.: PaMira – A Parallel SAT Solver with Knowledge Sharing. In: 6th International Workshop on Microprocessor Test and Verification (MTV 2005), pp. 29–36. IEEE Computer Society, Los Alamitos (2005)

    Chapter  Google Scholar 

  35. Jurkowiak, B., Li, C.M., Utard, G.: Parallelizing SATZ Using Dynamic Workload Balancing. In: Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT 2001), June 2001, vol. 9. Elsevier Science Publishers, Amsterdam (2001)

    Google Scholar 

  36. Feldman, Y., Dershowitz, N., Hanna, Z.: Parallel multithreaded satisfiability solver: Design and implementation. Electronic Notes in Theoretical Computer Science 128(3), 75–90 (2005)

    Article  Google Scholar 

  37. Lewis, M.D.T., Schubert, T., Becker, B.: Multithreaded SAT solving. In: Proceedings of the 12th Asia and South Pacific Design Automation Conference, pp. 926–931. IEEE Computer Society, Los Alamitos (2007)

    Google Scholar 

  38. Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: A distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation 21(4), 543–560 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  39. Ábrahám, E., Schubert, T., Becker, B., Fränzle, M., Herde, C.: Parallel SAT solving in bounded model checking. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 301–315. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  40. Strichman, O.: Accelerating bounded model checking of safety properties. Formal Methods in System Design 24(1), 5–24 (2004)

    Article  MATH  Google Scholar 

  41. Walsh, T.: Stochastic constraint programming. In: Proc. of the 15th European Conference on Artificial Intelligence (ECAI 2002). IOS Press, Amsterdam (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Carl von Ossietzky Universität Oldenburg, Germany

    Andreas Eggers & Tino Teige

  2. Albert-Ludwigs-Universität Freiburg, Germany

    Natalia Kalinnik & Stefan Kupferschmid

Authors
  1. Andreas Eggers
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Natalia Kalinnik
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Stefan Kupferschmid
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Tino Teige
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. ISTC-CNR, Institute for Cognitive Science and Technology, National Research Council of Italy, Via San Martino della Battaglia 44, 00185, Rome, Italy

    Angelo Oddi

  2. INRIA Rocquencourt, BP 105, 78153, Le Chesnay Cedex, France

    François Fages

  3. Department of Pure and Applied Mathematics, University of Padova, Via Trieste 63, 35121, Padova, Italy

    Francesca Rossi

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Eggers, A., Kalinnik, N., Kupferschmid, S., Teige, T. (2009). Challenges in Constraint-Based Analysis of Hybrid Systems. In: Oddi, A., Fages, F., Rossi, F. (eds) Recent Advances in Constraints. CSCLP 2008. Lecture Notes in Computer Science(), vol 5655. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03251-6_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-03251-6_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-03250-9

  • Online ISBN: 978-3-642-03251-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation