{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:20:00Z","timestamp":1725484800655},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540430759"},{"type":"electronic","value":"9783540455752"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45575-2_10","type":"book-chapter","created":{"date-parts":[[2007,5,30]],"date-time":"2007-05-30T21:30:22Z","timestamp":1180560622000},"page":"79-94","source":"Crossref","is-referenced-by-count":2,"title":["Accurate Widenings and Boundedness Properties of Timed Systems"],"prefix":"10.1007","author":[{"given":"Supratik","family":"Mukhopadhyay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,12,18]]},"reference":[{"key":"10_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/BFb0084802","volume-title":"CONCUR: Concurrency Theory","author":"R. Alur","year":"1992","unstructured":"R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. Minimization of timed transition systems. In R. Cleaveland, editor, CONCUR: Concurrency Theory, volume 630 of LNCS, pages 340\u2013354. Springer-Verlag, 1992."},{"issue":"2","key":"10_CR2","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":"10_CR3","doi-asserted-by":"crossref","unstructured":"F. Balarin. Approximate reachability analysis of timed automata. In 17th IEEE Real-Time Systems Symposium, pages 52\u201361. IEEE Computer Society Press, 1996.","DOI":"10.1109\/REAL.1996.563700"},{"key":"10_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-63166-6_18","volume-title":"CAV\u201997: Computer Aided Verification","author":"B. Boigelot","year":"1997","unstructured":"B. Boigelot, L. Bronne, and S. Rassart. An improved reachability analysis method for strongly linear hybrid systems. In O. Grumberg, editor, CAV\u201997: Computer Aided Verification, volume 1254 of LNCS, pages 167\u2013178. Springer-Verlag, 1997."},{"key":"10_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":"10_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":"10_CR7","doi-asserted-by":"crossref","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Model Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results, february 1998.","DOI":"10.1145\/325478.325480"},{"key":"10_CR8","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":"10_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"Symbolic verification with periodic sets","author":"B. Boigelot","year":"1994","unstructured":"Bernard Boigelot and Pierre Wolper. Symbolic verification with periodic sets. In David Dill, editor, 6th International Conference on Computer-Aided Verification, volume 818 of LNCS, pages 55\u201367. Springer-Verlag, June 1994."},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In the 4th ACM Symposium on Principles of Programming Languages, 1977.","DOI":"10.1145\/512950.512973"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In the Fifth Annual ACM Symposium on Principles of Programming Languages. ACM Press, 1978.","DOI":"10.1145\/512760.512770"},{"key":"10_CR12","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. InBernhard Steffen, editor, TACAS98: Tools and Algorithms for the Construction of Systems, LNCS 1384, pages 313\u2013329. Springer-Verlag, March\/April 1998."},{"key":"10_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Delay analysis in synchronous programs","author":"N. Halbwachs","year":"1993","unstructured":"N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, the International Conference on Computer-Aided-Verification, volume 697 of LNCS, pages 333\u2013346. Springer-Verlag, 1993."},{"key":"10_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-60472-3_13","volume-title":"Hybrid Systems II","author":"T. A. Henzinger","year":"1995","unstructured":"T. A. Henzinger and P.-H. Ho. A note on abstract-interpretation strategies for hybrid automata. In P. Antsaklis, A. Nerode, W. Kohn, and S. Sastry, editors, Hybrid Systems II, LNCS 999, pages 252\u2013264. Springer-Verlag, 1995."},{"key":"10_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"CAV97: Computer-aided Verification","author":"T. A. Henzinger","year":"1997","unstructured":"T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a model checker for hybrid systems. In O. Grumberg, editor, CAV97: Computer-aided Verification, LNCS 1254, pages 460\u2013463. Springer-Verlag, 1997."},{"key":"10_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/BFb0014712","volume-title":"From quantity to quality","author":"Thomas. A. Henzinger","year":"1997","unstructured":"Thomas. A. Henzinger and Orna Kupferman. From quantity to quality. In Oded Maler, editor, Hybrid and Real-Time Systems International Workshop,Hart\u201997, volume 1201 of LNCS, pages 48\u201362, Grenoble, France, March 1997. Springer-Verlag."},{"key":"10_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":"10_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/BFb0028745","volume-title":"CAV\u201998: Computeraided Verification","author":"T. A. Henzinger","year":"1998","unstructured":"T. A. Henzinger, O. Kupferman, and S. Qadeer. From pre-historic to post-modern symbolic model checking. In A. J. Hu and M. Y. Vardi, editors, CAV\u201998: Computeraided Verification, LNCS 1427, pages 195\u2013206. Springer-Verlag, 1998."},{"issue":"2","key":"10_CR19","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"N. Halbwachs, Y-E. Proy, and P. Romanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157\u2013185, 1997.","journal-title":"Formal Methods in System Design"},{"key":"10_CR20","series-title":"Lect Notes Comput Sci","first-page":"381","volume-title":"Automated analysis of an audio control protocol","author":"P.-H. Ho","year":"1995","unstructured":"Pei-Hsin Ho and Howard Wong-Toi. Automated analysis of an audio control protocol. In P. Wolper, editor, the Seventh Conference on Computer-Aided Verification, pages 381\u2013394, Liege, Belgium, 1995. Springer-Verlag. LNCS 939."},{"issue":"20","key":"10_CR21","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19","author":"J. Jaffar","year":"1994","unstructured":"J. Jaffar and M. J. Maher. Constraint logic programming: A survey. The Journal of Logic Programming, 19\/20:503\u2013582, May\u2013July 1994.","journal-title":"The Journal of Logic Programming"},{"key":"10_CR22","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":"10_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"598","DOI":"10.1007\/3-540-44957-4_40","volume-title":"CL: Computational Logic","author":"S. Mukhopadhyay","year":"2000","unstructured":"S. Mukhopadhyay and A. Podelski. Model checking for timed logic processes. In J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K-K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, and P. J. Stuckey, editors, CL: Computational Logic, LNCS, pages 598\u2013612. Springer, 2000. Available at http:\/\/www.mpi-sb.mpg.de\/?supratik\/ ."},{"key":"10_CR24","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","Perspectives of System Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45575-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T09:34:32Z","timestamp":1556444072000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45575-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430759","9783540455752"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45575-2_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}