{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T19:21:44Z","timestamp":1725909704499},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319670881"},{"type":"electronic","value":"9783319670898"}],"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-67089-8_7","type":"book-chapter","created":{"date-parts":[[2017,8,24]],"date-time":"2017-08-24T12:47:26Z","timestamp":1503578846000},"page":"87-100","source":"Crossref","is-referenced-by-count":0,"title":["Model Checking CTL over Restricted Classes of Automatic Structures"],"prefix":"10.1007","author":[{"given":"Norbert","family":"Hundeshagen","sequence":"first","affiliation":[]},{"given":"Martin","family":"Lange","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,25]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/3-540-45694-5_9","volume-title":"CONCUR 2002 \u2014 Concurrency Theory","author":"PA Abdulla","year":"2002","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular model checking made simple and effcient. In: Brim, L., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A., Jan\u010dar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 116\u2013131. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45694-5_9"},{"key":"7_CR2","unstructured":"I. Accellera Organization. Formal semantics of Accellera property specification language (2004). In Appendix B. http:\/\/www.eda.org\/vfv\/docs\/PSL-v1.1.pdf"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-16242-8_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Axelsson","year":"2010","unstructured":"Axelsson, R., Hague, M., Kreutzer, S., Lange, M., Latte, M.: Extended computation tree logic. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 67\u201381. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16242-8_6"},{"key":"7_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Berstel, J.: Transductions and Context-Free Languages. Leitf\u00e4den der angewandten Mathematik und Mechanik. Teubner (1979)","DOI":"10.1007\/978-3-663-09367-1"},{"key":"7_CR6","unstructured":"Blumensath, A.: Automatic structures. Master\u2019s thesis, RWTH Aachen (1999)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Blumensath, A., Gr\u00e4del, E.: Automatic structures. In: Proceedings of the 15th Symposium on Logic in Computer Science, LICS 2000, pp. 51\u201362. IEEE (2000)","DOI":"10.1109\/LICS.2000.855755"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372\u2013386. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27813-9_29","DOI":"10.1007\/978-3-540-27813-9_29"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403\u2013418. Springer, Heidelberg (2000). doi: 10.1007\/10722167_31"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Automata, Languages and Programming","author":"O Burkart","year":"1997","unstructured":"Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 419\u2013429. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63165-8_198"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). doi: 10.1007\/BFb0025774"},{"key":"7_CR12","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S1567-8326(02)00025-5","volume":"52\u201353","author":"D Dams","year":"2002","unstructured":"Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. J. Log. Algebr. Program 52\u201353, 109\u2013127 (2002)","journal-title":"J. Log. Algebr. Program"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Demri, S., Goranko, V., Lange, M.: Temporal Logics in Computer Science, volume I - Finite State Systems of Cambridge Tracts in Theor. Comp. Sc. Cambridge Univ. Press (2016)","DOI":"10.1017\/CBO9781139236119"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"EA Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: Bakker, J., Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169\u2013181. Springer, Heidelberg (1980). doi: 10.1007\/3-540-10003-2_69"},{"issue":"3","key":"7_CR15","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"7_CR16","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: On branching versus linear time temporal logic. J. ACM 33(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"issue":"2","key":"7_CR17","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Vojnar, T.: Regular model checking using inference of regular languages. In: Proceedings of the 6th International Workshop on Verification of Infinite-State Systems, INFINITY 2004, vol. 138(3), pp. 21\u201336 (2005)","DOI":"10.1016\/j.entcs.2005.01.044"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BFb0023739","volume-title":"Computer-Aided Verification","author":"K Hamaguchi","year":"1991","unstructured":"Hamaguchi, K., Hiraishi, H., Yajima, S.: Branching time regular temporal logic for model checking with linear time complexity. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 253\u2013262. Springer, Heidelberg (1991). doi: 10.1007\/BFb0023739"},{"issue":"8","key":"7_CR20","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 220\u2013235. Springer, Heidelberg (2000). doi: 10.1007\/3-540-46419-0_16","DOI":"10.1007\/3-540-46419-0_16"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/3-540-63166-6_41","volume-title":"Computer Aided Verification","author":"Y Resten","year":"1997","unstructured":"Resten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 424\u2013435. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63166-6_41"},{"key":"7_CR23","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$ -calculus. TCS 27, 333\u2013354 (1983)","journal-title":"TCS"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-88387-6_6","volume-title":"Automated Technology for Verification and Analysis","author":"R Mateescu","year":"2008","unstructured":"Mateescu, R., Monteiro, P.T., Dumas, E., Jong, H.: Computation tree regular logic for genetic regulatory networks. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 48\u201363. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-88387-6_6"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"A Calculus of Communicating Systems","year":"1980","unstructured":"Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L.: Higher-order model checking: an overview. In: Proceedings of the 30th IEEE Symposium on Logic in Computer Science, LICS 2015, pp. 1\u201315. IEEE Computer Society (2015)","DOI":"10.1109\/LICS.2015.9"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Symposium on Foundations of Computer Science, FOCS 1977, pp. 46\u201357. IEEE, Providence (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR28","series-title":"EATCS Monographs on Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69968-9","volume-title":"Petri Nets (An Introduction)","author":"W Reisig","year":"1985","unstructured":"Reisig, W.: Petri Nets (An Introduction). EATCS Monographs on Theoretical Computer Science, vol. 4. Springer, Heidelberg (1985)"},{"key":"7_CR29","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195218","volume-title":"Elements of Automata Theory","author":"J Sakarovitch","year":"2009","unstructured":"Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, Cambridge (2009)"},{"issue":"1\/2","key":"7_CR30","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"RS Streett","year":"1982","unstructured":"Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Inf. Control 54(1\/2), 121\u2013141 (1982)","journal-title":"Inf. Control"},{"issue":"1\u20132","key":"7_CR31","doi-asserted-by":"crossref","first-page":"259","DOI":"10.3233\/FI-2015-1211","volume":"138","author":"K Sutner","year":"2015","unstructured":"Sutner, K.: Iterating transducers. Fundam. Inf. 138(1\u20132), 259\u2013272 (2015)","journal-title":"Fundam. Inf."},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Touili, T.: Regular model checking using widening techniques. In: Proceedings of the Workshop on Verification of Parameterized Systems, VEPAS 2001. Electr. Notes Theor. Comput. Sci., vol. 50(4), pp. 342\u2013356. Elsevier (2001)","DOI":"10.1016\/S1571-0661(04)00187-2"},{"issue":"1","key":"7_CR33","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":"2","key":"7_CR34","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I Walukiewicz","year":"2001","unstructured":"Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234\u2013263 (2001)","journal-title":"Inf. Comput."},{"issue":"110\u2013111","key":"7_CR35","first-page":"119","volume":"28","author":"P Wolper","year":"1985","unstructured":"Wolper, P.: The tableau method for temporal logic: an overview. Logique Anal. 28(110\u2013111), 119\u2013136 (1985)","journal-title":"Logique Anal."},{"key":"7_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 88\u201397. Springer, Heidelberg (1998). doi: 10.1007\/BFb0028736"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67089-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,16]],"date-time":"2020-10-16T05:21:08Z","timestamp":1602825668000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67089-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319670881","9783319670898"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67089-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}