Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. (English) Zbl 1205.68252
Summary: We recall different approaches to the constraint-based, symbolic analysis of hybrid discrete-continuous systems and combine them to a technology able to address hybrid systems exhibiting both non-deterministic and probabilistic behavior akin to infinite-state Markov decision processes. To enable mechanized analysis of such systems, we extend the reasoning power of arithmetic Satisfiability-Modulo-Theories (SMT) solving by, first, reasoning over Ordinary Differential Equations (ODEs) and, second, a comprehensive treatment of randomized (also known as stochastic) quantification over discrete variables as well as existential quantification over both discrete and continuous variables within the mixed Boolean-arithmetic constraint system. This provides the technological basis for a constraint-based analysis of dense-time probabilistic hybrid automata, extending previous results addressing discrete-time automata. Generalizing SMT-based bounded model-checking of hybrid automata, stochastic SMT including ODEs permits the direct analysis of probabilistic bounded reachability problems of dense-time probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.
MSC:
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 68Q45 | Formal languages and automata |
Keywords:
probabilistic hybrid automata; bounded model checking; arithmetic constraint solving; stochastic satisfiabilityReferences:
| [1] | Ábrahám, E.; Becker, B.; Klaedke, F.; Steffen, M., Optimizing bounded model checking for linear hybrid systems, (Cousot, R., Proc. of Sixth Int. Conf. on Verification, Model Checking and Abstract Interpretation, VMCAI 2005, Paris, January 2005. Proc. of Sixth Int. Conf. on Verification, Model Checking and Abstract Interpretation, VMCAI 2005, Paris, January 2005, Lect. Notes in Comput. Sci, vol. 3385 (2005), Springer), 396-412 · Zbl 1111.68493 |
| [2] | E. Ábrahám, T. Schubert, B. Becker, M. Fränzle, C. Herde, Parallel SAT solving in bounded model checking, J. Log. Comput., in press, doi:10.1093/logcom/exp002.; E. Ábrahám, T. Schubert, B. Becker, M. Fränzle, C. Herde, Parallel SAT solving in bounded model checking, J. Log. Comput., in press, doi:10.1093/logcom/exp002. · Zbl 1213.68359 |
| [3] | Amin, S.; Abate, A.; Prandini, M.; Lygeros, J.; Sastry, S., Reachability analysis of controlled discrete-time stochastic hybrid systems, (Hespanha, J. P.; Tiwari, A., Proc. of Ninth Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2006, Santa Barbara, CA, March 2006. Proc. of Ninth Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2006, Santa Barbara, CA, March 2006, Lecture Notes in Computer Science, vol. 3927 (2006), Springer), 49-63 · Zbl 1178.93069 |
| [4] | Arnold, L., Stochastic Differential Equations: Theory and Applications (1974), Wiley · Zbl 0278.60039 |
| [5] | G. Audemard, M. Bozzano, A. Cimatti, R. Sebastiani, Verifying industrial hybrid systems with mathsat, in: A. Biere, O. Strichman (Eds.), Proc. of Second Int. Wksh. on Bounded Model-Checking, BMC (Boston, MA, July), Electron. Notes in Theor. Comput. Sci., vol. 119 (2) , Elsevier, 2005, pp. 17-32.; G. Audemard, M. Bozzano, A. Cimatti, R. Sebastiani, Verifying industrial hybrid systems with mathsat, in: A. Biere, O. Strichman (Eds.), Proc. of Second Int. Wksh. on Bounded Model-Checking, BMC (Boston, MA, July), Electron. Notes in Theor. Comput. Sci., vol. 119 (2) , Elsevier, 2005, pp. 17-32. · Zbl 1272.68220 |
| [6] | Baier, C.; Hermanns, H.; Katoen, J.-P.; Haverkort, B. R., Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes, Theor. Comput. Sci., 345, 1, 2-26 (2005) · Zbl 1081.90066 |
| [7] | Barrett, C.; Sebastiani, R.; Seshia, S. A.; Tinelli, C., Satisfiability modulo theories, (Biere, A.; Heule, M. J.H.; van Maaren, H.; Walsh, T., Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185 (2009), IOS Press), 825-885 · Zbl 1183.68568 |
| [8] | A. Bauer, M. Pister, M. Tautschnig, Tool-support for the analysis of hybrid systems and models, in: Proc. of 2007 Conf. on Design, Automation and Test in Europe (Nice, April 2007), EDA Consortium, 2007, pp. 924-929.; A. Bauer, M. Pister, M. Tautschnig, Tool-support for the analysis of hybrid systems and models, in: Proc. of 2007 Conf. on Design, Automation and Test in Europe (Nice, April 2007), EDA Consortium, 2007, pp. 924-929. |
| [9] | R.J. Bayardo, R. Schrag, Using CSP look-back techniques to solve real-world SAT instances, in: Proc. of 14th Nat. Conf. on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conf. AAAI/’97/IAAI ’97 (Providence, RI, July 1997), AAAI Press/The MIT Press, 1997, pp. 203-208.; R.J. Bayardo, R. Schrag, Using CSP look-back techniques to solve real-world SAT instances, in: Proc. of 14th Nat. Conf. on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conf. AAAI/’97/IAAI ’97 (Providence, RI, July 1997), AAAI Press/The MIT Press, 1997, pp. 203-208. |
| [10] | Bellman, R., A Markovian decision process, J. Math. Mech., 6, 679-684 (1957) · Zbl 0078.34101 |
| [11] | Bemporad, A.; Cairano, S. D., Optimal control of discrete hybrid stochastic automata, (Morari, M.; Thiele, L., Proc. of Eighth Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2005 (Zürich, March 2005). Proc. of Eighth Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2005 (Zürich, March 2005), Lecture Notes in Computer Science, vol. 3414 (2005), Springer), 151-167 · Zbl 1078.93573 |
| [12] | Benhamou, F., Heterogeneous constraint solving, (Hanus, M.; Rodríguez-Artalejo, M., Proc. of 5th Int. Conf. on Algebraic and Logic Programming, ALP ’96 (Aachen, September 1996). Proc. of 5th Int. Conf. on Algebraic and Logic Programming, ALP ’96 (Aachen, September 1996), Lecture Notes in Computer Science, vol. 1139 (1996), Springer), 62-76 · Zbl 1355.68030 |
| [13] | Benhamou, F.; Granvilliers, L., Continuous and interval constraints, (Rossi, F.; van Beek, P.; Walsh, T., Handbook of Constraint Programming, Foundations of Artificial Intelligence (2006), Elsevier), 571-603 · Zbl 1175.90011 |
| [14] | Benhamou, F.; McAllester, D.; Van Hentenryck, P., CLP(intervals) revisited, (Bruynooghe, M., Proc. of 1994 Int. Symp. on Logic Programming, IPLS ’94 (Ithaca, NY, November 1994) (1994), MIT Press), 124-138 |
| [15] | Berz, M.; Makino, K., Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models, Reliab. Comput., 4, 4, 361-369 (1998) · Zbl 0976.65061 |
| [16] | Biere, A.; Cimatti, A.; Clarke, E.; Zhu, Y., Symbolic model checking without BDDs, (Cleaveland, R., Proc. of Fifth Int. Conf. on Tools for Construction and Analysis of Systems, TACAS ’99 (Seattle, WA, Aug. 2006). Proc. of Fifth Int. Conf. on Tools for Construction and Analysis of Systems, TACAS ’99 (Seattle, WA, Aug. 2006), Lecture Notes in Computer Science, vol. 4144 (2006), Springer), 81-94 |
| [17] | (Blom, H. A.; Lygeros, J., Stochastic Hybrid Systems: Theory and Safety Critical Applications. Stochastic Hybrid Systems: Theory and Safety Critical Applications, Lecture Notes in Control and Information Sciences, vol. 337 (2006), Springer) · Zbl 1094.93003 |
| [18] | Blom, H. A.P.; Krystul, J.; Bakker, G. J., A particle system for safety verification of free flight in air traffic, (Decision and Control (2006), IEEE), 1574-1579 |
| [19] | Bozzano, M.; Bruttomesso, R.; Cimatti, A.; Junttila, T. A.; van Rossum, P.; Schulz, S.; Sebastiani, R., The MathSAT 3 system, (Nieuwenhuis, R., Proc. of 20th Int. Conf. on Automated Deduction CADE-20 (Tallinn, July 2005). Proc. of 20th Int. Conf. on Automated Deduction CADE-20 (Tallinn, July 2005), Lecture Notes in Artificial Intelligence, vol. 3632 (2005), Springer), 315-321 |
| [20] | Bujorianu, M. L.; Lygeros, J., Reachability questions in piecewise deterministic Markov processes, (Maler, O.; Pnueli, A., Proc. of Sixth Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2003 (Prague, April 2003). Proc. of Sixth Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2003 (Prague, April 2003), Lecture Notes in Computer Science, vol. 2623 (2003), Springer), 126-140 · Zbl 1032.93074 |
| [21] | Bujorianu, M. L.; Lygeros, J., Toward a general theory of stochastic hybrid systems, (Stochastic Hybrid Systems: Theory and Safety Critical Applications. Stochastic Hybrid Systems: Theory and Safety Critical Applications, Lecture Notes in Control and Information Science, vol. 337 (2006), Springer), 3-30 · Zbl 1130.93048 |
| [22] | (Cassandras, C. G.; Lygeros, J., Stochastic Hybrid Systems (2007), CRC Taylor & Francis) · Zbl 1123.93004 |
| [23] | Cimatti, A.; Pistore, M.; Roveri, M.; Sebastiani, R., Improving the encoding of LTL model checking into SAT, (Cortesi, A., Revised Papers from 3rd Int. Wksh. on Verification, Model Checking and Abstract Interpretation VMCAI 2002 (Venice, Jan. 2002). Revised Papers from 3rd Int. Wksh. on Verification, Model Checking and Abstract Interpretation VMCAI 2002 (Venice, Jan. 2002), Lecture Notes in Computer Science, vol. 2294 (2002), Springer), 196-207 · Zbl 1057.68056 |
| [24] | Davis, M. H.A., Piecewise-deterministic markov processes: a general class of non-diffusion stochastic models, J. Roy. Statist. Soc., 46, 3, 353-384 (1984) · Zbl 0565.60070 |
| [25] | Davis, M., Markov Models and Optimization (1993), Chapman and Hall: Chapman and Hall London · Zbl 0780.60002 |
| [26] | Davis, M.; Putnam, H., A computing procedure for quantification theory, J. ACM, 7, 3, 201-215 (1960) · Zbl 0212.34203 |
| [27] | Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem proving, Commun. ACM, 5, 394-397 (1962) · Zbl 0217.54002 |
| [28] | Dutertre, B.; de Moura, L., A fast linear-arithmetic solver for DPLL(T), (Ball, T.; Jones, R. B., Proc. of 18th Computer-Aided Verification Conference, CAV 2006 (Seattle, WA, Aug. 2006). Proc. of 18th Computer-Aided Verification Conference, CAV 2006 (Seattle, WA, Aug. 2006), Lecture Notes in Computer Science, vol. 4144 (2006), Springer), 81-94 |
| [29] | Eggers, A.; Fränzle, M.; Herde, C., SAT modulo ODE: a direct SAT approach to hybrid systems, (Cha, S. S.; Choi, J.-Y.; Kim, M.; Lee, I.; Viswanathan, M., Proc. of Sixth Int. Symp. on Automated Technology for Verification and Analysis, ATVA 2008 (Seoul, October 2008). Proc. of Sixth Int. Symp. on Automated Technology for Verification and Analysis, ATVA 2008 (Seoul, October 2008), ATVA, Lect. Notes in Comput. Sci, vol. 5311 (2008), Springer), 171-185 · Zbl 1183.68369 |
| [30] | Feng, X.; Loparo, K. A.; Ji, Y.; Chizeck, H. J., Stochastic stability properties of jump linear systems, IEEE Trans. Autom. Control, 37, 1, 38-53 (1992) · Zbl 0747.93079 |
| [31] | Fränzle, M.; Herde, C., HySAT: an efficient proof engine for bounded model checking of hybrid systems, Formal Methods Syst. Design, 30, 3, 179-198 (2007) · Zbl 1116.68048 |
| [32] | Fränzle, M.; Herde, C.; Teige, T.; Ratschan, S.; Schubert, T., Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure, J. Satisfiability, Boolean Model. Comput., 1, 209-236 (2007) · Zbl 1144.68371 |
| [33] | Fränzle, M.; Hermanns, H.; Teige, T., Stochastic satisfiability modulo theory: a novel technique for the analysis of Probabilistic hybrid systems, (Egerstedt, M.; Mishra, B., Proc. of 11th Int. Conf. on Hybrid Systems: Computation and Control, HSCC 2008 (St. Louis, MO, April 2008). Proc. of 11th Int. Conf. on Hybrid Systems: Computation and Control, HSCC 2008 (St. Louis, MO, April 2008), Lecture Notes in Computer Science, vol. 4981 (2008), Springer), 172-186 · Zbl 1143.68452 |
| [34] | Girard, A., Reachability of uncertain linear systems using zonotopes, (Morari, M.; Thiele, L., Proc. of Eighth Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2005 (Zürich, March 2005). Proc. of Eighth Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2005 (Zürich, March 2005), Lecture Notes in Computer Science, vol. 3414 (2005), Springer), 291-305 · Zbl 1078.93005 |
| [35] | J. Greifeneder, J. Frey, Probabilistic hybrid automata with variable step width applied to the analysis of networked automation systems, in: Proc. of Third IFAC Wksh. on Discrete Event System Design, DESDes ’06 (Rydzyna, September 2006), 2006, pp. 283-288.; J. Greifeneder, J. Frey, Probabilistic hybrid automata with variable step width applied to the analysis of networked automation systems, in: Proc. of Third IFAC Wksh. on Discrete Event System Design, DESDes ’06 (Rydzyna, September 2006), 2006, pp. 283-288. |
| [36] | J.F. Groote, J.W.C. Koorn, S.F.M. van Vlijmen, The safety guaranteeing system at Station Hoorn-Kersenboogerd, in: Conf. on Computer Assurance, National Institute of Standards and Technology, 1995, pp. 57-68.; J.F. Groote, J.W.C. Koorn, S.F.M. van Vlijmen, The safety guaranteeing system at Station Hoorn-Kersenboogerd, in: Conf. on Computer Assurance, National Institute of Standards and Technology, 1995, pp. 57-68. |
| [37] | Hehner, E. C.R., Predicative programming, Commun. ACM, 27, 134-151 (1984) · Zbl 0593.68010 |
| [38] | Hespanha, J. P., Polynomial stochastic hybrid systems, (Morari, M.; Thiele, L., Proc. of Eighth Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2005 (Zürich, March 2005). Proc. of Eighth Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2005 (Zürich, March 2005), Lecture Notes in Computer Science, vol. 3414 (2005), Springer), 322-338 · Zbl 1078.93063 |
| [39] | Hickey, T. J.; Wittenberg, D. K., Rigorous modeling of hybrid systems using interval arithmetic constraints, (Alur, R.; Pappas, G. J., Proc. of Seventh Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2004 (Philadelphia, PA, March 2004). Proc. of Seventh Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2004 (Philadelphia, PA, March 2004), Lecture Notes in Computer Science, vol. 2993 (2004), Springer), 402-416 · Zbl 1135.93341 |
| [40] | Hickey, T.; Ju, Q.; van Emden, M., Interval arithmetic: from principles to implementation, J. ACM, 48, 5, 1038-1068 (2001) · Zbl 1323.65047 |
| [41] | Hu, J.; Lygeros, J.; Sastry, S., Towards a theory of stochastic hybrid systems, (Lynch, N. A.; Krogh, B. H., Proc. of Third Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2000 (Pittsburgh, PA, March 2000). Proc. of Third Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2000 (Pittsburgh, PA, March 2000), Lecture Notes in Computer Science, vol. 1790 (2000), Springer), 160-173 · Zbl 0962.93082 |
| [42] | Koutsoukos, X. D.; Riley, D., Computational methods for reachability analysis of stochastic hybrid systems, (Hespanha, J. P.; Tiwari, A., Proc. of 9th Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2006 (Santa Barbara, CA, March 2006). Proc. of 9th Int. Wksh. on Hybrid Systems: Computation and Control, HSCC 2006 (Santa Barbara, CA, March 2006), Lecture Notes in Computer Science, vol. 3927 (2006), Springer), 377-391 · Zbl 1178.93027 |
| [43] | Littman, M. L.; Majercik, S. M.; Pitassi, T., Stochastic Boolean satisfiability, J. Autom. Reason., 27, 3, 251-296 (2001) · Zbl 0988.68189 |
| [44] | R. Lohner, Einschließung der Lösung gewöhnlicher Anfangs- und Randwertaufgaben, PhD thesis, Univ. Karlsruhe, 1998.; R. Lohner, Einschließung der Lösung gewöhnlicher Anfangs- und Randwertaufgaben, PhD thesis, Univ. Karlsruhe, 1998. |
| [45] | Majercik, S., Nonchronological backtracking in stochastic Boolean satisfiability, (Proc. of 16th IEEE Int. Conf. on Tools with Artificial Intelligence, ICTAI 2004 (Boca Raton, FL, Nov. 2004) (2004), IEEE CS Press), 498-507 |
| [46] | Majercik, S. M., APPSSAT: approximate probabilistic planning using stochastic satisfiability, Int. J. Approx. Reason., 45, 2, 402-419 (2007) · Zbl 1119.68441 |
| [47] | Majercik, S. M., Stochastic Boolean satisfiability, (Biere, A.; Heule, M. J.H.; van Maaren, H.; Walsh, T., Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185 (2009), IOS Press), 887-925 · Zbl 1183.68568 |
| [48] | Majercik, S. M.; Littman, M. L., MAXPLAN: a new approach to probabilistic planning, (Simmons, R. G.; Veloso, M. M.; Smith, S., Proc. of 4th Int. Conf. Artificial Intelligence Planning Systems, AIPS ’98 (Pittsburgh, PA) (1998), AAAI), 86-93 |
| [49] | Makino, K.; Berz, M., Suppression of the wrapping effect by Taylor model-based verified integrators: long-term stabilization by preconditioning, Int. J. Differ. Equ. Appl., 10, 4, 353-384 (2005) · Zbl 1133.65045 |
| [50] | Makino, K.; Berz, M., Suppression of the wrapping effect by Taylor model-based verified integrators: the single step, Int. J. Pure Appl. Math., 36, 2, 175-197 (2006) · Zbl 1131.65060 |
| [51] | Moore, R. E., Interval Analysis (1966), Prentice Hall · Zbl 0176.13301 |
| [52] | Moore, R., Interval Analysis (1966), Prentice-Hall · Zbl 0176.13301 |
| [53] | N.S. Nedialkov, Interval tools for ODEs and DAEs, Tech. Rep. CAS 06-09-NN, McMaster University, Hamilton, ON, 2006. Available online at <http://www.cas.mcmaster.ca/∼;nedialk/PAPERS/intvtools/intvtools.pdf>.; N.S. Nedialkov, Interval tools for ODEs and DAEs, Tech. Rep. CAS 06-09-NN, McMaster University, Hamilton, ON, 2006. Available online at <http://www.cas.mcmaster.ca/∼;nedialk/PAPERS/intvtools/intvtools.pdf>. |
| [54] | Neumaier, A., Interval Methods for Systems of Equations (1990), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0706.15009 |
| [55] | Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), J. ACM, 53, 6, 937-977 (2006) · Zbl 1326.68164 |
| [56] | Papadimitriou, C. H., Games against nature, J. Comput. Syst. Sci., 31, 2, 288-301 (1985) · Zbl 0583.68020 |
| [57] | Pnueli, A., The temporal logic of programs, (Proc. of 18th Ann. Symp. on Foundations of Computer Science, FOCS ’77 (Providence, RI, October-November 1977) (1977), IEEE CS Press), 46-57 |
| [58] | D. Riley, X.D. Koutsoukos, K. Riley, Reachability analysis of a biodiesel production system using stochastic hybrid systems, in: Proc. of 15th IEEE Mediterranean Conf. on Control and Automation, MED ’07 (Athens, June 2007), IEEE, 2007, 6 pp.; D. Riley, X.D. Koutsoukos, K. Riley, Reachability analysis of a biodiesel production system using stochastic hybrid systems, in: Proc. of 15th IEEE Mediterranean Conf. on Control and Automation, MED ’07 (Athens, June 2007), IEEE, 2007, 6 pp. · Zbl 1214.90044 |
| [59] | J. Sproston, Model Checking of Probabilistic Timed and Hybrid Systems, PhD thesis, Univ. of Birmingham, 2000.; J. Sproston, Model Checking of Probabilistic Timed and Hybrid Systems, PhD thesis, Univ. of Birmingham, 2000. · Zbl 0986.68058 |
| [60] | J. Sproston, Decidable model checking of probabilistic hybrid automata, in: M. Joseph (Ed.), Proc. of Sixth Int. Symp. on Formal Techniques for Real-Time and Fault-Tolerant Systems, FTRTFT 2000 (Pune, Sept. 2000), Lecture Notes in Computer Science, vol. 1926, Springer, 2000, pp. 31-45.; J. Sproston, Decidable model checking of probabilistic hybrid automata, in: M. Joseph (Ed.), Proc. of Sixth Int. Symp. on Formal Techniques for Real-Time and Fault-Tolerant Systems, FTRTFT 2000 (Pune, Sept. 2000), Lecture Notes in Computer Science, vol. 1926, Springer, 2000, pp. 31-45. · Zbl 0986.68058 |
| [61] | Teige, T.; Fränzle, M., Stochastic satisfiability modulo theories for non-linear arithmetic, (Perron, L.; Trick, M. A., Proc. of Fifth Int. Conf. on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, CPAIOR 2008 (Paris, May 2008). Proc. of Fifth Int. Conf. on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, CPAIOR 2008 (Paris, May 2008), Lecture Notes in Computer Science, vol. 5015 (2008), Springer), 248-262 · Zbl 1142.68525 |
| [62] | T. Teige, M. Fränzle, Constraint-based analysis of probabilistic hybrid systems, in: A. Giua, C. Mahulea, M. Silva, J. Zaytoon (Eds.), Proc. of Third IFAC Conf. on Analysis and Design of Hybrid Systems, ADHS’09 (Zaragoza, Sept. 2009), IFAC, 2009, pp. 162-167.; T. Teige, M. Fränzle, Constraint-based analysis of probabilistic hybrid systems, in: A. Giua, C. Mahulea, M. Silva, J. Zaytoon (Eds.), Proc. of Third IFAC Conf. on Analysis and Design of Hybrid Systems, ADHS’09 (Zaragoza, Sept. 2009), IFAC, 2009, pp. 162-167. |
| [63] | Walsh, T., Stochastic constraint programming, (van Harmelen, F., Proc. of the 15th Europ. Conf. on Artificial Intelligence, ECAI ’02 (Lyon, July 2002) (2002), IOS Press), 111-115 |
| [64] | Zhang, L.; Madigan, C. F.; Moskewicz, M. H.; Malik, S., Efficient conflict driven learning in a Boolean satisfiability solver, (Proc. of 2001 IEEE/ACM Int. Conf. on Computer-Aided Design, ICCAD ’01 (San Jose, CA, November 2001) (2001), IEEE), 279-285 |
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.
