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).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
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)
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)
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)
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)
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)
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)
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)
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
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)
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)
Tseitin, G.: On the complexity of derivations in propositional calculus. Studies in Constructive Mathematics and Mathematical Logics (1968)
Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. Journal of the ACM 7(3), 201–215 (1960)
Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM 5, 394–397 (1962)
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)
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)
Stauning, O.: Automatic Validation of Numerical Solutions. PhD thesis, Technical University of Denmark, Lyngby (1997)
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)
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)
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)
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)
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)
Papadimitriou, C.H.: Games against nature. J. Comput. Syst. Sci. 31(2), 288–301 (1985)
Schmitt, C.: Bounded Model Checking of Probabilistic Hybrid Automata. Master’s thesis, Carl von Ossietzky University, Dpt. of Computing Science, Oldenburg, Germany (March 2008)
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)
Craig, W.: Linear reasoning: A new form of the Herbrand-Gentzen theorem. Journal of Symbolic Logic 22(3), 250–268 (1957)
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)
McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101–121 (2005)
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)
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)
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)
Pudlák, P.: Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Journal of Symbolic Logic 62(3), 981–998 (1997)
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)
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)
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)
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)
Feldman, Y., Dershowitz, N., Hanna, Z.: Parallel multithreaded satisfiability solver: Design and implementation. Electronic Notes in Theoretical Computer Science 128(3), 75–90 (2005)
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)
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)
Á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)
Strichman, O.: Accelerating bounded model checking of safety properties. Formal Methods in System Design 24(1), 5–24 (2004)
Walsh, T.: Stochastic constraint programming. In: Proc. of the 15th European Conference on Artificial Intelligence (ECAI 2002). IOS Press, Amsterdam (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)