{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T06:47:53Z","timestamp":1764053273796,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642287169"},{"type":"electronic","value":"9783642287176"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28717-6_24","type":"book-chapter","created":{"date-parts":[[2012,3,6]],"date-time":"2012-03-06T15:13:04Z","timestamp":1331046784000},"page":"304-319","source":"Crossref","is-referenced-by-count":5,"title":["An Asymptotically Correct Finite Path Semantics for LTL"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Morgenstern","sequence":"first","affiliation":[]},{"given":"Manuel","family":"Gesell","sequence":"additional","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/3-540-36577-X_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Bustan, D., Kupferman, O., Vardi, M.: Resets vs. Aborts in Linear Temporal Logic. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 65\u201380. Springer, Heidelberg (2003)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-77395-5_11","volume-title":"Runtime Verification","author":"A. Bauer","year":"2007","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The Good, the Bad, and the Ugly, But How Ugly Is Ugly? In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol.\u00a04839, pp. 126\u2013138. Springer, Heidelberg (2007)"},{"issue":"3","key":"24_CR3","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A. Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. Journal of Logic and Computation\u00a020(3), 651\u2013674 (2010)","journal-title":"Journal of Logic and Computation"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (2011)","DOI":"10.1145\/2000799.2000800"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/3-540-55719-9_97","volume-title":"Automata, Languages and Programming","author":"E. Chang","year":"1992","unstructured":"Chang, E., Manna, Z., Pnueli, A.: Characterization of Temporal Property Classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 474\u2013486. Springer, Heidelberg (1992)"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C. Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., van Campenhout, D.: Reasoning with Temporal Logic on Truncated Paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 27\u201339. Springer, Heidelberg (2003)"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science: Formal Models and Semantics, vol.\u00a0B, ch.16, pp. 995\u20131072. Elsevier (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"24_CR8","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? Research Report TR-2010-5, Verimag (January 2010)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"24_CR10","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating automata on \u03c9-words. Theoretical Computer Science (TCS)\u00a032, 321\u2013330 (1984)","journal-title":"Theoretical Computer Science (TCS)"},{"key":"24_CR11","unstructured":"Morgenstern, A., Schneider, K., Lamberti, S.: Generating deterministic \u03c9-automata for most LTL formulas by the breakpoint construction. In: Scholl, C., Disch, S. (eds.) Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Freiburg, Germany, pp. 119\u2013128. Shaker (2008)"},{"key":"24_CR12","first-page":"46","volume-title":"Foundations of Computer Science (FOCS)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science (FOCS), pp. 46\u201357. IEEE Computer Society, Providence (1977)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/11813040_38","volume-title":"FM 2006: Formal Methods","author":"A. Pnueli","year":"2006","unstructured":"Pnueli, A., Zaks, A.: PSL Model Checking and Run-Time Verification Via Testers. In: Misra, J., Nipkow, T., Karakostas, G. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 573\u2013586. Springer, Heidelberg (2006)"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Ruf, J., Hoffmann, D., Kropf, T., Rosenstiel, W.: Simulation-guided property checking based on a multi-valued AR-automata. In: Design, Automation and Test in Europe (DATE), Munich, Germany, pp. 742\u2013748. ACM (2001)","DOI":"10.1109\/DATE.2001.915111"},{"key":"24_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-45653-8_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Schneider","year":"2001","unstructured":"Schneider, K.: Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 39\u201354. Springer, Heidelberg (2001)"},{"key":"24_CR16","series-title":"Texts in Theoretical Computer Science (EATCS Series)","volume-title":"Verification of Reactive Systems \u2013 Formal Methods and Algorithms","author":"K. Schneider","year":"2003","unstructured":"Schneider, K.: Verification of Reactive Systems \u2013 Formal Methods and Algorithms. Texts in Theoretical Computer Science (EATCS Series). Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28717-6_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T14:59:26Z","timestamp":1742655566000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28717-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287169","9783642287176"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28717-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}