{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T10:54:48Z","timestamp":1648724088452},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540436317","type":"print"},{"value":"9783540478133","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-47813-2_8","type":"book-chapter","created":{"date-parts":[[2007,5,30]],"date-time":"2007-05-30T22:35:31Z","timestamp":1180564531000},"page":"109-125","source":"Crossref","is-referenced-by-count":0,"title":["Compositional Termination Analysis of Symbolic Forward Analysis"],"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,4,10]]},"reference":[{"key":"8_CR1","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.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems I, LNCS 736, pages 209\u2013229. Springer-Verlag, 1993."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"P. Abdulla, K. Cerans, B. Jonsson, and T. K. Tsay. General decidability theorems for infinite state systems. In LICS, pages 313\u2013321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"issue":"2","key":"8_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":"8_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."},{"key":"8_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/3-540-48320-9_14","volume-title":"CONCUR: Concurrency Theory","author":"B. Berard'","year":"1999","unstructured":"B. Berard' and L. Fribourg. Reachability analysis of (timed) petri nets using real arithmetic. In J. C. M. Baeten and S. Mauw, editors, CONCUR: Concurrency Theory, volume 1664 of LNCS, pages 178\u2013193. Springer-Verlag, 1999."},{"key":"8_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Symbolic model checking of infinite state systems using presburger arithmetics","author":"T. Bultan","year":"1997","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Symbolic model checking of infinite state systems using presburger arithmetics. In Orna Grumberg, editor, the 9th International Conference on Computer Aided Verification (CAV\u201997), LNCS 1254, pages 400\u2013411. Springer, Haifa, Israel, July 1997."},{"key":"8_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":"Johan Bengtsson, Kim. G. Larsen, Fredrik Larsson, Paul Petersson, and Wang Yi. Uppaal in 1995. In T. Margaria and B. Steffen, editors, TACAS, LNCS 1055, pages 431\u2013434. Springer-Verlag, 1996."},{"key":"8_CR8","unstructured":"Bernard Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Universite De Liege, Montefiore, Belgium, 1998."},{"key":"8_CR9","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 Alan J. Hu and M. Y. Vardi, editors, CAV\u201998: Computer Aided Verification, volume 1427 of LNCS, pages 268\u2013279. Springer-Verlag, 1998."},{"key":"8_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Model Checking in CLP","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. Springer-Verlag, March 1999."},{"key":"8_CR11","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 Bernhard Steffen, editor, TACAS98: Tools and Algorithms for the Construction of Systems, LNCS 1384, pages 313\u2013329. Springer-Verlag, March\/April 1998."},{"key":"8_CR12","unstructured":"S. Eilenberg. Automata, Languages and Machines, volume B. Academic Press, 1976."},{"issue":"3","key":"8_CR13","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1023\/A:1009747629591","volume":"2","author":"L. Fribourg","year":"1997","unstructured":"L. Fribourg and H. Olsen. A Decompositional Approach for Computing Least Fixed Point of Datalog Programs with Z-counters. Journal of Constraints, 2(3\u20134):305\u2013336, 1997.","journal-title":"Journal of Constraints"},{"key":"8_CR14","unstructured":"A. Finkel and P. Schnoebelen. Well-structured Transition Systems Everywhere! Technical Report LSV-98-4, Laboratoire Sp\u00e9cification et V\u00e9rification, Ecole Normale Sup\u00e9rieure de Cachan, 1998."},{"key":"8_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-60084-1_85","volume-title":"ICALP 95: Automata, Languages, and Programming","author":"T.A. Henzinger","year":"1995","unstructured":"T.A. Henzinger. Hybrid automata with finite bisimulations. In Z. F\u00fcl\u00f6p and F. G\u00e9cseg, editors, ICALP 95: Automata, Languages, and Programming, LNCS 944, pages 324\u2013335. Springer-Verlag, 1995."},{"key":"8_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-60630-0_3","volume-title":"TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems","author":"T.A. Henzinger","year":"1995","unstructured":"T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to HYTECH. In E. Brinksma, W.R. Cleaveland, K.G. Larsen, T. Margaria, and B. Steffen, editors, TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019, pages 41\u201371. Springer-Verlag, 1995."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. What\u2019s decidable about hybrid automata? In the 27th Annual Symposium on Theory of Computing, pages 373\u2013382. ACM Press, 1995.","DOI":"10.1145\/225058.225162"},{"key":"8_CR18","series-title":"Lect Notes Comput Sci","first-page":"236","volume-title":"Alternating RQ timed automata","author":"W. K. C. Lam","year":"1993","unstructured":"W. K. C. Lam and R. K. Brayton. Alternating RQ timed automata. In Costas Courcoubetis, editor, the 5th International Conference on Computer-Aided Verification, LNCS 697, pages 236\u2013252. Springer-Verlag, June\/July 1993."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"L. Libkin. Variable independence, quantifier elimination, and constraint representations. In ICALP: International Colloqium on Automata Languages and Programming, 2000.","DOI":"10.1007\/3-540-45022-X_23"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, P. Pettersson, and W. Yi. Compositional and symbolic model checking of real-time systems. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 76\u201387. IEEE Computer Society Press, 1995.","DOI":"10.1109\/REAL.1995.495198"},{"key":"8_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-48983-5_15","volume-title":"Hybrid Systems, Computation and Control","author":"G. Lafferriere","year":"1999","unstructured":"G. Lafferriere, G. J. Pappas, and S. Yovine. A new class of decidable hybrid systems. In F. W. Vaandrager and J. H. van Schuppen, editors, Hybrid Systems, Computation and Control, volume 1569 of LNCS, pages 137\u2013151, 1999."},{"issue":"1","key":"8_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/PL00009858","volume":"13","author":"G. Lafferriere","year":"2000","unstructured":"G. Lafferriere, G. J. Pappas, and S. Yovine. O-minimal hybrid systems. Mathematics of Control, Signals and Systems, 13(1):1\u201321, March 2000.","journal-title":"Mathematics of Control, Signals and Systems"},{"key":"8_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/3-540-15199-0_22","volume-title":"TAPSOFT: Theory and Practice of Software","author":"N. G. Leveson","year":"1985","unstructured":"N. G. Leveson and J. L. Stolzy. Analyzing safety and fault tolerance using time petri nets. In H. Uhrig, C. Floyd, M. Nivat, and J. W. Thatcher, editors, TAPSOFT: Theory and Practice of Software, volume 186 of LNCS, pages 339\u2013355. Springer, 1985."},{"key":"8_CR24","series-title":"Lect Notes Comput Sci","first-page":"233","volume-title":"Beyond region graphs: Symbolic forward analysis of timed automata","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."},{"key":"8_CR25","unstructured":"K. S. Namjoshi. Ameliorating the State Explosion Problem. PhD thesis, The Graduate School of the University of Texas at Austin, 1998."},{"key":"8_CR26","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"8","author":"W. Pugh","year":"1992","unstructured":"W. Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 8:102\u2013104, 1992.","journal-title":"Communications of the ACM"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"H. Wong-Toi. Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Stanford University, 1995.","DOI":"10.1142\/9789812831583_0007"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47813-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T09:36:18Z","timestamp":1556444178000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47813-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540436317","9783540478133"],"references-count":27,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-47813-2_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}