{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:07:46Z","timestamp":1773655666192,"version":"3.50.1"},"reference-count":28,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.3103\/s0146411621070051","type":"journal-article","created":{"date-parts":[[2022,2,1]],"date-time":"2022-02-01T09:15:43Z","timestamp":1643706943000},"page":"776-785","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the Model Checking Problem for Some Extension of CTL*"],"prefix":"10.3103","volume":"55","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1499-2090","authenticated-orcid":false,"given":"A. R.","family":"Gnatenko","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3794-9565","authenticated-orcid":false,"given":"V. A.","family":"Zakharov","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2022,2,1]]},"reference":[{"key":"7404_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R. and Cerny, P., Streaming transducers for algorithmic verification of single-pass list-processing programs, Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011, pp. 599\u2013610.","DOI":"10.1145\/1926385.1926454"},{"key":"7404_CR2","doi-asserted-by":"crossref","unstructured":"Hu, Q. and D\u2019Antoni, L., Automatic program inversion using symbolic transducers, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017, pp. 376\u2013389.","DOI":"10.1145\/3062341.3062345"},{"key":"7404_CR3","doi-asserted-by":"crossref","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., and Bjorner, N., Symbolic finite state transducers: Algorithms and applications, Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012, pp. 137\u2013150.","DOI":"10.1145\/2103656.2103674"},{"key":"7404_CR4","doi-asserted-by":"publisher","first-page":"663","DOI":"10.3103\/S014641161907006X","volume":"53","author":"A.R. Gnatenko","year":"2019","unstructured":"Gnatenko, A.R. and Zakharov, V.A., On the expressive power of some extensions of linear temporal logic, Autom. Control Comput. Sci., 2019, vol. 53, no. 7, pp. 663\u2013675.","journal-title":"Autom. Control Comput. Sci."},{"key":"7404_CR5","unstructured":"Zakharov, D.G., Kozlova, V.A., and Kozlova, D., On the model checking of sequential reactive systems, Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, 2016, vol. 1698, pp. 233\u2013244."},{"key":"7404_CR6","doi-asserted-by":"crossref","unstructured":"Gnatenko, A.R. and Zakharov, V.A., On the model checking of finite state transducers over semigroups, Proc. ISP RAS, 2018, vol. 30, no. 3, pp. 303\u2013324.","DOI":"10.15514\/ISPRAS-2018-30(3)-21"},{"key":"7404_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"2018","unstructured":"Clarke, E.M., Jr., Grumberg, O., Kroening, D., Peled, D., and Veith, H., Model Checking, MIT Press, 2018."},{"key":"7404_CR8","unstructured":"Gnatenko, A.R., On the complexity of model checking problem for finite state transducers over free semigroups, Proceedings of the Student Session of European Summer School on Logic, Language and Information, Riga, 2019."},{"key":"7404_CR9","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J. Hopcro","year":"1979","unstructured":"Hopcro, J. and Ullman, J., Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979."},{"key":"7404_CR10","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., and Stavi, J., On the temporal analysis of fairness, Proceedings of the 7th\u00a0ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1980, pp. 163\u2013173.","DOI":"10.1145\/567446.567462"},{"key":"7404_CR11","doi-asserted-by":"crossref","unstructured":"Manna, Z. and Wolper, P., Synthesis of communicating processes from temporal logic specifications, Workshop on Logic of Programs, Springer, 1981, vol. 131, pp. 253\u2013281.","DOI":"10.1007\/BFb0025786"},{"key":"7404_CR12","doi-asserted-by":"publisher","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, 1983, vol. 56, nos. 1\u20132, pp. 72\u201399.","journal-title":"Inf. Control"},{"key":"7404_CR13","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Piterman, N., and Vardi, M.Y., Extended temporal logic revisited, Proceedings of 12-th International Conference on Concurrency Theory, Springer, 2001, pp. 519\u2013535.","DOI":"10.1007\/3-540-44685-0_35"},{"key":"7404_CR14","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y. and Wolper, P., Yet another process logic, in Lecture Notes in Computer Science, Springer, 1983, vol.\u00a014, pp. 501\u2013512.","DOI":"10.1007\/3-540-12896-4_383"},{"key":"7404_CR15","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y., A temporal fixpoint calculus, Proceedings of the 15-th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1988, pp. 250\u2013259.","DOI":"10.1145\/73560.73582"},{"key":"7404_CR16","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"J.G. Henriksen","year":"1999","unstructured":"Henriksen, J.G. and Thiagarajan, P.S., Dynamic linear time temporal logic, Ann. Pure Appl. Logic, 1999, vol.\u00a096, nos. 1\u20133, pp. 187\u2013207.","journal-title":"Ann. Pure Appl. Logic"},{"key":"7404_CR17","doi-asserted-by":"crossref","unstructured":"Leucker, M. and Sanchez, C., Regular linear temporal logic, Proceedings of the 4-th International Colloquium on Theoretical Aspects of Computing, Springer, 2007, pp. 291\u2013305.","DOI":"10.1007\/978-3-540-75292-9_20"},{"key":"7404_CR18","doi-asserted-by":"publisher","first-page":"2854","DOI":"10.1016\/j.tcs.2010.05.009","volume":"412","author":"R. Mateescu","year":"2011","unstructured":"Mateescu, R., Monteiro, P.T., Dumas, E., and De Jong, H., CTRL: Extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks, Theor. Comput. Sci., 2011, vol. 412, no. 26, pp.\u00a02854\u20132883.","journal-title":"Theor. Comput. Sci."},{"key":"7404_CR19","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., and Wolper, P., Simple on-the-fly automatic verification of linear temporal logic, International Conference on Protocol Specification, Testing and Verification, Springer, 1995, pp. 3\u201318.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"7404_CR20","unstructured":"Vardi, M.Y. and Wolper, P., An automata-theoretic approach to automatic program verification, Proceedings of the First Symposium on Logic in Computer Science, IEEE Comput. Soc., 1986, pp. 322\u2013331."},{"key":"7404_CR21","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"W.J. Savitch","year":"1970","unstructured":"Savitch, W.J., Relationships between nondeterministic and deterministic tape complexities, J. Comput. Syst. Sci., 1970, vol. 4, no. 2, pp. 177\u2013192.","journal-title":"J. Comput. Syst. Sci."},{"key":"7404_CR22","doi-asserted-by":"crossref","unstructured":"Kozen, D., Lower bounds for natural proof systems, Proceedings of the 18-th Symp. on the Foundations of Computer Science, IEEE, 1977, pp. 254\u2013266.","DOI":"10.1109\/SFCS.1977.16"},{"key":"7404_CR23","series-title":"A classification of PLC models and applications","volume-title":"Discrete Event Systems","author":"A. Mader","year":"2000","unstructured":"Mader, A., A classification of PLC models and applications, in Discrete Event Systems, Springer, 2000, vol. 569, pp. 239\u2013246."},{"key":"7404_CR24","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1007\/s10270-014-0448-7","volume":"15","author":"T. Ovatman","year":"2016","unstructured":"Ovatman, T., Aral, A., Polat, D., and Unver, A.O., An overview of model checking practices on verification of PLC software, Software Syst. Model., 2016, vol. 15, no. 4, pp. 937\u2013960.","journal-title":"Software Syst. Model."},{"key":"7404_CR25","first-page":"33","volume":"17","author":"N. Garanina","year":"2020","unstructured":"Garanina, N., Anureev, I., Zyubin, V., Rozov, A., Liakh, T., and Gorlatch, S., Reasoning about programmable logic controllers, Syst. Inf., 2020, vol. 17, pp. 33\u201342.","journal-title":"Syst. Inf."},{"key":"7404_CR26","doi-asserted-by":"publisher","first-page":"510","DOI":"10.3103\/S0146411616070130","volume":"50","author":"E.V. Kuzmin","year":"2016","unstructured":"Kuzmin, E.V., Ryabukhin, D.A., and Sokolov, V.A., On the expressiveness of the approach to constructing PLC-programs by LTL-specification, Autom. Control Comput. Sci., 2016, vol. 50, no. 7, pp. 510\u2013519.","journal-title":"Autom. Control Comput. Sci."},{"key":"7404_CR27","doi-asserted-by":"crossref","unstructured":"Ljungkrantz, O., Akesson, K., Fabian, M., and Yuan, C., A formal specification language for PLC-based control logic, Proceedings of the 8th IEEE International Conference on Industrial Informatics, IEEE, 2010, pp. 1067\u20131072.","DOI":"10.1109\/INDIN.2010.5549591"},{"key":"7404_CR28","doi-asserted-by":"publisher","first-page":"655","DOI":"10.1007\/s10664-012-9232-x","volume":"19","author":"O. Ljungkrantz","year":"2014","unstructured":"Ljungkrantz, O., Akesson, K., Fabian, M., and Ebrahimi, A.H., An empirical study of control logic specifications for programmable logic controllers, Empirical Software Eng., 2014, vol. 19, no. 3, pp. 655\u2013677.","journal-title":"Empirical Software Eng."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411621070051.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411621070051","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411621070051.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:03:51Z","timestamp":1773612231000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411621070051"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":28,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["7404"],"URL":"https:\/\/doi.org\/10.3103\/s0146411621070051","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12]]},"assertion":[{"value":"16 November 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 December 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 December 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 February 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare that they have no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}