{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:49:12Z","timestamp":1740098952814,"version":"3.37.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319694825"},{"type":"electronic","value":"9783319694832"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-69483-2_12","type":"book-chapter","created":{"date-parts":[[2017,10,16]],"date-time":"2017-10-16T07:34:48Z","timestamp":1508139288000},"page":"200-215","source":"Crossref","is-referenced-by-count":1,"title":["Reasoning About Periodicity on Infinite Words"],"prefix":"10.1007","author":[{"given":"Wanwei","family":"Liu","sequence":"first","affiliation":[]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[]},{"given":"Ge","family":"Zhou","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,17]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21, 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"12_CR2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-51803-7_22","volume-title":"Temporal Logic in Specification","author":"B Banieqbal","year":"1989","unstructured":"Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 62\u201374. Springer, Heidelberg (1989). doi:\n10.1007\/3-540-51803-7_22"},{"key":"12_CR4","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 1960, pp. 1\u201312, Palo Alto. Stanford University Press (1962)"},{"key":"12_CR5","doi-asserted-by":"crossref","first-page":"101","DOI":"10.2307\/2269030","volume":"1","author":"A Church","year":"1936","unstructured":"Church, A.: A note on the Entscheidungsproblem. J. Symb. Log. 1, 101\u2013102 (1936)","journal-title":"J. Symb. Log."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Schlingloff, B.: Model checking. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. vol. 2, Chapt. 24, pp. 1369\u20131522. MIT and Elsevier Science Publishers (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"12_CR7","unstructured":"Diekert, V., Gastin, P.: First-order definable languages. In: Flum, J., Gr\u00e4del, E., Wilke, T. (eds.) Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], vol. 2, pp. 261\u2013306. Amsterdam University Press (2008)"},{"key":"12_CR8","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare s\u00e4tze der principia mathematica und verwandter system I. Monatshefte f\u00fcr Methematik und Physik 38, 173\u2013198 (1931)","journal-title":"Monatshefte f\u00fcr Methematik und Physik"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-75292-9_20","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2007","author":"M Leucker","year":"2007","unstructured":"Leucker, M., S\u00e1nchez, C.: Regular linear temporal logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 291\u2013305. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-75292-9_20"},{"key":"12_CR10","first-page":"521","volume":"9","author":"R McNaughton","year":"1966","unstructured":"McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Comput. 9, 521\u2013530 (1966)","journal-title":"Inf. Comput."},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE Symposium on Foundation of Computer Science (FOCS 1977), pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"12_CR12","first-page":"1","volume":"141","author":"MO Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1\u201335 (1969)","journal-title":"Trans. AMS"},{"issue":"2\u20133","key":"12_CR13","first-page":"1123","volume":"350","author":"N Schweikardt","year":"2010","unstructured":"Schweikardt, N.: On the expressive power of monadic least fixed point logic. Theor. Comput. Sci. 350(2\u20133), 1123\u20131135 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-39724-3_12","volume-title":"Correct Hardware Design and Verification Methods","author":"R Sebastiani","year":"2003","unstructured":"Sebastiani, R., Tonetta, S.: \u201cMore deterministic\u201d vs. \u201csmaller\u201d B\u00fcchi automata for efficient LTL model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 126\u2013140. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-39724-3_12"},{"key":"12_CR15","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/s100090200070","volume":"4","author":"H Taurainen","year":"2002","unstructured":"Taurainen, H., Heljanko, K.: Testing LTL formula translation into B\u00fcchi automata. STTT 4, 57\u201370 (2002)","journal-title":"STTT"},{"key":"12_CR16","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1016\/S0019-9958(79)90629-6","volume":"42","author":"W Thomas","year":"1979","unstructured":"Thomas, W.: Star-free regular sets of omega-sequences. Inf. Control 42, 148\u2013156 (1979)","journal-title":"Inf. Control"},{"issue":"1","key":"12_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"issue":"1\u20132","key":"12_CR18","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1\u20132), 72\u201399 (1983)","journal-title":"Inf. Control"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-69483-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,16]],"date-time":"2017-10-16T07:38:13Z","timestamp":1508139493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-69483-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319694825","9783319694832"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-69483-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}