Challenges in constraint-based analysis of hybrid systems. (English) Zbl 1248.68328
Oddi, Angelo (ed.) et al., Recent advances in constraints. 13th annual ERCIM international workshop on constraint solving and constraint logic programming, CSCLP 2008, Rome, Italy, June 18–20, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-03250-9/pbk). Lecture Notes in Computer Science 5655. Lecture Notes in Artificial Intelligence, 51-65 (2009).
Summary: 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.
For the entire collection see [Zbl 1168.68004].
For the entire collection see [Zbl 1168.68004].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
Keywords:
mixed Boolean and arithmetic constraints; differential equations; stochastic SMT; Craig interpolation; parallel solverReferences:
| [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) · Zbl 0944.68119 · doi:10.1007/3-540-48168-0_10 |
| [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) · Zbl 0978.68534 |
| [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) · doi:10.1109/CMPASS.1995.521887 |
| [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) · doi:10.1007/3-540-49059-0_14 |
| [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) · Zbl 1272.68220 · doi:10.1016/j.entcs.2004.12.022 |
| [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) · Zbl 1116.68048 · doi:10.1007/s10703-006-0031-0 |
| [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) · doi:10.1016/S1574-6526(06)80020-9 |
| [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) |
| [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) · Zbl 1144.68371 |
| [11] | Tseitin, G.: On the complexity of derivations in propositional calculus. Studies in Constructive Mathematics and Mathematical Logics (1968) |
| [12] | Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. Journal of the ACM 7(3), 201–215 (1960) · Zbl 0212.34203 · doi:10.1145/321033.321034 |
| [13] | Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM 5, 394–397 (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557 |
| [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) |
| [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) · Zbl 0663.65074 |
| [16] | Stauning, O.: Automatic Validation of Numerical Solutions. PhD thesis, Technical University of Denmark, Lyngby (1997) |
| [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) · Zbl 0976.65061 · doi:10.1023/A:1024467732637 |
| [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) · Zbl 0938.93552 · doi:10.1007/3-540-46430-1_14 |
| [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) · Zbl 1135.93341 · doi:10.1007/978-3-540-24743-2_27 |
| [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) · Zbl 1183.68369 · doi:10.1007/978-3-540-88387-6_14 |
| [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) · Zbl 1143.68452 · doi:10.1007/978-3-540-78929-1_13 |
| [22] | Papadimitriou, C.H.: Games against nature. J. Comput. Syst. Sci. 31(2), 288–301 (1985) · Zbl 0583.68020 · doi:10.1016/0022-0000(85)90045-5 |
| [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) |
| [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) · Zbl 1142.68525 · doi:10.1007/978-3-540-68155-7_20 |
| [25] | Craig, W.: Linear reasoning: A new form of the Herbrand-Gentzen theorem. Journal of Symbolic Logic 22(3), 250–268 (1957) · Zbl 0081.24402 · doi:10.2307/2963593 |
| [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) · Zbl 1278.68184 · doi:10.1007/978-3-540-45069-6_1 |
| [27] | McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101–121 (2005) · Zbl 1079.68092 · doi:10.1016/j.tcs.2005.07.003 |
| [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) · doi:10.1007/s10009-007-0044-z |
| [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) · Zbl 1132.68480 · doi:10.1007/978-3-540-69738-1_25 |
| [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) · Zbl 1134.68402 · doi:10.1007/978-3-540-78800-3_30 |
| [31] | Pudlák, P.: Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Journal of Symbolic Logic 62(3), 981–998 (1997) · Zbl 0945.03086 · doi:10.2307/2275583 |
| [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) · Zbl 0891.68096 · doi:10.1007/BF02127976 |
| [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) · Zbl 0990.90563 |
| [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) · doi:10.1109/MTV.2005.17 |
| [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) · Zbl 0990.90546 |
| [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) · doi:10.1016/j.entcs.2004.10.020 |
| [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) |
| [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) · Zbl 0863.68013 · doi:10.1006/jsco.1996.0030 |
| [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) · Zbl 1213.68359 · doi:10.1007/978-3-540-70952-7_21 |
| [40] | Strichman, O.: Accelerating bounded model checking of safety properties. Formal Methods in System Design 24(1), 5–24 (2004) · Zbl 1073.68054 · doi:10.1023/B:FORM.0000004785.67232.f8 |
| [41] | Walsh, T.: Stochastic constraint programming. In: Proc. of the 15th European Conference on Artificial Intelligence (ECAI 2002). IOS Press, Amsterdam (2002) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
