{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T23:01:26Z","timestamp":1773615686771,"version":"3.50.1"},"reference-count":28,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"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":[[2022,12]]},"DOI":"10.3103\/s0146411622070057","type":"journal-article","created":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T09:03:26Z","timestamp":1676797406000},"page":"649-660","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Satisfiability and Model Checking for One Parameterized Extension of Linear Temporal Logic"],"prefix":"10.3103","volume":"56","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1499-2090","authenticated-orcid":false,"given":"A. R.","family":"Gnatenko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3794-9565","authenticated-orcid":false,"given":"V. A.","family":"Zakharov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1627","published-online":{"date-parts":[[2023,2,19]]},"reference":[{"key":"7521_CR1","doi-asserted-by":"publisher","unstructured":"Artale, A., Kontchakov, R., Ryzhikov, V., and Zakharyaschev, M., Tractable interval temporal propositional and description logics, Proc. 29th AAAI Conf. on Artificial Intell., 2015, pp. 1417\u20131423. \u00a0https:\/\/doi.org\/10.1609\/aaai.v29i1.9406","DOI":"10.1609\/aaai.v29i1.9406"},{"key":"7521_CR2","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C. and Katoen, J.-P., Principles of Model Checking, Cambridge: MIT Press, 2008."},{"key":"7521_CR3","doi-asserted-by":"publisher","unstructured":"Ben-Ari, M., Manna, Z., and Pnueli, A., The temporal logic of branching time, POPL \u201981: Proc. 8th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Williamsburg, Va., 1981, New York: Association for Computing Machinery, 1981, pp. 164\u2013176. \u00a0https:\/\/doi.org\/10.1145\/567532.567551","DOI":"10.1145\/567532.567551"},{"key":"7521_CR4","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999","unstructured":"Clarke, E. M., Gramberg, O., and Peled, D. A., Model Checking, Cambridge: MIT Press, 1999."},{"key":"7521_CR5","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1006\/inco.1999.2846","volume":"160","author":"K. Etessami","year":"2000","unstructured":"Etessami, K. and Wilke, T., An until hierarchy and other applications of an Ehrenfeucht\u2013Fra\u00efss\u00e9 game for temporal logic, Inf. Comput., 2000, vol. 160, nos. 1\u20132, pp. 88\u2013108. \u00a0https:\/\/doi.org\/10.1006\/inco.1999.2846","journal-title":"Inf. Comput."},{"key":"7521_CR6","doi-asserted-by":"publisher","unstructured":"French, T., Quantified propositional temporal logic with repeating states, 10th Int. Symp. on Temporal Representation and Reasoning, 2003 and Fourth Int. Conf. on Temporal Logic. Proc., Cairns, Australia, 2003, IEEE, 2003, pp. 155\u2013165. \u00a0https:\/\/doi.org\/10.1109\/TIME.2003.1214891","DOI":"10.1109\/TIME.2003.1214891"},{"key":"7521_CR7","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"J.M. Fisher","year":"1979","unstructured":"Fisher, J.M. and Ladner, R.E., Propositional dynamic logic of regular programs, J.\u00a0Comput. Syst. Sci., 1979, vol.\u00a018, no. 2, pp. 194\u2013211. \u00a0https:\/\/doi.org\/10.1016\/0022-0000(79)90046-1","journal-title":"J.\u00a0Comput. Syst. Sci."},{"key":"7521_CR8","doi-asserted-by":"publisher","unstructured":"Gabbay, D., Pnueli, A., Shelach, S., and Stavi, J., The temporal analysis of fairness, POPL \u201980: Proc. 7th ACM Symp. on Principles of Programming Languages, Las Vegas, 1980, New York: Association for Computing Machinery, 1980, pp. 163\u2013173. \u00a0https:\/\/doi.org\/10.1145\/567446.567462","DOI":"10.1145\/567446.567462"},{"key":"7521_CR9","volume-title":"Linear temporal logic and linear dynamic logic on finite traces, Proc. 23th\u00a0Int. Joint Conf. on Artificial Intelligence","author":"G. De Giacomo","year":"2013","unstructured":"De Giacomo, G. and Vardi, M.Y., Linear temporal logic and linear dynamic logic on finite traces, Proc. 23th\u00a0Int. Joint Conf. on Artificial Intelligence, Association for Computing Machinery, 2013, pp. 854\u2013860. https:\/\/hdl.handle.net\/1911\/78495."},{"key":"7521_CR10","volume-title":"On the complexity of verification of automata-transducers over commutative semigroups, Problemy teoreticheskoi kibernetiki (Problems of Theoretical Cybernetics)","author":"A.R. Gnatenko","year":"2017","unstructured":"Gnatenko, A.R. and Zakharov, V.A., On the complexity of verification of automata-transducers over commutative semigroups, Problemy teoreticheskoi kibernetiki (Problems of Theoretical Cybernetics), Zhuravlev, Yu.I., Ed., Moscow: Maks Press, 2017, pp. 68\u201370."},{"key":"7521_CR11","doi-asserted-by":"publisher","first-page":"303","DOI":"10.15514\/ISPRAS-2018-30(3)-21","volume":"30","author":"A.R. Gnatenko","year":"2018","unstructured":"Gnatenko, A.R. and Zakharov, V.A., On the model checking of finite state transducers over semigroups, Tr. Inst. Sist. Anal. Ross. Akad. Nauk, 2018, vol. 30, no. 3, pp. 303\u2013324. \u00a0https:\/\/doi.org\/10.15514\/ISPRAS-2018-30(3)-21","journal-title":"Tr. Inst. Sist. Anal. Ross. Akad. Nauk"},{"key":"7521_CR12","doi-asserted-by":"publisher","first-page":"506","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. 506\u2013524. \u00a0https:\/\/doi.org\/10.3103\/S014641161907006X","journal-title":"Autom. Control Comput. Sci."},{"key":"7521_CR13","doi-asserted-by":"publisher","first-page":"776","DOI":"10.3103\/S0146411621070051","volume":"55","author":"A.R. Gnatenko","year":"2021","unstructured":"Gnatenko, A.R. and Zakharov, V.A., On the model checking problem for some extension of CTL*, Autom. Control Comput. Sci., 2021, vol. 55, no. 7, pp. 776\u2013785. \u00a0https:\/\/doi.org\/10.3103\/S0146411621070051","journal-title":"Autom. Control Comput. Sci."},{"key":"7521_CR14","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"J.J. Henriksen","year":"1996","unstructured":"Henriksen, J.J. and Thiagarajan, P.S., Dynamic linear time temporal logic, Ann. Pure Appl. Logic, 1996, vol. 96, nos. 1\u20133, pp. 187\u2013207. \u00a0https:\/\/doi.org\/10.1016\/S0168-0072(98)00039-6","journal-title":"Ann. Pure Appl. Logic"},{"key":"7521_CR15","unstructured":"Kamp, J.A.W., Tense logic and the theory of linear order, PhD Thesis, Univ. of California, Los Angeles, 1968."},{"key":"7521_CR16","doi-asserted-by":"publisher","unstructured":"Kozen, D., Lower bounds for natural proof systems, 18th Ann. Symp. on Foundations of Computer Science, Providence, R.I., 1977, IEEE, 1977, pp. 254\u2013266. \u00a0https:\/\/doi.org\/10.1109\/SFCS.1977.16","DOI":"10.1109\/SFCS.1977.16"},{"key":"7521_CR17","first-page":"233","volume":"1698","author":"D.G. Kozlova","year":"2016","unstructured":"Kozlova, D.G. and Zakharov, V.A., On the model checking of sequential reactive systems, CEUR Workshop Proc., 2016, vol. 1698, pp. 233\u2013244.","journal-title":"CEUR Workshop Proc."},{"key":"7521_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44685-0_35","volume-title":"Extended temporal logic revisited, CONCUR 2001\u2014Concurrency Theory","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Piterman, N., and Vardi, M.Y., Extended temporal logic revisited, CONCUR 2001\u2014Concurrency Theory, Larsen, K.G. and Nielsen, M., Eds., Lecture Notes in Computer Science, 2154, Berlin: Springer, 2001, pp. 519\u2013535. \u00a0https:\/\/doi.org\/10.1007\/3-540-44685-0_35"},{"key":"7521_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75292-9_20","volume-title":"Regular linear temporal logic, Theoretical Aspects of Computing\u2014ICTAC 2007","author":"M. Leucker","year":"2007","unstructured":"Leucker, M. and S\u00e1nchez, C., Regular linear temporal logic, Theoretical Aspects of Computing\u2014ICTAC 2007, Jones, C.B., Liu, Z., and Woodcock, J., Eds., Lecture Notes in Computer Science, vol. 4711, Berlin: Springer, 2007, pp. 291\u2013305.\u00a0https:\/\/doi.org\/10.1007\/978-3-540-75292-9_20"},{"key":"7521_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z. and Pnueli, A., The Temporal Logic of Reactive and Concurrent Systems: Specification, New York: Springer, 1992. \u00a0https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"key":"7521_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36578-8_7","volume-title":"A spatio-temporal logic for the specification and refinement of mobile systems, Fundamental Approaches to Software Engineering. FASE 2003","author":"S. Merz","year":"2003","unstructured":"Merz, S., Wirsing, M., and Zappe, J., A spatio-temporal logic for the specification and refinement of mobile systems, Fundamental Approaches to Software Engineering. FASE 2003, Pezz\u00e8, M., Ed., Lecture Notes in Computer Science, vol. 2621, Berlin: Springer, 2003, pp. 87\u2013101. \u00a0https:\/\/doi.org\/10.1007\/3-540-36578-8_7"},{"key":"7521_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85778-5_1","volume-title":"Some recent results in metric temporal logic, Formal Modeling and Analysis of Timed Systems. FORMATS 2008","author":"J. Ouaknine","year":"2008","unstructured":"Ouaknine, J. and Worrell, J., Some recent results in metric temporal logic, Formal Modeling and Analysis of Timed Systems. FORMATS 2008, Cassez, F. and Jard, C., Eds., Lecture Notes in Computer Science, vol. 5215, Berlin: Springer, 2008, pp. 1\u201313. \u00a0https:\/\/doi.org\/10.1007\/978-3-540-85778-5_1"},{"key":"7521_CR23","doi-asserted-by":"publisher","unstructured":"Pnueli, A., The temporal logic of programs, 18th Ann. Symp. on Foundations of Computer Science, Providence, R.I., IEEE, 1977, pp. 46\u201357. \u00a0https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"7521_CR24","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. \u00a0https:\/\/doi.org\/10.1016\/S0022-0000(70)80006-X","journal-title":"J. Comput. Syst. Sci."},{"key":"7521_CR25","unstructured":"Vardi, M.Y. and Wolper, P., An automata-theoretic approach to automatic program verification, Proc. First Symp. on Logic in Computer Science, Cambridge, Mass., 1986, IEEE, 1986, pp. 322\u2013331. https:\/\/hdl.handle.net\/2268\/116609."},{"key":"7521_CR26","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.\u00a01\u20132, pp. 72\u201399. \u00a0https:\/\/doi.org\/10.1016\/S0019-9958(83)80051-5","journal-title":"Inf. Control"},{"key":"7521_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23021-4_19","volume-title":"Equivalence checking problem for finite state transducers over semigroups, Algebraic Informatics. CAI 2015","author":"V.A. Zakharov","year":"2015","unstructured":"Zakharov, V.A., Equivalence checking problem for finite state transducers over semigroups, Algebraic Informatics. CAI 2015, Maletti, A., Ed., Lecture Notes in Computer Science, vol. 9270, Cham: Springer, 2015, pp. 208\u2013221.\u00a0https:\/\/doi.org\/10.1007\/978-3-319-23021-4_19"},{"key":"7521_CR28","doi-asserted-by":"publisher","first-page":"523","DOI":"10.3103\/S0146411617070288","volume":"51","author":"V.A. Zakharov","year":"2017","unstructured":"Zakharov, V.A. and Temerbekova, G.G., On the minimization problem for sequential programs, Autom. Control Comput. Sci., 2017, vol. 51, no. 7, pp. 523\u2013530. \u00a0https:\/\/doi.org\/10.3103\/S0146411617070288","journal-title":"Autom. Control Comput. Sci."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411622070057.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411622070057","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411622070057.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:03:19Z","timestamp":1773612199000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411622070057"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12]]},"references-count":28,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["7521"],"URL":"https:\/\/doi.org\/10.3103\/s0146411622070057","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12]]},"assertion":[{"value":"15 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 December 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 December 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2023","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"}}]}}