{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:48:55Z","timestamp":1768002535461,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540008989","type":"print"},{"value":"9783540365778","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_18","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"254-270","source":"Crossref","is-referenced-by-count":45,"title":["Static Guard Analysis in Timed Automata Verification"],"prefix":"10.1007","author":[{"given":"Gerd","family":"Behrmann","sequence":"first","affiliation":[]},{"given":"Patricia","family":"Bouyer","sequence":"additional","affiliation":[]},{"given":"Emmanuel","family":"Fleury","sequence":"additional","affiliation":[]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An Implementation of Three Algorithms for Timing Verification Based on Automata Emptiness. In Proc. 13th IEEE Real-Time Systems Symp. (RTSS\u201992), pp. 157\u2013166. IEEE Computer Society Press, 1992.","DOI":"10.1109\/REAL.1992.242667"},{"key":"18_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/BFb0084802","volume-title":"Minimization of Timed Transition Systems","author":"R. Alur","year":"1992","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. Minimization of Timed Transition Systems. In Proc. 3rd Int. Conf. on Concurrency Theory (CONCUR\u201992), vol. 630 of LNCS, pp. 340\u2013354. Springer, 1992."},{"issue":"2","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. ATheory ofTimedAutomata. Theoretical Computer Science, 126(2):183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"18_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Efficient Timed Reachability Analysis Using Clock Difference Diagrams","author":"G. Behrmann","year":"1999","unstructured":"G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In Proc. 11th Int. Conf. on Computer Aided Verification (CAV\u201999), vol. 1633 of LNCS, pp. 341\u2013353. Springer, 1999."},{"key":"18_CR5","unstructured":"J. Bengtsson. Clocks, DBMs ans States in Timed Systems. PhD thesis, Dept. of Information Technology, Uppsala Univ., Uppsala, Sweden, 2002."},{"key":"18_CR6","unstructured":"J. Bengtsson, K. G. Larsen, Fredrik Larsson, P. Pettersson, W. Yi, and Carsten Weise. New Generation of uppaal. In Proc. Int. Workshop on Software Tools for Technology Transfer (STTT\u201998), BRICS Notes, pp. 43\u201352, 1998."},{"key":"18_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Diophantine Equations, PresburgerArithmetic and FiniteAutomata","author":"A. Boudet","year":"1996","unstructured":"A. Boudet and H. Comon. Diophantine Equations, PresburgerArithmetic and FiniteAutomata. In Proc. 21st Int. Coll. on Trees in Algebra and Programming (CAAP\u201996), vol. 1059 of LNCS, pp. 30\u201343. Springer, 1996."},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"P. Bouyer. Timed Automata May Cause Some Troubles. Research Report LSV-02-9, LSV, ENS de Cachan, France, 2002.","DOI":"10.7146\/brics.v9i35.21750"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"P. Bouyer. Untameable Timed Automata! In Proc. 20th Annual Symp. on Theoretical Aspects of Computer Science (STACS\u20192003), 2003. To appear.","DOI":"10.1007\/3-540-36494-3_54"},{"key":"18_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1007\/10722167_35","volume-title":"Are timed automata updatable","author":"P. Bouyer","year":"2000","unstructured":"P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Are timed automata updatable? In Proc. 12th Int. Conf. on Computer Aided Verification (CAV\u20192000), vol. 1855 of LNCS, pp. 464\u2013479. Springer, 2000."},{"key":"18_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/3-540-44612-5_19","volume-title":"Expressiveness of updatable timed automata","author":"P. Bouyer","year":"2000","unstructured":"P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Expressiveness of updatable timed automata. In Proc. 25th Int. Symp. on Mathematical Foundations of Computer Science (MFCS\u20192000), vol. 1893 of LNCS, pp. 232\u2013242. Springer, 2000."},{"key":"18_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Kronos: a Model-Checking Tool for Real-Time Systems","author":"M. Bozga","year":"1998","unstructured":"M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: a Model-Checking Tool for Real-Time Systems. In Proc. 10th Int. Conf. on Computer Aided Verification (CAV\u201998), vol. 1427 of LNCS, pp. 546\u2013550. Springer, 1998."},{"key":"18_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/3-540-46002-0_3","volume-title":"Improving the Verification of Timed Systems Using Influence Information","author":"V. Braberman","year":"2002","unstructured":"V. Braberman, D. Garbervetsky, and A. Olivero. Improving the Verification of Timed Systems Using Influence Information. In Proc. 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902), vol. 2280 of LNCS, pp. 21\u201336. Springer, 2002."},{"key":"18_CR14","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model-Checking. The MIT Press, 1999."},{"key":"18_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"Model-Checking of Real-Time Reachability Properties using Abstractions","author":"C. Daws","year":"1998","unstructured":"C. Daws and S. Tripakis. Model-Checking of Real-Time Reachability Properties using Abstractions. In Proc. 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201998), vol. 1384 of LNCS, pp. 313\u2013329. Springer, 1998."},{"key":"18_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Timing Assumptions and Verification of Finite-State Concurrent Systems","author":"D. Dill","year":"1990","unstructured":"D. Dill. Timing Assumptions and Verification of Finite-State Concurrent Systems. In Proc. of theWorkshop on Automatic Verification Methods for Finite State Systems, vol. 407 of LNCS, pp. 197\u2013212. Springer, 1989."},{"key":"18_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-54345-7_57","volume-title":"Solving Systems of Linear Diophantine Equations: an Algebraic Approach","author":"E. Domenjoud","year":"1991","unstructured":"E. Domenjoud. Solving Systems of Linear Diophantine Equations: an Algebraic Approach. In Proc. 16th Int. Symp. on Mathematical Foundations of Computer Science (MFCS\u201991), vol. 520 of LNCS, pp. 141\u2013150. Springer, 1991."},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"K. Havelund, A. Skou, K.G. Larsen, and K. Lund. Formal Modeling and Analysis of an Audio\/Video Protocol: an Industrial Case Study using uppaal. In Proc. 18th IEEE Real-Time Systems Symp. (RTSS\u201997), pp. 2\u201313. IEEE Computer Society Press, 1997.","DOI":"10.1109\/REAL.1997.641264"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"F. Laroussinie and K.G. Larsen. CMC: a Tool for Compositional Model-Checking of Real-Time Systems. In Proc. IFIP Int. Conf. on Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV\u201998), pp. 439\u2013456. Kluwer Academic, 1998.","DOI":"10.1007\/978-0-387-35394-4_27"},{"issue":"1\u20132","key":"18_CR20","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. Software Tools for Technology Transfer, 1(1\u20132):134\u2013152, 1997.","journal-title":"Software Tools for Technology Transfer"},{"key":"18_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/3-540-48168-0_9","volume-title":"Difference Decision Diagrams","author":"J. M\u00f8ller","year":"1999","unstructured":"J. M\u00f8ller, J. Lichtenberg, H.R. Andersen, and H. Hulgaard. Difference Decision Diagrams. In Proc. 13th Int. Workshop on Computer Science Logic (CSL\u201999), vol. 1683 of LNCS, pp. 111\u2013125. Springer, 1999."}],"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\/3-540-36577-X_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:47:47Z","timestamp":1558982867000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]}}}