{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T00:18:28Z","timestamp":1760055508437,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319568409"},{"type":"electronic","value":"9783319568416"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-56841-6_5","type":"book-chapter","created":{"date-parts":[[2017,4,5]],"date-time":"2017-04-05T13:00:33Z","timestamp":1491397233000},"page":"151-194","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Runtime Verification for Linear-Time Temporal Logic"],"prefix":"10.1007","author":[{"given":"Martin","family":"Leucker","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,4,6]]},"reference":[{"key":"5_CR1","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Model-Based Testing of Reactive Systems, Advanced Lectures","year":"2005","unstructured":"Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems, Advanced Lectures. LNCS, vol. 3472. Springer, Heidelberg (2005). The volume is the outcome of a research seminar that was held in Schloss Dagstuhl in January 2004"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Model-based runtime analysis of distributed reactive systems. In: Proceedings of the Australian Software Engineering Conference (ASWEC 2006), pp. 243\u2013252. IEEE (2006)","DOI":"10.1109\/ASWEC.2006.36"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Model-based runtime analysis of distributed reactive systems. In: ASWEC, pp. 243\u2013252 (2006)","DOI":"10.1109\/ASWEC.2006.36"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. (TOSEM), 20(4) (2011, in press)","DOI":"10.1145\/2000799.2000800"},{"key":"5_CR7","volume-title":"Software Engineering Economics","author":"BW Boehm","year":"1981","unstructured":"Boehm, B.W.: Software Engineering Economics. Prentice Hall, Englewood Cliffs (1981)"},{"key":"5_CR8","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Method, and Philosophy of Science, pp. 1\u201312. Stanford University Press, Stanford (1962)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-319-23820-3_21","volume-title":"Runtime Verification","author":"JM Chimento","year":"2015","unstructured":"Chimento, J.M., Ahrendt, W., Pace, G.J., Schneider, G.: StaRVOOrS: a tool for combined static and runtime verification of Java. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 297\u2013305. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-23820-3_21"},{"key":"5_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)"},{"issue":"3","key":"5_CR11","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/TSE.1978.231496","volume":"4","author":"TS Chow","year":"1978","unstructured":"Chow, T.S.: Testing software design modeled by finite-state machines. IEEE Trans. Softw. Eng. 4(3), 178\u2013187 (1978)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR12","unstructured":"Crow, J., Rushby, J.: Model-based reconfiguration: diagnosis and recovery. NASA Contractor report 4596, NASA Langley Research Center (1994)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Chen, F., Rosu, G.: Mop: an efficient and generic runtime verification framework. In: OOPSLA, pp. 569\u2013588 (2007)","DOI":"10.1145\/1297027.1297069"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"issue":"12","key":"5_CR15","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1109\/TSE.2004.91","volume":"30","author":"N Delgado","year":"2004","unstructured":"Delgado, N., Gates, A.Q., Roach, S.: A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Trans. Softw. Eng. 30(12), 859\u2013872 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR16","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., S\u00e1nchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: Runtime monitoring of synchronous systems. In: TIME (2005)"},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/MC.2006.69","volume":"39","author":"MG Hinchey","year":"2006","unstructured":"Hinchey, M.G., Sterritt, R.: Self-managing software. IEEE. Comput. 39(2), 107\u2013109 (2006)","journal-title":"IEEE. Comput."},{"key":"5_CR18","volume-title":"Introduction to Automata Theory, Languages and Computation","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Boston (1979)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-642-35632-2_10","volume-title":"Runtime Verification","author":"M Leucker","year":"2013","unstructured":"Leucker, M.: Sliding between model checking and runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 82\u201387. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-35632-2_10"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, Hyderabad, India, 25\u201329 May 2015, pp. 494\u2013503. IEEE Computer Society (2015)","DOI":"10.1109\/IPDPS.2015.95"},{"key":"5_CR21","volume-title":"The Art of Software Testing","author":"GJ Myers","year":"2004","unstructured":"Myers, G.J.: The Art of Software Testing, 2nd edn. Wiley, Hoboken (2004)","edition":"2"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/11498490_27","volume-title":"Model-Based Testing of Reactive Systems","author":"A Pretschner","year":"2005","unstructured":"Pretschner, A., Leucker, M.: Model-based testing \u2013 a glossary. In: Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.) Model-Based Testing of Reactive Systems. LNCS, vol. 3472, pp. 607\u2013609. Springer, Heidelberg (2005). doi:10.1007\/11498490_27"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"3","key":"5_CR24","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-31980-1_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Schwoon","year":"2005","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 174\u2013190. Springer, Heidelberg (2005). doi:10.1007\/978-3-540-31980-1_12"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Scheffel, T., Schmitz, M.: Three-valued asynchronous distributed runtime verification. In: Twelfth ACM\/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2014, Lausanne, Switzerland, 19\u201321 October 2014, pp. 52\u201361. IEEE (2014)","DOI":"10.1109\/MEMCOD.2014.6961843"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Sen, K., Vardhan, A., Agha, G., Rosu, G.: Efficient decentralized monitoring of safety in distributed systems. In: Finkelstein, A., Estublier, J., Rosenblum, D.S. (eds.) 26th International Conference on Software Engineering (ICSE 2004), 23\u201328 May 2004, Edinburgh, UK, pp. 418\u2013427. IEEE Computer Society (2004)","DOI":"10.1109\/ICSE.2004.1317464"},{"issue":"2","key":"5_CR28","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"5_CR29","first-page":"133","volume-title":"Handbook of Theoretical Computer Science, Volume B","author":"W Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects (Chap. 4). In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B, pp. 133\u2013191. Elsevier Science Publishers B. V., Amsterdam (1990)"},{"issue":"4","key":"5_CR30","doi-asserted-by":"publisher","first-page":"653","DOI":"10.1007\/BF01068590","volume":"9","author":"MP Vasilevski","year":"1973","unstructured":"Vasilevski, M.P.: Failure diagnosis of automata. Cybernetic 9(4), 653\u2013665 (1973)","journal-title":"Cybernetic"},{"key":"5_CR31","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp. 332\u2013344 (1986)"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-56841-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T05:23:29Z","timestamp":1759987409000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-56841-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319568409","9783319568416"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-56841-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"6 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chongqing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 March 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}