{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T05:10:07Z","timestamp":1746335407365,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662445211"},{"type":"electronic","value":"9783662445228"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44522-8_7","type":"book-chapter","created":{"date-parts":[[2014,8,12]],"date-time":"2014-08-12T10:12:23Z","timestamp":1407838343000},"page":"75-86","source":"Crossref","is-referenced-by-count":6,"title":["A Logical Characterization of Timed (non-)Regular Languages"],"prefix":"10.1007","author":[{"given":"Marcello M.","family":"Bersani","sequence":"first","affiliation":[]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[]},{"given":"Pierluigi","family":"San Pietro","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"7_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. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"7_CR2","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R. Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. Journal of the ACM\u00a043(1), 116\u2013146 (1996)","journal-title":"Journal of the ACM"},{"key":"7_CR3","first-page":"390","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Information and Computation\u00a0104, 390\u2013401 (1993)","journal-title":"Information and Computation"},{"issue":"1","key":"7_CR4","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. Journal of the ACM\u00a041(1), 181\u2013204 (1994)","journal-title":"Journal of the ACM"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/978-3-642-24288-5_7","volume-title":"Reachability Problems","author":"M.M. Bersani","year":"2011","unstructured":"Bersani, M.M., Frigeri, A., Rossi, M., San Pietro, P.: Completeness of the bounded satisfiability problem for constraint LTL. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol.\u00a06945, pp. 58\u201371. Springer, Heidelberg (2011)"},{"unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: On the satisfiability of metric temporal logics over the reals. In: Proc. of the Int. Work. on Automated Verification of Critical Systems (AVOCS), pp. 1\u201315 (2013)","key":"7_CR6"},{"doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: A tool for deciding the satisfiability of continuous-time metric temporal logic. In: Proc. of TIME, pp. 99\u2013106 (2013)","key":"7_CR7","DOI":"10.1109\/TIME.2013.20"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-41036-9_8","volume-title":"Reachability Problems","author":"M.M. Bersani","year":"2013","unstructured":"Bersani, M.M., Rossi, M., Pietro, P.S.: Deciding continuous-time metric temporal logic with counting modalities. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol.\u00a08169, pp. 70\u201382. Springer, Heidelberg (2013)"},{"doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: Deciding the satisfiability of MITL specifications. In: Proc. of the Int. Symp. on Games, Automata, Logics and Formal Verification (GandALF), pp. 64\u201378 (2013)","key":"7_CR9","DOI":"10.4204\/EPTCS.119.8"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/978-3-540-70583-3_11","volume-title":"Automata, Languages and Programming","author":"P. Bouyer","year":"2008","unstructured":"Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.B.: On expressiveness and complexity in real-time model checking. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 124\u2013135. Springer, Heidelberg (2008)"},{"issue":"3","key":"7_CR11","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S. Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint LTL. Information and Computation\u00a0205(3), 380\u2013415 (2007)","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"Harel, E., Lichtenstein, O., Pnueli, A.: Explicit clock temporal logic. In: LICS, pp. 402\u2013413. IEEE Computer Society (1990)","key":"7_CR12","DOI":"10.1109\/LICS.1990.113765"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"580","DOI":"10.1007\/BFb0055086","volume-title":"Automata, Languages and Programming","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Raskin, J.-F., Schobbens, P.-Y.: The regular real-time languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 580\u2013591. Springer, Heidelberg (1998)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1007\/3-540-60084-1_93","volume-title":"Automata, Languages and Programming","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Kopke, P.W., Wong-Toi, H.: The expressive power of clocks. In: F\u00fcl\u00f6p, Z., G\u00e9cseg, F. (eds.) ICALP 1995. LNCS, vol.\u00a0944, pp. 417\u2013428. Springer, Heidelberg (1995)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-48168-0_13","volume-title":"Computer Science Logic","author":"Y. Hirshfeld","year":"1999","unstructured":"Hirshfeld, Y., Rabinovich, A.: Quantitative temporal logic. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 172\u2013187. Springer, Heidelberg (1999)"},{"unstructured":"Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. Ph.D. thesis, University of California at Los Angeles (1968)","key":"7_CR16"},{"issue":"4","key":"7_CR17","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R. Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems\u00a02(4), 255\u2013299 (1990)","journal-title":"Real-Time Systems"},{"unstructured":"Microsoft Research: Z3: An efficient SMT solver, http:\/\/z3.codeplex.com","key":"7_CR18"},{"unstructured":"Ostroff, J.S.: Temporal Logic for Real Time Systems. John Wiley & Sons, Inc., New York (1989)","key":"7_CR19"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/11691372_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Ouaknine","year":"2006","unstructured":"Ouaknine, J., Worrell, J.B.: Safety metric temporal logic is fully decidable. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 411\u2013425. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Pradella, M., Morzenti, A., San Pietro, P.: Bounded satisfiability checking of metric temporal logic specifications. ACM Transactions on Software Engineering and Methodology (TOSEM)\u00a022(3) (2013)","key":"7_CR21","DOI":"10.1145\/2491509.2491514"},{"doi-asserted-by":"crossref","unstructured":"Suman, P.V., Pandya, P.K.: An introduction to timed automata, ch.\u00a04, pp. 111\u2013146. World Scientific (2012)","key":"7_CR22","DOI":"10.1142\/9789814271059_0004"},{"unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. of LICS, pp. 332\u2013344 (1986)","key":"7_CR23"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"694","DOI":"10.1007\/3-540-58468-4_191","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"T. Wilke","year":"1994","unstructured":"Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata (extended abstract). In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol.\u00a0863, pp. 694\u2013715. Springer, Heidelberg (1994)"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44522-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T04:29:26Z","timestamp":1746332966000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44522-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662445211","9783662445228"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44522-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}