{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T05:10:02Z","timestamp":1748581802381,"version":"3.41.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319234038"},{"type":"electronic","value":"9783319234045"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-23404-5_7","type":"book-chapter","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T00:57:19Z","timestamp":1440550639000},"page":"84-101","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Practical Stutter-Invariance Checks for $$\\omega $$-Regular Languages"],"prefix":"10.1007","author":[{"given":"Thibaud","family":"Michaud","sequence":"first","affiliation":[]},{"given":"Alexandre","family":"Duret-Lutz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"key":"7_CR1","unstructured":"Property specification language reference manual v1.1. Accellera (2004). http:\/\/www.eda.org\/vfv\/"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-28756-5_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Babiak","year":"2012","unstructured":"Babiak, T., K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: LTL to B\u00fcchi automata translation: fast and more deterministic. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95\u2013109. Springer, Heidelberg (2012)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"T Babiak","year":"2015","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., K\u0159et\u00ednsk\u00fd, J., M\u00fcller, D., Parker, D., Strej\u010dek, J.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479\u2013486. Springer, Heidelberg (2015)"},{"key":"7_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Parallel partial order reduction with topological sort proviso. In: SEFM 2010, pp. 222\u2013231. IEEE Computer Society Press (2010)","DOI":"10.1109\/SEFM.2010.35"},{"key":"7_CR6","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM\u201999 - Formal Methods","author":"J-M Couvreur","year":"1999","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253\u2013271. Springer, Heidelberg (1999)"},{"key":"7_CR8","first-page":"56","volume":"1","author":"J Dallien","year":"2006","unstructured":"Dallien, J., MacCaull, W.: Automated recognition of stutter-invariant LTL formulas. Atlantic Electron. J. Math. 1, 56\u201374 (2006)","journal-title":"Atlantic Electron. J. Math."},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-04761-9_19","volume-title":"Automated Technology for Verification and Analysis","author":"C Dax","year":"2009","unstructured":"Dax, C., Klaedtke, F., Leue, S.: Specification languages for stutter-invariant regular properties. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 244\u2013254. Springer, Heidelberg (2009)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-319-02444-8_31","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2013","unstructured":"Duret-Lutz, A.: Manipulating LTL formulas using Spot 1.0. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 442\u2013445. Springer, Heidelberg (2013)"},{"issue":"1\/2","key":"7_CR11","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1504\/IJCCBS.2014.059594","volume":"5","author":"A Duret-Lutz","year":"2014","unstructured":"Duret-Lutz, A.: LTL translation improvements in Spot 1.0. Int. J. Crit. Comput.-Based Syst. 5(1\/2), 31\u201354 (2014)","journal-title":"Int. J. Crit. Comput.-Based Syst."},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-48683-6_22","volume-title":"Computer Aided Verification","author":"K Etessami","year":"1999","unstructured":"Etessami, K.: Stutter-invariant languages, $$\\omega $$-automata, and temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 236\u2013248. Springer, Heidelberg (1999)"},{"issue":"6","key":"7_CR13","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/S0020-0190(00)00113-7","volume":"75","author":"K Etessami","year":"2000","unstructured":"Etessami, K.: A note on a question of Peled and Wilke regarding stutter-invariant LTL. Inf. Process. Lett. 75(6), 261\u2013263 (2000)","journal-title":"Inf. Process. Lett."},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/11691617_4","volume-title":"Model Checking Software","author":"J Geldenhuys","year":"2006","unstructured":"Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 53\u201370. Springer, Heidelberg (2006)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"D Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of LTL formul\u00e6 to B\u00fcchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308\u2013326. Springer, Heidelberg (2002)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Hansen, H., Penczek, W., Valmari, A.: Stuttering-insensitive automata for on-the-fly detection of livelock properties. In: FMICS 2002, vol. 66(2) of ENTCS. Elsevier (2002)","DOI":"10.1016\/S1571-0661(04)80411-0"},{"key":"7_CR18","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2003)"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Kupferman, O.: Not checking for closure under stuttering. In: SPIN 1996, pp. 17\u201322. American Mathematical Society (1996)","DOI":"10.1090\/dimacs\/032\/02"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-76336-9_7","volume-title":"Implementation and Application of Automata","author":"J Klein","year":"2007","unstructured":"Klein, J., Baier, C.: On-the-fly stuttering in the construction of deterministic $$\\omega $$-automata. In: Holub, J., \u017d\u010f\u00e1rek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 51\u201361. Springer, Heidelberg (2007)"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Laarman, A., Pater, E., van de Pol, J., Hansen, H.: Guard-based partial-order reduction. In: STTT, pp. 1\u201322 (2014)","DOI":"10.1007\/978-3-642-39176-7_15"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-12920-0_26","volume-title":"STACS 1984","author":"M Michel","year":"1984","unstructured":"Michel, M.: Alg\u00e8bre de machines et logique temporelle. In: Fontet, M., Mehlhorn, K. (eds.) STACS 1984. LNCS, vol. 166, pp. 287\u2013298. Springer, Heidelberg (1984)"},{"issue":"4","key":"7_CR23","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/s00165-002-225-1","volume":"14","author":"DO P\u0103un","year":"2003","unstructured":"P\u0103un, D.O., Chechik, M.: On closure under stuttering. Formal Aspects Comput. 14(4), 342\u2013368 (2003)","journal-title":"Formal Aspects Comput."},{"issue":"5","key":"7_CR24","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D Peled","year":"1997","unstructured":"Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Inf. Process. Lett. 63(5), 243\u2013246 (1997)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"7_CR25","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S0304-3975(97)00219-3","volume":"195","author":"D Peled","year":"1998","unstructured":"Peled, D., Wilke, T., Wolper, P.: An algorithmic approach for checking closure properties of temporal logic specifications and $$\\omega $$-regular languages. Theor. Comput. Sci. 195(2), 183\u2013203 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1007\/978-3-642-45221-5_44","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"E Renault","year":"2013","unstructured":"Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Three SCC-based emptiness checks for generalized B\u00fcchi automata. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 668\u2013682. Springer, Heidelberg (2013)"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-24372-1_28","volume-title":"Automated Technology for Verification and Analysis","author":"V Schuppan","year":"2011","unstructured":"Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 397\u2013413. Springer, Heidelberg (2011)"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Tauriainen, H.: Nested emptiness search for generalized B\u00fcchi automata. In: ACSD 2004, pp. 165\u2013174. IEEE Computer Society (2004)","DOI":"10.1109\/CSD.2004.1309129"},{"issue":"13","key":"7_CR29","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1016\/j.ipl.2009.02.020","volume":"109","author":"C Tian","year":"2009","unstructured":"Tian, C., Duan, Z.: A note on stutter-invariant PLTL. Inf. Process. Lett. 109(13), 663\u2013667 (2009)","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23404-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T04:37:49Z","timestamp":1748579869000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23404-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319234038","9783319234045"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23404-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}