{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,28]],"date-time":"2024-08-28T07:51:01Z","timestamp":1724831461912},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,10,9]],"date-time":"2010-10-09T00:00:00Z","timestamp":1286582400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J of Log Lang and Inf"],"published-print":{"date-parts":[[2011,4]]},"DOI":"10.1007\/s10849-010-9127-4","type":"journal-article","created":{"date-parts":[[2010,10,13]],"date-time":"2010-10-13T19:22:16Z","timestamp":1286997736000},"page":"169-203","source":"Crossref","is-referenced-by-count":10,"title":["Timed Modal Logics for Real-Time Systems"],"prefix":"10.1007","volume":"20","author":[{"given":"Patricia","family":"Bouyer","sequence":"first","affiliation":[]},{"given":"Franck","family":"Cassez","sequence":"additional","affiliation":[]},{"given":"Fran\u00e7ois","family":"Laroussinie","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,10,9]]},"reference":[{"key":"9127_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Bouyer, P., Burgue\u00f1o, A., & Larsen, K. G. (1998a). The power of reachability testing for timed automata. In V. Arvind, R. Ramanujam (Eds.), Proceedings of the 18th conference on fundations of software technology and theoretical computer science (FSTTCS\u201998) (Vol. 1530, pp. 245\u2013256). Chennai, India: Lecture Notes in Computer Science.","DOI":"10.1007\/978-3-540-49382-2_22"},{"key":"9127_CR2","doi-asserted-by":"crossref","unstructured":"Aceto, L., Burgue\u00f1o, A., & Larsen, K. G. (1998b) Model checking via reachability testing for timed Automata. In Proceedings of the 4th international conference on tools and algorithms for the construction and analysis of systems (TACAS \u201998) (Vol. 1384, pp. 263\u2013280). Lisbon, Portugal, Mar. 1998, Lecture Notes in Computer Science.","DOI":"10.1007\/BFb0054177"},{"issue":"6","key":"9127_CR3","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1051\/ita:2000131","volume":"34","author":"L. Aceto","year":"2000","unstructured":"Aceto L., Ing\u00f3lfsd\u00f3ttir A., Pedersen M. L., Poulsen J. (2000) Characteristic formulae for timed automata. Theoretical Informatics and Applications 34(6): 565\u2013584","journal-title":"Theoretical Informatics and Applications"},{"key":"9127_CR4","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/S1567-8326(02)00022-X","volume":"52\u201353","author":"L. Aceto","year":"2002","unstructured":"Aceto L., Laroussinie F. (2002) Is your model checker on time? On the complexity of model checking for timed modal logics. Journal of Logic and Algebraic Programming 52\u201353: 7\u201351","journal-title":"Journal of Logic and Algebraic Programming"},{"issue":"1","key":"9127_CR5","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur R., Courcoubetis C., Dill D. L. (1993) Model-checking in dense real-time. Information and Computation 104(1): 2\u201334","journal-title":"Information and Computation"},{"key":"9127_CR6","unstructured":"Alur, R., Courcoubetis, C., & Henzinger, T. A. (1994). The observational power of clocks. In Proceedings of the 5th international conference on theory of concurrency (CONCUR \u201994) (Vol. 836, pp. 162\u2013177). Uppsala, Sweden: Lecture Notes in Computer Science."},{"issue":"2","key":"9127_CR7","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur R., Dill D. L. (1994) A theory of timed automata. Theoretical Computer Science 126(2): 183\u2013235","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"9127_CR8","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. (1996) The benefits of relaxing punctuality. Journal of the ACM 43(1): 116\u2013146","journal-title":"Journal of the ACM"},{"key":"9127_CR9","unstructured":"Alur, R., & Henzinger, T. A. (1992). Logics and models of real time: A survey. In Real-time: theory in practice, proceedings of REX workshop (Vol. 600, pp. 74\u2013106). Mook, NL: Lecture Notes in Computer Science, June 1991."},{"issue":"1","key":"9127_CR10","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. (1994) A really temporal logic. Journal of the ACM 41(1): 181\u2013203","journal-title":"Journal of the ACM"},{"key":"9127_CR11","unstructured":"Andersen, H. R. (1995). Partial model checking (Extended Abstract). In Proceedings of the 10th IEEE Symposium (pp. 398\u2013407). San Diego, CA, USA: Logic in Computer Science (LICS \u201995), June 1995."},{"issue":"303","key":"9127_CR12","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/S0304-3975(02)00442-5","volume":"1","author":"A. Arnold","year":"2003","unstructured":"Arnold A., Vincent A., Walukiewicz I. (2003) Games for synthesis of controllers with partial observation. Theoretical Computer Science 1(303): 7\u201334","journal-title":"Theoretical Computer Science"},{"key":"9127_CR13","unstructured":"Bouyer, P., Cassez, F., & Laroussinie, F. (2005). Modal logics for timed control. In M. Abadi, L. de Alfaro (Eds.), Proceedings of the 16th international conference on concurrency theory (CONCUR\u201905) (Vol. 3653, pp. 81\u201394). San Francisco, CA, USA: Lecture Notes in Computer Science."},{"key":"9127_CR14","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Chevalier, F., & Markey, N. (2010). On the expressiveness of TPTL and MTL. Information and Computation. To appear.","DOI":"10.1016\/j.ic.2009.10.004"},{"key":"9127_CR15","unstructured":"Cassez, F., Henzinger, T. A., & Raskin, J.-F. (2002). A comparison of control problems for timed and hybrid systems. In Proceedings of 5th international workshop on hybrid systems: Computation and control (HSCC\u201902), LNCS (Vol. 2289, pp. 134\u2013148)."},{"key":"9127_CR16","unstructured":"Cassez, F., & Laroussinie, F. (2000). Model-checking for hybrid systems by quotienting and constraints solving. In E. A. Emerson, A. P. Sistla (Eds.), Proceedings of the 12th international conference on computer aided verification (CAV 2000) (Vol. 1855, pp. 373\u2013388). Chicago, Illinois, USA: Lecture Notes in Computer Science."},{"key":"9127_CR17","volume-title":"Model checking","author":"E. M. Clarke","year":"1999","unstructured":"Clarke E. M., Grumberg O., Peled D. A. (1999) Model checking. MIT Press, Cambridge"},{"key":"9127_CR18","doi-asserted-by":"crossref","unstructured":"Emerson E. A. (1990) Temporal and modal logic. In: Leeuwen J. v. Handbook of theoretical computer science, Vol. B (Chap. 16). Elsevier, Amsterdam, pp 995\u20131072","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"2","key":"9127_CR19","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. A. Henzinger","year":"1994","unstructured":"Henzinger T. A., Nicollin X., Sifakis J., Yovine S. (1994) Symbolic model checking for real-time systems. Information and Computation 111(2): 193\u2013244","journal-title":"Information and Computation"},{"key":"9127_CR20","unstructured":"Janin, D., & Walukiewicz, I. (1995). Automata for the modal mu-calculus and related results. In Proceedings of the 20th international symposium on mathematical foundations of computer science (MFCS\u201995) (Vol. 969, pp. 552\u2013562). Lecture Notes in Computer Science."},{"key":"9127_CR21","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., & Larsen, K. G. (1995a). Compositional model-checking of real time systems. In I. Lee, S. A. Smolka (Eds.), Proceedings of the 6th international conference on concurrency theory (CONCUR\u201995) (Vol. 962, pp. 529\u2013539). Philadelphia, Pennsylvania, USA: Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-60218-6_3"},{"key":"9127_CR22","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., & Larsen K. G. (1995b). Compositional model checking of real time systems. Technical Report RS-95-19, BRICS.","DOI":"10.7146\/brics.v2i19.19921"},{"key":"9127_CR23","unstructured":"Laroussinie, F., & Larsen, K. G. (1998). CMC: A tool for compositional model-checking of real-time systems. In: S. Budkowski, A. R. Cavalli, E. Najm (Eds.), Proceedings of IFIP TC6 WG6.1 joint international conference on formal description techniques for distributed systems and communication protocols (FORTE\u2019XI) and protocol specification, testing and verification (PSTV\u2019XVIII) (Vol. 135, pp. 439\u2013456) Paris, France: IFIP Conference Proceedings."},{"key":"9127_CR24","unstructured":"Laroussinie, F., Larsen, K. G., & Weise, C. (1995). From timed automata to logic\u2014and Back. In J. Wiedermann, P. H\u00e1jek (Eds.), Proceedings of the 20th international symposium on mathematical fundations of computer science (MFCS\u201995) (Vol. 969, pp. 27\u201341) Prague, Czech Republic: Lecture Notes in Computer Science."},{"key":"9127_CR25","unstructured":"Larsen, K. G., Pettersson, P., & Yi, W. (1995). Model-checking for real-time systems. In Proceedings of the 10th international conference on fundamentals of computation theory (FCT \u201995) (Vol. 965, pp. 62\u201388). Dresden, Germany: Lecture Notes in Computer Science, Aug. 1995."},{"issue":"1\u20132","key":"9127_CR26","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"Larsen K. G., Pettersson P., Yi W. (1997) UPPAAL in a nutshell. Journal of Software Tools for Technology Transfer 1(1\u20132): 134\u2013152","journal-title":"Journal of Software Tools for Technology Transfer"},{"key":"9127_CR27","doi-asserted-by":"crossref","unstructured":"Maler, O., A. Pnueli, & Sifakis, J. (1995). On the synthesis of discrete controllers for timed systems. In Proceedings of the 12th annual symposium on theoretical aspects of computer science (STACS\u201995) (Vol. 900, pp. 229\u2013242). Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-59042-0_76"},{"key":"9127_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna Z., Pnueli A. (1992) The temporal logic of reactive and concurrent systems: Specification. Springer, New York"},{"issue":"2","key":"9127_CR29","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0890-5401(89)90070-9","volume":"81","author":"R. Milner","year":"1989","unstructured":"Milner R. (1989) A complete axiomatisation for observational congruence of finite-state behaviours. Information and Computation 81(2): 227\u2013247","journal-title":"Information and Computation"},{"key":"9127_CR30","unstructured":"Ouaknine, J., & Worrell, J. (2005). On the decidability of metric temporal logic. In Proceedings of the 20th IEEE Symposium. Chicago, IL, USA: Logic in Computer Science (LICS 2005), June 2005."},{"key":"9127_CR31","doi-asserted-by":"crossref","unstructured":"Park, D. (1981). Concurrency and automata on infinite sequences. In Proceedings of the 5th GI Conference on theoretical computer science, Karlsruhe, FRG, Mar. 1981 (Vol. 104, pp. 167\u2013183). Lecture Notes in Computer Science.","DOI":"10.1007\/BFb0017309"},{"issue":"1\u20132","key":"9127_CR32","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine S. (1997) Kronos: A verification tool for real-time systems. Journal of Software Tools for Technology Transfer 1(1\u20132): 123\u2013133","journal-title":"Journal of Software Tools for Technology Transfer"}],"container-title":["Journal of Logic, Language and Information"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-010-9127-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10849-010-9127-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-010-9127-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T12:47:33Z","timestamp":1559738853000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10849-010-9127-4"}},"subtitle":["Specification, Verification and Control"],"short-title":[],"issued":{"date-parts":[[2010,10,9]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,4]]}},"alternative-id":["9127"],"URL":"https:\/\/doi.org\/10.1007\/s10849-010-9127-4","relation":{},"ISSN":["0925-8531","1572-9583"],"issn-type":[{"value":"0925-8531","type":"print"},{"value":"1572-9583","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,10,9]]}}}