{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:57:40Z","timestamp":1754485060521},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643562"},{"type":"electronic","value":"9783540697534"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054177","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:43:43Z","timestamp":1153979023000},"page":"263-280","source":"Crossref","is-referenced-by-count":41,"title":["Model checking via reachability testing for timed automata"],"prefix":"10.1007","author":[{"given":"Luca","family":"Aceto","sequence":"first","affiliation":[]},{"given":"Augusto","family":"Burgue\u00f1o","sequence":"additional","affiliation":[]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"18_CR1","unstructured":"L. Aceto, P. Bouyer, A. Burgueno, and K. G. Larsen. The limitations of testing for timed automata, 1997. Forthcoming paper."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"L. Aceto, A. Burgueno, and K. G. Larsen. Model checking via reachability testing for timed automata. Research Report RS-97-29, BRICS, Aalborg University, November 1997.","DOI":"10.7146\/brics.v4i29.18955"},{"key":"18_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:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"18_CR4","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"R. Alur and T.A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181\u2013204, 1994. Preliminary version appears in Proc. 30th FOCS, 1989.","journal-title":"Journal of the ACM"},{"key":"18_CR5","volume-title":"Proc. of the 8th. International Conference on Computer-Aided Verification, CAV'96, volume 1102 of Lecture Notes in Computer Science","author":"J. Bengtsson","year":"1996","unstructured":"J. Bengtsson, D. Griffioen, K. Kristoifersen, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Verification of an audio protocol with bus collision using Uppaal. In R. Alur and T. A. Henzinger, editors, Proc. of the 8th. International Conference on Computer-Aided Verification, CAV'96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, USA, July 31\u2013August 3 1996. Springer-Verlag."},{"key":"18_CR6","unstructured":"J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Uppaal \u2014 a tool suite for automatic verification of real-time systems. In Proc. of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, 22\u201324 October 1995."},{"key":"18_CR7","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R. Nicola De","year":"1984","unstructured":"R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83\u2013133, 1984.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"18_CR8","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computer Machinery, 32(1):137\u2013161, January 1985.","journal-title":"Journal of the Association for Computer Machinery"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: the next generation. In Proc. of the 16th Real-time Systems Symposium, RTSS'95. IEEE Computer Society press, 1995.","DOI":"10.1109\/REAL.1995.495196"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Proc. of the 27th Annual ACM Symposium on Theory of Computing, STOC'95, pages 373\u2013382, 1995. Also appeared as Cornell University technical report TR95-1541.","DOI":"10.1145\/225058.225162"},{"issue":"2","key":"18_CR11","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. A. Henzinger","year":"1994","unstructured":"T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"18_CR12","first-page":"381","volume-title":"Proc. of the 7th. International Conference on Computer-Aided Verification, CAV'95, volume 939 of Lecture Notes in Computer Science","author":"P.-H. Ho","year":"1995","unstructured":"P.-H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. In P. Wolper, editor, Proc. of the 7th. International Conference on Computer-Aided Verification, CAV'95, volume 939 of Lecture Notes in Computer Science, pages 381\u2013394, Lige, Belgium, July 1995. Springer-Verlag."},{"key":"18_CR13","volume-title":"Modelling and analysis of a collision avoidance protocol using SPIN and Uppaal","author":"H. E. Jensen","year":"1996","unstructured":"H. E. Jensen, K. G. Larsen, and A. Skou. Modelling and analysis of a collision avoidance protocol using SPIN and Uppaal. In DIMACS Workshop SPIN '96, 2nd International SPIN Verification Workshop on Algorithms, Applications, Tool Use, Theory. Rutgers University, New Jersey, USA, 1996."},{"key":"18_CR14","unstructured":"K.J. Kristoffersen and P. Pettersson. Modelling and analysis of a steam generator using Uppaal. In Proc. of the 7th Nordic Workshop on Programming Theory, G\u00f6teborg, Sweden, November 1\u20133 1995."},{"key":"18_CR15","first-page":"529","volume-title":"From timed automata to logic \u2014 and back","author":"F. Laroussinie","year":"1995","unstructured":"F. Laroussinie, K. G. Larsen, and C. Weise. From timed automata to logic \u2014 and back. In J. Wiedermann and P. H\u00e1jek, editors, Proc. of the 20th. International Symposium on Mathematical Foundations of Computer Science, MFCS'95, volume 969 of Lecture Notes in Computer Science, pages 529\u2013539, Prague, Czech Republic, August 28\u2013September 1 1995. Springer-Verlag."},{"issue":"1","key":"18_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K. G. Larsen","year":"1991","unstructured":"Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1\u201328, September 1991.","journal-title":"Information and Computation"},{"key":"18_CR17","unstructured":"R. Milner. Communication and Concurrency. Series in Computer Science. Prentice Hall International, 1989."},{"key":"18_CR18","volume-title":"Kronos: a tool for verifying real-time systems. User's guide and reference manual.","author":"A. Olivero","year":"1993","unstructured":"A. Olivero and S. Yovine. Kronos: a tool for verifying real-time systems. User's guide and reference manual. VERIMAG, Grenoble, France, 1993."},{"issue":"1","key":"18_CR19","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/inco.1994.1028","volume":"110","author":"B. Steffen","year":"1994","unstructured":"B. Steffen and A. Ing\u00f3lfsd\u00f3ttir. Characteristic formulae for processes with divergence. Information and Computation, 110(1):149\u2013163, April 1994.","journal-title":"Information and Computation"},{"key":"18_CR20","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. of the 1st. Annual Symposium on Logic in Computer Science, LICS'86, pages 322\u2013331. IEEE Computer Society Press, 1986."},{"key":"18_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Y. Vardi","year":"1994","unstructured":"M. Y. Vardi and P. Wolper. Reasoning about infinte computations. Information and Computation, 115:1\u201337, 1994.","journal-title":"Information and Computation"},{"key":"18_CR22","first-page":"502","volume-title":"Lecture Notes in Computer Science","author":"Y. Wang","year":"1990","unstructured":"Y. Wang. Real-time behaviour of asynchronous agents. In J.C.M. Baeten and J.W. Klop, editors, Proc. of the Conference on Theories of Concurrency: Unification and Extension, CONCUR '90, volume 458 of Lecture Notes in Computer Science, pages 502\u2013520, Amsterdam, The Netherlands, August 27\u201330 1990. Springer-Verlag."},{"key":"18_CR23","volume-title":"PhD thesis","author":"Y. Wang","year":"1991","unstructured":"Y. Wang. A calculus of real time systems. PhD thesis, Chalmers university of Technology, G\u00f6teborg, Sweden, 1991."},{"key":"18_CR24","unstructured":"P. Wolper. Where could SPIN go next? a unifying approach to exploring infinite state spaces. Slides for an invited talk at the 1997 SPIN Workshop, Enschede, The Netherlands. Available at the URL http:\/\/www.montefiore.ulg.ac.be\/~pw\/papers\/psfiles\/SPIN4-97.ps ."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054177","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T08:27:59Z","timestamp":1555748879000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054177"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643562","9783540697534"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/bfb0054177","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}