{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:56Z","timestamp":1760202536512,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433668"},{"type":"electronic","value":"9783540459316"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45931-6_19","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T04:53:52Z","timestamp":1181364832000},"page":"264-279","source":"Crossref","is-referenced-by-count":17,"title":["On Model Checking Durational Kripke Structures"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Laroussinie","sequence":"first","affiliation":[]},{"given":"Nicolas","family":"Markey","sequence":"additional","affiliation":[]},{"given":"Philippe","family":"Schnoebelen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,3,15]]},"reference":[{"issue":"1","key":"19_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2\u201334, 1993.","journal-title":"Information and Computation"},{"issue":"1","key":"19_CR2","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R. Alur","year":"1996","unstructured":"R. Alur, T. Feder, and T. A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116\u2013146, 1996.","journal-title":"Journal of the ACM"},{"key":"19_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/BFb0031988","volume-title":"Real-Time: Theory in Practice","author":"R. Alur","year":"1992","unstructured":"R. Alur and T. A. Henzinger. Logics and models of real time: A survey. In Real-Time: Theory in Practice, Proc. REX Workshop, Mook, NL, June 1991, volume 600 of Lecture Notes in Computer Science, pages 74\u2013106. Springer, 1992."},{"issue":"1","key":"19_CR4","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur and T. A. Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation, 104(1):35\u201377, 1993.","journal-title":"Information and Computation"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"R. Alur and T. A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181\u2013203, 1994.","journal-title":"Journal of the ACM"},{"key":"19_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/3-540-48340-3_12","volume-title":"Proc. 24th Int. Symp. Math. Found. Comp. Sci. (MFCS\u201999)","author":"L. Aceto","year":"1999","unstructured":"L. Aceto and F. Laroussinie. Is your model checker on time? In Proc. 24th Int. Symp. Math. Found. Comp. Sci. (MFCS\u201999), Szklarska Poreba, Poland, Sep. 1999, volume 1672 of Lecture Notes in Computer Science, pages 125\u2013136. Springer, 1999."},{"key":"19_CR7","unstructured":"R. Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Stanford Univ., August 1991. Available as Tech. Report STAN-CS-91-1378."},{"key":"19_CR8","unstructured":"E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999."},{"key":"19_CR9","unstructured":"T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to algorithms. MIT Press, 1990."},{"issue":"4","key":"19_CR10","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/BF00709157","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-time systems. Formal Methods in System Design, 1(4):385\u2013415, 1992.","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"19_CR11","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E. A. Emerson","year":"1987","unstructured":"E. A. Emerson and Chin-Laung Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, chapter 16, pages 995\u20131072. Elsevier Science, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"4","key":"19_CR13","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"E. A. Emerson","year":"1992","unstructured":"E. A. Emerson, A. K. Mok, A. P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. Real-Time Systems, 4(4):331\u2013352, 1992.","journal-title":"Real-Time Systems"},{"key":"19_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BFb0030596","volume-title":"Proc. 7th Int. Joint Conf. Theory and Practice of Software Development (TAPSOFT\u201997)","author":"E. A. Emerson","year":"1997","unstructured":"E. A. Emerson and R. J. Trefler. Generalized quantitative temporal reasoning: An automata-theoretic approach. In Proc. 7th Int. Joint Conf. Theory and Practice of Software Development (TAPSOFT\u201997), Lille, France, Apr. 1997, volume 1214 of Lecture Notes in Computer Science, pages 189\u2013200. Springer, 1997."},{"key":"19_CR15","first-page":"336","volume-title":"Proc. 14th IEEE Symp. Logic in Computer Science (LICS\u201999)","author":"E. A. Emerson","year":"1999","unstructured":"E. A. Emerson and R. J. Trefler. Parametric quantitative temporal reasoning. In Proc. 14th IEEE Symp. Logic in Computer Science (LICS\u201999), Trento, Italy, July 1999, pages 336\u2013343. IEEE Comp. Soc. Press, 1999."},{"key":"19_CR16","unstructured":"M. R. Garey and D. S. Johnson. Computers and Intractability. A Guide to the Theory of NP-Completeness. Freeman, 1979."},{"key":"19_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/BFb0055640","volume-title":"Proc. 9th Int. Conf. Concurrency Theory (CONCUR\u201998)","author":"T. A. Henzinger","year":"1998","unstructured":"T. A. Henzinger. It\u2019s about time: real-time logics reviewed. In Proc. 9th Int. Conf. Concurrency Theory (CONCUR\u201998), Nice, France, Sep. 1998, volume 1466 of Lecture Notes in Computer Science, pages 439\u2013454. Springer, 1998."},{"issue":"3","key":"19_CR18","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1016\/0022-0000(88)90039-6","volume":"36","author":"M. W. Krentel","year":"1988","unstructured":"M. W. Krentel. The complexity of optimization problems. Journal of Computer and System Sciences, 36(3):490\u2013509, 1988.","journal-title":"Journal of Computer and System Sciences"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"H. R. Lewis. A logic of concrete time intervals (extended abstract). In Proc. 5th IEEE Symp. Logic in Computer Science (LICS\u201990), Philadelphia, PA, USA, June 1990, pages 380\u2013389. IEEE Comp. Soc. Press, 1990.","DOI":"10.1109\/LICS.1990.113763"},{"key":"19_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-45315-6_21","volume-title":"Proc. 4th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS\u20192001)","author":"F. Laroussinie","year":"2001","unstructured":"F. Laroussinie, N. Markey, and Ph. Schnoebelen. Model checking CTL+ and FCTL is hard. In Proc. 4th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS\u20192001), Genova, Italy, Apr. 2001, volume 2030 of Lecture Notes in Computer Science, pages 318\u2013331. Springer, 2001."},{"key":"19_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/10719839_43","volume-title":"Proc. 4th Latin American Symposium on Theoretical Informatics (LATIN\u20192000)","author":"F. Laroussinie","year":"2000","unstructured":"F. Laroussinie, Ph. Schnoebelen, and M. Turuani. On the expressivity and complexity of quantitative branching-time temporal logics. In Proc. 4th Latin American Symposium on Theoretical Informatics (LATIN\u20192000), Punta del Este, Uruguay, Apr. 2000, volume 1776 of Lecture Notes in Computer Science, pages 437\u2013446. Springer, 2000."},{"issue":"2","key":"19_CR22","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1109\/71.80145","volume":"1","author":"J. S. Ostroff","year":"1990","unstructured":"J. S. Ostroff. Deciding properties of timed transition models. IEEE Transactions on Parallel and Distributed Systems, 1(2):170\u2013183, 1990.","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"issue":"2","key":"19_CR23","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1145\/62.322435","volume":"31","author":"C. H. Papadimitriou","year":"1984","unstructured":"C. H. Papadimitriou. On the complexity of unique solutions. Journal of the ACM, 31(2):392\u2013400, 1984.","journal-title":"Journal of the ACM"},{"key":"19_CR24","unstructured":"C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994."},{"issue":"1","key":"19_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"L. J. Stockmeyer","year":"1976","unstructured":"L. J. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3(1):1\u201322, 1976.","journal-title":"Theoretical Computer Science"},{"issue":"1\u20132","key":"19_CR26","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/0304-3975(87)90049-1","volume":"51","author":"K. W. Wagner","year":"1987","unstructured":"K. W. Wagner. More complicated questions about maxima and minima, and some closures of NP. Theoretical Computer Science, 51(1\u20132):53\u201380, 1987.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45931-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T04:20:19Z","timestamp":1737087619000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45931-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433668","9783540459316"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-45931-6_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}