{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:58Z","timestamp":1763468098299},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642335570"},{"type":"electronic","value":"9783642335587"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33558-7_20","type":"book-chapter","created":{"date-parts":[[2012,10,2]],"date-time":"2012-10-02T22:32:47Z","timestamp":1349217167000},"page":"248-264","source":"Crossref","is-referenced-by-count":7,"title":["Solving Temporal Problems Using SMT: Strong Controllability"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Andrea","family":"Micheli","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0004-3702(91)90006-6","volume":"49","author":"R. Dechter","year":"1991","unstructured":"Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artif. Intell.\u00a049, 61\u201395 (1991)","journal-title":"Artif. Intell."},{"key":"20_CR2","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1080\/095281399146607","volume":"11","author":"T. Vidal","year":"1999","unstructured":"Vidal, T., Fargier, H.: Handling contingency in temporal constraint networks: from consistency to controllabilities. Journal of Experimental Theoretical Artificial Intelligence\u00a011, 23\u201345 (1999)","journal-title":"Journal of Experimental Theoretical Artificial Intelligence"},{"key":"20_CR3","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825\u2013885. IOS Press (2009)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT\u00a04 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"20_CR5","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R., Schaafsma, B.: The MathSAT5 SMT solver (2011), \n                    \n                      http:\/\/mathsat.fbk.eu"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"20_CR7","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver (2006), Tool paper at \n                    \n                      http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 150\u2013153. Springer, Heidelberg (2010)"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-04238-6_3","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"I. Niemel\u00e4","year":"2009","unstructured":"Niemel\u00e4, I.: Integrating Answer Set Programming and Satisfiability Modulo Theories. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol.\u00a05753, p. 3. Springer, Heidelberg (2009)"},{"key":"20_CR10","unstructured":"Franz\u00e9n, A., Cimatti, A., Nadel, A., Sebastiani, R., Shalev, J.: Applying SMT in symbolic execution of microcode. In: Bloem, R., Sharygina, N. (eds.) Formal Methods in Computer-Aided Design - FMCAD, pp. 121\u2013128. IEEE (2010)"},{"key":"20_CR11","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Network and Distributed System Security Symposium - NDSS. The Internet Society (2008)"},{"key":"20_CR12","unstructured":"Kleene, S.: Mathematical Logic. J. Wiley & Sons (1967)"},{"key":"20_CR13","first-page":"530","volume-title":"Design Automation Conference - DAC","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Design Automation Conference - DAC, pp. 530\u2013535. ACM Press, New York (2001)"},{"key":"20_CR14","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. J. Wiley & Sons (1998)"},{"key":"20_CR15","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R. Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Computer Journal\u00a036, 450\u2013462 (1993)","journal-title":"Computer Journal"},{"key":"20_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-89439-1_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Monniaux","year":"2008","unstructured":"Monniaux, D.: A Quantifier Elimination Algorithm for Linear Real Arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 243\u2013257. Springer, Heidelberg (2008)"},{"key":"20_CR17","doi-asserted-by":"publisher","first-page":"832","DOI":"10.1145\/182.358434","volume":"26","author":"J.F. Allen","year":"1983","unstructured":"Allen, J.F.: Maintaining knowledge about temporal intervals. Communication of the ACM\u00a026, 832\u2013843 (1983)","journal-title":"Communication of the ACM"},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0004-3702(03)00113-9","volume":"151","author":"I. Tsamardinos","year":"2003","unstructured":"Tsamardinos, I., Pollack, M.E.: Efficient solution techniques for disjunctive temporal reasoning problems. Artificial Intelligence\u00a0151, 43\u201389 (2003)","journal-title":"Artificial Intelligence"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"856","DOI":"10.1007\/978-3-540-74970-7_64","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"B. Peintner","year":"2007","unstructured":"Peintner, B., Venable, K.B., Yorke-Smith, N.: Strong Controllability of Disjunctive Temporal Problems with Uncertainty. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 856\u2013863. Springer, Heidelberg (2007)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/10720246_8","volume-title":"Recent Advances in AI Planning","author":"A. Armando","year":"2000","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-Based Procedures for Temporal Reasoning. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol.\u00a01809, pp. 97\u2013108. Springer, Heidelberg (2000)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1007\/3-540-52885-7_114","volume-title":"10th International Conference on Automated Deduction","author":"T.B. Tour de la","year":"1990","unstructured":"de la Tour, T.B.: Minimizing the Number of Clauses by Renaming. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 558\u2013572. Springer, Heidelberg (1990)"},{"key":"20_CR22","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1613\/jair.3509","volume":"43","author":"L. Planken","year":"2012","unstructured":"Planken, L., de Weerdt, M., van der Krogt, R.: Computing all-pairs shortest paths by leveraging low treewidth. Journal of Artificial Intelligence Research (JAIR)\u00a043, 353\u2013388 (2012)","journal-title":"Journal of Artificial Intelligence Research (JAIR)"},{"key":"20_CR23","unstructured":"Venable, K.B., Volpato, M., Peintner, B., Yorke-Smith, N.: Weak and dynamic controllability of temporal problems with disjunctions and uncertainty. In: Workshop on Constraint Satisfaction Techniques for Planning & Scheduling, pp. 50\u201359 (2010)"},{"key":"20_CR24","unstructured":"Cimatti, A., Micheli, A., Roveri, M.: Solving Temporal Problems using SMT: Weak Controllability. In: Hoffmann, J., Selman, B. (eds.) American Association for Artificial Intelligence - AAAI. AAAI Press (2012)"},{"key":"20_CR25","unstructured":"Morris, P.H., Muscettola, N., Vidal, T.: Dynamic control of plans with temporal uncertainty. In: Nebel, B. (ed.) International Joint Conference on Artificial Intelligence - IJCAI, pp. 494\u2013502. Morgan Kaufmann (2001)"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Barrett, C., Deters, M., de Moura, L., Oliveras, A., Stump, A.: 6 Years of SMT-COMP. Journal of Automated Reasoning (to appear, 2012)","DOI":"10.1007\/s10817-012-9246-5"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11814948_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"S. Cotton","year":"2006","unstructured":"Cotton, S., Maler, O.: Fast and Flexible Difference Constraint Propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 170\u2013183. Springer, Heidelberg (2006)"},{"key":"20_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33558-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,7]],"date-time":"2019-05-07T23:30:48Z","timestamp":1557271848000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33558-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642335570","9783642335587"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33558-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}