{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T18:43:41Z","timestamp":1783709021434,"version":"3.55.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030309411","type":"print"},{"value":"9783030309428","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-30942-8_16","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"245-261","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["How Hard Is Finding Shortest Counter-Example Lassos in Model Checking?"],"prefix":"10.1007","author":[{"given":"R\u00fcdiger","family":"Ehlers","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-030-01090-4_20","volume-title":"Automated Technology for Verification and Analysis","author":"K Adabala","year":"2018","unstructured":"Adabala, K., Ehlers, R.: A fragment of linear temporal logic for universal very weak automata. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 335\u2013351. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-01090-4_20"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"554","DOI":"10.1007\/3-540-58027-1_27","volume-title":"Mathematical Foundations of Programming Semantics","author":"H Calbrix","year":"1994","unstructured":"Calbrix, H., Nivat, M., Podelski, A.: Ultimately periodic words of rational w-languages. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 554\u2013566. Springer, Heidelberg (1994). \nhttps:\/\/doi.org\/10.1007\/3-540-58027-1_27"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: 32nd Conference on Design Automation (DAC), pp. 427\u2013432. ACM Press (1995)","DOI":"10.1145\/217474.217565"},{"key":"16_CR4","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: 23rd International Joint Conference on Artificial Intelligence (IJCAI), pp. 854\u2013860. IJCAI\/AAAI (2013)"},{"issue":"2","key":"16_CR5","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1016\/j.scico.2010.03.005","volume":"76","author":"S Edelkamp","year":"2011","unstructured":"Edelkamp, S., Sulewski, D., Barnat, J., Brim, L., Simecek, P.: Flash memory efficient LTL model checking. Sci. Comput. Program. 76(2), 136\u2013157 (2011)","journal-title":"Sci. Comput. Program."},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-642-13089-2_22","volume-title":"Language and Automata Theory and Applications","author":"R Ehlers","year":"2010","unstructured":"Ehlers, R.: Short witnesses and accepting lassos in $$\\omega $$-Automata. In: Dediu, A.-H., Fernau, H., Mart\u00edn-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 261\u2013272. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-13089-2_22"},{"key":"16_CR7","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Series on Integrated Circuits and Systems. Springer, Heidelberg (2006)"},{"issue":"5","key":"16_CR8","doi-asserted-by":"publisher","first-page":"1159","DOI":"10.1137\/S0097539703420675","volume":"34","author":"K Etessami","year":"2005","unstructured":"Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for B\u00fcchi automata. SIAM J. Comput. 34(5), 1159\u20131175 (2005)","journal-title":"SIAM J. Comput."},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-78800-3_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Farzan","year":"2008","unstructured":"Farzan, A., Chen, Y.-F., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Extending automated compositional verification to the full class of omega-regular languages. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 2\u201317. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_2"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-540-24732-6_7","volume-title":"Model Checking Software","author":"P Gastin","year":"2004","unstructured":"Gastin, P., Moro, P., Zeitoun, M.: Minimization of counterexamples in SPIN. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 92\u2013108. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24732-6_7"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-44829-2_8","volume-title":"Model Checking Software","author":"A Groce","year":"2003","unstructured":"Groce, A., Visser, W.: What went wrong: explaining counterexamples. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 121\u2013136. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-44829-2_8"},{"issue":"5","key":"16_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/11817949_33","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"O Kupferman","year":"2006","unstructured":"Kupferman, O., Sheinvald-Faragy, S.: Finding shortest witnesses to the nonemptiness of automata on infinite words. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 492\u2013508. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11817949_33"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer Aided Verification","author":"O Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 172\u2013183. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-48683-6_17"},{"key":"16_CR15","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: 41st Annual Symposium on Foundations of Computer Science (FOCS), pp. 643\u2013652 (2000)"},{"issue":"2\u20133","key":"16_CR16","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-003-0121-x","volume":"5","author":"V Schuppan","year":"2004","unstructured":"Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. STTT 5(2\u20133), 185\u2013204 (2004)","journal-title":"STTT"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-540-31980-1_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Schuppan","year":"2005","unstructured":"Schuppan, V., Biere, A.: Shortest counterexamples for symbolic model checking of LTL with past. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 493\u2013509. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31980-1_32"},{"key":"16_CR18","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31980-1_12"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Tonetta, S.: \u201cmore deterministic\u201d vs. \u201csmaller\u201d B\u00fcchi automata for efficient LTL model checking. In: 12th IFIP WG 10.5 Advanced Research Working Conference (CHARME), Correct Hardware Design and Verification Methods, pp. 126\u2013140 (2003)","DOI":"10.1007\/978-3-540-39724-3_12"},{"issue":"2","key":"16_CR20","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."}],"container-title":["Lecture Notes in Computer Science","Formal Methods \u2013 The Next 30 Years"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30942-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,5]],"date-time":"2020-05-05T06:08:16Z","timestamp":1588658896000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30942-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309411","9783030309428"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30942-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"129","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}