{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T03:17:29Z","timestamp":1743131849742,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031684159"},{"type":"electronic","value":"9783031684166"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-68416-6_10","type":"book-chapter","created":{"date-parts":[[2024,8,28]],"date-time":"2024-08-28T07:02:40Z","timestamp":1724828560000},"page":"160-178","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Expressive Timed Modal Mu-Calculus for\u00a0Timed Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4952-5380","authenticated-orcid":false,"given":"Rance","family":"Cleaveland","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5772-9527","authenticated-orcid":false,"given":"Jeroen J. A.","family":"Keiren","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Fontana","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,8,29]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/S1567-8326(02)00022-X","volume":"52\u201353","author":"L Aceto","year":"2002","unstructured":"Aceto, L., Laroussinie, F.: Is your model checker on time? On the complexity of model checking for timed modal logics. J. Logic Algebraic Program. 52\u201353, 7\u201351 (2002). https:\/\/doi.org\/10.1016\/S1567-8326(02)00022-X","journal-title":"J. Logic Algebraic Program."},{"key":"10_CR2","unstructured":"Alur, R.: Techniques for Automatic Verification of Real-Time Systems. Ph.D. thesis (1991). https:\/\/www.cis.upenn.edu\/~alur\/Thesis91.pdf"},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 414\u2013425 (1990).https:\/\/doi.org\/10.1109\/LICS.1990.113766","DOI":"10.1109\/LICS.1990.113766"},{"issue":"1","key":"10_CR4","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993). https:\/\/doi.org\/10.1006\/inco.1993.1024","journal-title":"Inf. Comput."},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Alur, R., et al.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3\u201334 (1995). https:\/\/doi.org\/10.1016\/0304-3975(94)00202-T, hybrid Systems","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"Computer Aided Verification","author":"R Alur","year":"1999","unstructured":"Alur, R.: Timed automata. In: Halbwachs, N., Peled, D. (eds.) Computer Aided Verification, pp. 8\u201322. Springer, Berlin, Heidelberg (1999)"},{"issue":"2","key":"10_CR7","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. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H Andersen","year":"1994","unstructured":"Andersen, H.: Model checking and Boolean graphs. Theor. Comput. Sci. 126(1), 3\u201330 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90266-6","journal-title":"Theor. Comput. Sci."},{"key":"10_CR9","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87\u2013124. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Bhat, G., Cleaveland, R.: Efficient model checking via the equational $$\\mu $$-calculus. In: Proceedings of the 11th Annual IEEE Symposium on Logic and Computer Science (LICS 1996), pp. 304\u2013312. IEEE Computer Society, New Brunswick, NJ, USA (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561358","DOI":"10.1109\/LICS.1996.561358"},{"issue":"2","key":"10_CR13","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/s10849-010-9127-4","volume":"20","author":"P Bouyer","year":"2011","unstructured":"Bouyer, P., Cassez, F., Laroussinie, F.: Timed modal logics for real-time systems. J. Logic Lang. Inform. 20(2), 169\u2013203 (2011). https:\/\/doi.org\/10.1007\/s10849-010-9127-4","journal-title":"J. Logic Lang. Inform."},{"issue":"2","key":"10_CR14","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.ic.2009.10.004","volume":"208","author":"P Bouyer","year":"2010","unstructured":"Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97\u2013116 (2010). https:\/\/doi.org\/10.1016\/j.ic.2009.10.004","journal-title":"Inf. Comput."},{"issue":"2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244\u2013263 (1986). https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"2","key":"10_CR16","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Meth. Syst. Des. 2(2), 121\u2013147 (1993). https:\/\/doi.org\/10.1007\/BF01383878","journal-title":"Formal Meth. Syst. Des."},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Cleaveland, R., Keiren, J.J.A.: Extensible proof systems for infinite-state systems. ACM Trans. Comput. Logic (2023). https:\/\/doi.org\/10.1145\/3622786","DOI":"10.1145\/3622786"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Cleaveland, R., Keiren, J.J.A., Fontana, P.: Expressiveness results for timed modal mu-calculi (2023). https:\/\/doi.org\/10.48550\/arXiv.2310.04100","DOI":"10.48550\/arXiv.2310.04100"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Emerson, E., Halpern, J.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151-178 (1986).https:\/\/doi.org\/10.1145\/4904.4999","DOI":"10.1145\/4904.4999"},{"key":"10_CR20","unstructured":"Emerson, E., Lei, C.L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proceedings of the 1st Symposium on Logic in Computer Science (LICS 1986), pp. 267\u2013278. IEEE Computer Society (1986)"},{"key":"10_CR21","unstructured":"Fontana, P.: Towards a Unified Theory of Timed Automata. Ph.D. thesis, University of Maryland (2014)"},{"key":"10_CR22","unstructured":"Fontana, P., Cleaveland, R.: Data structure choices for on-the-fly model checking of real-time systems. In: Ganai, M., Biere, A. (eds.) Proceedings of the First International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS 2011). CEUR Workshop Proceedings, vol.\u00a0832, pp. 13\u201321. Austin, TX, USA (2011). https:\/\/ceur-ws.org\/Vol-832\/Difts11Proceedings.pdf#page=17"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-319-10512-3_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P Fontana","year":"2014","unstructured":"Fontana, P., Cleaveland, R.: The power of proofs: new algorithms for timed automata model checking. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 115\u2013129. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10512-3_9"},{"issue":"1\u20133","key":"10_CR24","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/S0019-9958(86)80031-6","volume":"68","author":"S Graf","year":"1986","unstructured":"Graf, S., Sifakis, J.: A modal characterization of observational congruence on finite terms of CCS. Inf. Control 68(1\u20133), 125\u2013145 (1986)","journal-title":"Inf. Control"},{"issue":"2","key":"10_CR25","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T Henzinger","year":"1994","unstructured":"Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193\u2013244 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1045","journal-title":"Inf. Comput."},{"key":"10_CR26","unstructured":"Kamp, H.: Tense logic and the theory of linear order. Ph.D. thesis, UCLA (1968)"},{"issue":"3","key":"10_CR27","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983). https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","journal-title":"Theor. Comput. Sci."},{"key":"10_CR28","series-title":"IFIP \u2014 The International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-0-387-35394-4_27","volume-title":"Formal Description Techniques and Protocol Specification, Testing and Verification","author":"F Laroussinie","year":"1998","unstructured":"Laroussinie, F., Larsen, K.G.: CMC: a tool for compositional model-checking of real-time systems. In: Budkowski, S., Cavalli, A., Najm, E. (eds.) Formal Description Techniques and Protocol Specification, Testing and Verification. ITIFIP, vol. 6, pp. 439\u2013456. Springer, Boston, MA (1998). https:\/\/doi.org\/10.1007\/978-0-387-35394-4_27"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/3-540-60246-1_158","volume-title":"Mathematical Foundations of Computer Science 1995","author":"F Laroussinie","year":"1995","unstructured":"Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic \u2014 and back. In: Wiedermann, J., H\u00e1jek, P. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529\u2013539. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60246-1_158"},{"key":"10_CR30","unstructured":"Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. Edition versal 8, Bertz Verlag, Berlin, Germany (1997). http:\/\/doc.utwente.nl\/64253\/"},{"issue":"3","key":"10_CR31","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","volume":"46","author":"R Mateescu","year":"2003","unstructured":"Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci. Comput. Program. 46(3), 255\u2013281 (2003). https:\/\/doi.org\/10.1016\/S0167-6423(02)00094-1","journal-title":"Sci. Comput. Program."},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Penczek, W., P\u00f3lrola, A.: Advances in verification of time petri nets and timed automata. Studies in Computational Intelligence, vol.\u00a020. Springer, Berlin, Heidelberg, Secaucus, NJ, USA (2006).https:\/\/doi.org\/10.1007\/978-3-540-32870-4","DOI":"10.1007\/978-3-540-32870-4"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-45069-6_16","volume-title":"Computer Aided Verification","author":"SA Seshia","year":"2003","unstructured":"Seshia, S.A., Bryant, R.E.: Unbounded, fully symbolic model checking of timed automata using Boolean methods. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 154\u2013166. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_16"},{"key":"10_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-60045-0_52","volume-title":"Computer Aided Verification","author":"OV Sokolsky","year":"1995","unstructured":"Sokolsky, O.V., Smolka, S.A.: Local model checking for real-time systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 211\u2013224. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60045-0_52"},{"issue":"1","key":"10_CR36","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/inco.1994.1028","volume":"110","author":"B Steffen","year":"1994","unstructured":"Steffen, B., Ingolfsdottir, A.: Characteristic formulas for processes with divergence. Inf. Comput. 110(1), 149\u2013163 (1994)","journal-title":"Inf. Comput."},{"issue":"2","key":"10_CR37","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"issue":"1","key":"10_CR38","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10009-003-0135-4","volume":"6","author":"F Wang","year":"2004","unstructured":"Wang, F.: Efficient verification of timed automata with BDD-like data structures. Int. J. Softw. Tools Technol. Transfer 6(1), 77\u201397 (2004). https:\/\/doi.org\/10.1007\/s10009-003-0135-4","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"10_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/11562436_8","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"D Zhang","year":"2005","unstructured":"Zhang, D., Cleaveland, R.: Fast generic model-checking for data-based systems. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 83\u201397. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11562436_8"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-68416-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,28]],"date-time":"2024-08-28T07:05:52Z","timestamp":1724828752000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-68416-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031684159","9783031684166"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-68416-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"QEST+FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Calgary, AB","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.qest-formats.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}