{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:06:06Z","timestamp":1725483966872},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439301"},{"type":"electronic","value":"9783540456193"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45619-8_9","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:57:41Z","timestamp":1179586661000},"page":"115-129","source":"Crossref","is-referenced-by-count":2,"title":["Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP"],"prefix":"10.1007","author":[{"given":"Witold","family":"Charatonik","sequence":"first","affiliation":[]},{"given":"Supratik","family":"Mukhopadhyay","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,18]]},"reference":[{"issue":"2","key":"9_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model checking in dense real time. Information and Computation, 104(2):2\u201334, 1993.","journal-title":"Information and Computation"},{"key":"9_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems I","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, T. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R. Grossman, A. Nerode, A. Ravn, and H. Rischel, editors, Hybrid Systems I, LNCS 736, pages 209\u2013229. Springer-Verlag, 1993."},{"issue":"2","key":"9_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2): 183\u2013236, 1994.","journal-title":"Theoretical Computer Science"},{"key":"9_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/3-540-63141-0_6","volume-title":"CONCUR\u201997: Concurrency Theory","author":"R. Alur","year":"1997","unstructured":"R. Alur and T. A. Henzinger. Modularity for timed and hybrid systems. In A. Mazurkiewicz and J. Winkowski, editors, CONCUR\u201997: Concurrency Theory, volume 1243 of LNCS, pages 74\u201388. Springer-Verlag, 1997."},{"doi-asserted-by":"crossref","unstructured":"R. Alur and T. A. Henzinger. Computer-aided verification: An introduction to model building and model checking for concurrent systems, 1999. Book in preparation.","key":"9_CR5","DOI":"10.1007\/BFb0028774"},{"doi-asserted-by":"crossref","unstructured":"K. Apt, H. A. Blair, and A. Walker. Towards a theory of declarative knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 193\u2013214. Morgan Kaufmann, 1988.","key":"9_CR6","DOI":"10.1016\/B978-0-934613-40-8.50006-3"},{"key":"9_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/3-540-61042-1_66","volume-title":"TACAS","author":"J. Bengtsson","year":"1996","unstructured":"J. Bengtsson, K. G. Larsen, F. Larsson, P. Petersson, and W. Yi. Uppaal in 1995. In T. Margaria and B. Steffen, editors, TACAS, LNCS 1055, pages 431\u2013434. Springer-Verlag, 1996."},{"unstructured":"D. Chan. Constructive negation based on the completed database. In R. A. Kowalski and K. A. Bowen, editors, the fifth International Symposium on Logic Programming, pages 111\u2013125. MIT Press, 1988.","key":"9_CR8"},{"doi-asserted-by":"crossref","unstructured":"W. Charatonik, D. McAllester, D. Niwinski, A. Podelski, and I. Walukiewicz. The Horn mu-calculus. In V. Pratt, editor, The 13th IEEE Annual Symposium on Logic in Computer Science, 1998.","key":"9_CR9","DOI":"10.1109\/LICS.1998.705643"},{"key":"9_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/BFb0054183","volume-title":"Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"W. Charatonik","year":"1998","unstructured":"W. Charatonik and A. Podelski. Set-based analysis of reactive infinite-state systems. In B. Steffen, editor, Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of LNCS, pages 358\u2013375, Lisbon, Portugal, March\u2013April 1998. Springer-Verlag."},{"issue":"1","key":"9_CR11","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/227595.227597","volume":"43","author":"W. Chen","year":"1996","unstructured":"W. Chen and D. S. Warren. Tabled evaluation with delaying for general logic programs. JACM, 43(1):20\u201374, 1996.","journal-title":"JACM"},{"key":"9_CR12","volume-title":"Proceedings of INAP\u201995","author":"P. Codognet","year":"1995","unstructured":"P. Codognet. A tabulation method for constraint logic programming. Proceedings of INAP\u201995, Industrial Applications of Prolog, Tokyo, Japan, 1995."},{"key":"9_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"CAV\u201998: Computer Aided Verification","author":"H. Comon","year":"1998","unstructured":"H. Comon and Y. Jurski. Multiple Counters Automata, Safety Analysis, and Presburger Arithmetics. In A. J. Hu and M. Y. Vardi, editors, CAV\u201998: Computer Aided Verification, volume 1427 of LNCS, pages 268\u2013279. Springer-Verlag, 1998."},{"key":"9_CR14","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"PLAP\/ALP98","author":"B. Cui","year":"1998","unstructured":"B. Cui, Y. Dong, X. Du, K. N. Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, A. Roychoudhury, S. A. Smolka, and D.S. Warren. Logic programming and model checking. In PLAP\/ALP98, volume 1490 of LNCS, pages 1\u201320. Springer-Verlag, 1998."},{"key":"9_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"TACAS98: Tools and Algorithms for the Construction of Systems","author":"C. Daws","year":"1998","unstructured":"C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In B. Steffen, editor, TACAS98: Tools and Algorithms for the Construction of Systems, LNCS 1384, pages 313\u2013329. Springer-Verlag, March\/April 1998."},{"key":"9_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201999)","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski. Model Checking in CLP. In R. Cleaveland, editor, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201999), volume 1579 of LNCS, pages 223\u2013239, Amsterdam, The Netherlands, January 1999. Springer-Verlag."},{"unstructured":"X. Du, C. R. Ramakrishnan, and S. A. Smolka. Tabled resolution + constraints: A recipe for model checking real-time systems. In Proceedings of RTSS 2000, 2000.","key":"9_CR17"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002360050074","volume":"34","author":"J. Esparza","year":"1997","unstructured":"J. Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 34:85\u2013107, 1997.","journal-title":"Acta Informatica"},{"issue":"8","key":"9_CR19","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0743-1066(96)00092-1","volume":"32","author":"F. Fages","year":"1997","unstructured":"F. Fages. Constructive negation by prunning. Journal of Logic Programming, 32(8):85\u2013118, August 1997.","journal-title":"Journal of Logic Programming"},{"unstructured":"L. Fribourg and M. V. Peixoto. Concurrent constraint automata. In D. Miller, editor, Logic Programming-Proceedings of the 1993 International Symposium, page 656, Vancouver, Canada, 1993. The MIT Press.","key":"9_CR20"},{"key":"9_CR21","series-title":"Lect Notes Comput Sci","first-page":"20","volume-title":"LOPSTR\u201996: Logic Based Program Synthesis and Transformation","author":"L. Fribourg","year":"1996","unstructured":"L. Fribourg and J. Richardson. Symbolic verification with gap-order constraints. In J. P. Gallagher, editor, LOPSTR\u201996: Logic Based Program Synthesis and Transformation, volume 1207 of LNCS, pages 20\u201337. Springer-Verlag, 1996."},{"doi-asserted-by":"crossref","unstructured":"G. Gottlob, E. Gr\u00e4del, and H. Veith. Linear Time Datalog for Branching Time Logic. In J. Minker, editor, Logic-Based Artificial Intelligence, chapter 19. Kluwer, 2000.","key":"9_CR22","DOI":"10.1007\/978-1-4615-1567-8_19"},{"doi-asserted-by":"crossref","unstructured":"G. Gupta and E. Pontelli. A constraint-based approach for the specification and verification of real-time systems. In K.-J. Lin, editor, IEEE Real-Time Systems Symposium, pages 230\u2013239. IEEE Press, 1997.","key":"9_CR23","DOI":"10.1109\/REAL.1997.641285"},{"issue":"2","key":"9_CR24","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. Henzinger","year":"1994","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193\u2013244, 1994. Special issue for LICS 92.","journal-title":"Information and Computation"},{"key":"9_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/BFb0020933","volume-title":"Hybrid Systems III","author":"Y. Kesten","year":"1996","unstructured":"Y. Kesten, Z. Manna, and A. Pnueli. Verifying clocked transition systems. In R. Alur, T. A. Henzinger, and E. D. Sontag, editors, Hybrid Systems III, volume 1066 of LNCS, pages 13\u201340. Springer-Verlag, 1996."},{"doi-asserted-by":"crossref","unstructured":"K. Marriott and P. J. Stuckey. Programming with Constraints: An Introduction. MIT Press, 1998.","key":"9_CR26","DOI":"10.7551\/mitpress\/5625.001.0001"},{"key":"9_CR27","series-title":"Lect Notes Comput Sci","first-page":"233","volume-title":"19th International Conference on the Foundations of Software Technology and Theoretical Computer Science","author":"S. Mukhopadhyay","year":"1999","unstructured":"S. Mukhopadhyay and A. Podelski. Beyond region graphs: Symbolic forward analysis of timed automata. In C. Pandurangan, V. Raman, and R. Ramanujam, editors, 19th International Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1738 of LNCS, pages 233\u2013245, December 1999."},{"doi-asserted-by":"crossref","unstructured":"S. Mukhopadhyay and A. Podelski. Model checking for timed logic processes. In Proceedings of the First International Conference on Computational Logic (CL), volume 1861 of LNAI, pages 598\u2013612. Springer, 2000.","key":"9_CR28","DOI":"10.1007\/3-540-44957-4_40"},{"doi-asserted-by":"crossref","unstructured":"U. Nilsson and J. L\u00fcbke. Constraint logic programming for local and symbolic model checking. In Proceedings of the First International Conference on Computational Logic (CL), volume 1861 of LNAI, pages 384\u2013398. Springer, 2000.","key":"9_CR29","DOI":"10.1007\/3-540-44957-4_26"},{"doi-asserted-by":"crossref","unstructured":"G. Pemmasani, C. Ramakrishnan, and I. Ramakrishnan. Efficient model checking of real time systems using tabled logic programming and constraints. In This proceedings, 2002.","key":"9_CR30","DOI":"10.1007\/3-540-45619-8_8"},{"doi-asserted-by":"crossref","unstructured":"T. Przymusinski. On the semantics of stratified deductive databases. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 193\u2013216. Morgan Kaufmann, 1988.","key":"9_CR31","DOI":"10.1016\/B978-0-934613-40-8.50009-9"},{"key":"9_CR32","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification (CAV\u201997)","author":"Y. Ramakrishna","year":"1997","unstructured":"Y. Ramakrishna, C. Ramakrishnan, I. Ramakrishnan, S. Smolka, T. Swift, and D. Warren. Efficient model checking using tabled resolution. In Computer Aided Verification (CAV\u201997), volume 1254 of LNCS. Springer-Verlag, June 1997."},{"unstructured":"H. Seki and H. Ito. A query evaluation method for stratified programs under the extended cwa. In R. A. Kowalski and K. A. Bowen, editors, Proceedings of the fifth International Conference and Symposium on Logic Programming, pages 195\u2013211. MIT Press, 1988.","key":"9_CR33"},{"doi-asserted-by":"crossref","unstructured":"P. Stuckey. Negation for constraint logic programming. Information and Computation, 118(1), 1995.","key":"9_CR34","DOI":"10.1006\/inco.1995.1048"},{"doi-asserted-by":"crossref","unstructured":"P. J. Stuckey. Constructive negation for constraint logic programming. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 328\u2013339. IEEE Computer Society Press, 1991.","key":"9_CR35","DOI":"10.1109\/LICS.1991.151657"},{"key":"9_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-16492-8_66","volume-title":"Proceedings of the Third International Conference on Logic Programming","author":"H. Tamaki","year":"1986","unstructured":"H. Tamaki and T. Sato. OLD resolution with tabulation. In E. Shapiro, editor, Proceedings of the Third International Conference on Logic Programming, volume 225 of LNCS, pages 84\u201398, London, 1986. Springer-Verlag."},{"unstructured":"D. Toman. Top-down beats bottom-up for constraint extensions of datalog. In J. Lloyd, editor, Proceedings of the International Symposium on Logic Programming, pages 98\u2013114, Cambridge, Dec. 4\u20137 1995. MIT Press.","key":"9_CR37"},{"key":"9_CR38","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-48778-6_18","volume-title":"Formal Methods in Real time and Probablistic Systems: 5th International AMAST Workshop (ARTS99)","author":"S. Tripakis","year":"1999","unstructured":"S. Tripakis. Verifying progress in timed systems. In J. P. Katoen, editor, Formal Methods in Real time and Probablistic Systems: 5th International AMAST Workshop (ARTS99), volume 1601 of LNCS, pages 299\u2013314. Springer-Verlag, 1999."}],"container-title":["Lecture Notes in Computer Science","Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45619-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:20:58Z","timestamp":1556428858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45619-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439301","9783540456193"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-45619-8_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}