{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:59:08Z","timestamp":1725562748074},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642153488"},{"type":"electronic","value":"9783642153495"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15349-5_5","type":"book-chapter","created":{"date-parts":[[2010,8,21]],"date-time":"2010-08-21T03:39:27Z","timestamp":1282361967000},"page":"76-90","source":"Crossref","is-referenced-by-count":10,"title":["Behavioral Cartography of Timed Automata"],"prefix":"10.1007","author":[{"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Fribourg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"5_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. TCS\u00a0126(2), 183\u2013235 (1994)","journal-title":"TCS"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1145\/167088.167242","volume-title":"STOC \u201993","author":"R. Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC \u201993, pp. 592\u2013601. ACM, New York (1993)"},{"issue":"5","key":"5_CR3","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1142\/S0129054109006905","volume":"20","author":"\u00c9. Andr\u00e9","year":"2009","unstructured":"Andr\u00e9, \u00c9., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. International Journal of Foundations of Computer Science\u00a020(5), 819\u2013836 (2009)","journal-title":"International Journal of Foundations of Computer Science"},{"key":"5_CR4","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., Sproston, J.: An extension of the inverse method to probabilistic timed automata. In: AVoCS\u201909. Electronic Communications of the EASST, vol.\u00a023 (2009)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-642-03466-4_22","volume-title":"Theoretical Aspects of Computing - ICTAC 2009","author":"\u00c9. Andr\u00e9","year":"2009","unstructured":"Andr\u00e9, \u00c9.: IMITATOR: A tool for synthesizing constraints on timing bounds of timed automata. In: Leucker, M., Morgan, C. (eds.) Theoretical Aspects of Computing - ICTAC 2009. LNCS, vol.\u00a05684, pp. 336\u2013342. Springer, Heidelberg (2009)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/3-540-44585-4_34","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2001","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: Trex: A tool for reachability analysis of complex systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 368\u2013372. Springer, Heidelberg (2001)"},{"key":"5_CR7","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"5_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4210-9","volume-title":"Asynchronous Circuits","author":"J.A. Brzozowski","year":"1995","unstructured":"Brzozowski, J.A., Seger, C.J.: Asynchronous Circuits. Springer, Heidelberg (1995)"},{"issue":"1","key":"5_CR9","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10703-008-0061-x","volume":"34","author":"R. Chevallier","year":"2009","unstructured":"Chevallier, R., Encrenaz, E., Fribourg, L., Xu, W.: Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design\u00a034(1), 59\u201381 (2009)","journal-title":"Formal Methods in System Design"},{"key":"5_CR10","volume-title":"ACSD \u201905","author":"R. Claris\u00f3","year":"2005","unstructured":"Claris\u00f3, R., Cortadella, J.: Verification of concurrent systems with parametric delays using octahedra. In: ACSD \u201905. IEEE Computer Society, Los Alamitos (2005)"},{"issue":"1","key":"5_CR11","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.scico.2006.03.009","volume":"64","author":"R. Claris\u00f3","year":"2007","unstructured":"Claris\u00f3, R., Cortadella, J.: The octahedron abstract domain. Sci. Comput. Program.\u00a064(1), 115\u2013139 (2007)","journal-title":"Sci. Comput. Program."},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"5_CR13","unstructured":"Collomb\u2013Annichini, A., Sighireanu, M.: Parameterized reachability analysis of the IEEE 1394 Root Contention Protocol using TReX. In: RT-TOOLS \u201901 (2001)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-78929-1_14","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2008","unstructured":"Frehse, G., Jha, S.K., Krogh, B.H.: A counterexample-guided approach to parameter synthesis for linear hybrid automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol.\u00a04981, pp. 187\u2013200. Springer, Heidelberg (2008)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027241","volume-title":"Formal Methods for Industrial Applications","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A., Wong-Toi, H.: Using HyTech to synthesize control parameters for a steam boiler. In: Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol.\u00a01165, Springer, Heidelberg (1996)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"5_CR17","volume-title":"Spin model checker, the: primer and reference manual","author":"G. Holzmann","year":"2003","unstructured":"Holzmann, G.: Spin model checker, the: primer and reference manual. Addison-Wesley, Reading (2003)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. TCS\u00a0282, 101\u2013150 (2002)","journal-title":"TCS"},{"issue":"3","key":"5_CR20","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s001650300007","volume":"14","author":"M. Kwiatkowska","year":"2003","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects of Computing\u00a014(3), 295\u2013318 (2003)","journal-title":"Formal Aspects of Computing"},{"issue":"7","key":"5_CR21","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Information and Computation\u00a0205(7), 1027\u20131077 (2007)","journal-title":"Information and Computation"},{"issue":"1-2","key":"5_CR22","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/3-540-60385-9_12","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Maler","year":"1995","unstructured":"Maler, O., Pnueli, A.: Timing analysis of asynchronous circuits using timed automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 189\u2013205. Springer, Heidelberg (1995)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.R. D\u2019Argenio","year":"1997","unstructured":"D\u2019Argenio, P.R., Katoen, J.P., Ruys, T.C., Tretmans, G.J.: The bounded retransmission protocol must be on time! In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15349-5_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:51:10Z","timestamp":1619787070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15349-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642153488","9783642153495"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15349-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}