maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2021-4-356-371mais-1565Research ArticleTheory of ComputingО верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времениOn the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logichttps://orcid.org/0000-0003-1499-2090ГнатенкоАнтон РомановичGnatenkoAnton Romanovichgnatenko.cmc@gmail.comhttps://orcid.org/0000-0002-3794-9565ЗахаровВладимир АнатольевичZakharovVladimir Anatolyevichzakh@cs.msu.suНациональный исследовательский университет “Высшая школа экономики”РоссияNational Research University Higher School of Economics (HSE)Russian FederationНациональный исследовательский университет “Высшая школа экономики”;Институт системного программирования им. В. П. Иванникова РАНРоссияNational Research University Higher School of Economics (HSE);Ivannikov Institute for System Programming of the RASRussian Federation202118122021284356371Copyright © Гнатенко А.Р., Захаров В.А., 20212021Гнатенко А.Р., Захаров В.А.Gnatenko A.R., Zakharov V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1565

К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, представляющих собой расширение темпоральных логик $LTL$, $CTL$ и $CTL^*$ за счет использования регулярных языков в качестве параметров темпоральных операторов. Мы провели сравнительный анализ выразительных возможностей нового расширения темпоральной логики линейного времени $Reg$-$LTL$ и предложили алгоритмы верификации моделей для новых расширений логик $Reg$-$LTL$, $Reg$-$CTL$, и $Reg$-$CTL^*$. Однако вопрос о сложности задач верификации моделей и проверки выполнимости формул указанных логик оставался открытым. В этой статье мы восполняем этот пробел в наших исследованиях и показываем, что для темпоральной логики $Reg$-$LTL$ обе задачи являются Pspace-полными. Вычислительная трудность рассматриваемых задач легко доказывается сведением к ним проблемы пустоты пересечения семейств регулярных языков. Основным результатом статьи является алгоритм сведения задачи проверки выполнимости формул логики $Reg$-$LTL$ к проблеме пустоты автоматов Бюхи сравнительно небольшого размера и описание стратегии, позволяющей проверять пустоту полученных автоматов с использованием объема памяти, полиномального относительно размера исходных формул.

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.

темпоральные логикирегулярный языкавтомат-преобразовательверификация моделейпроверка выполнимостиавтоматы Бюхипроблема пустотыtemporal logicsregular languagetransducermodel checkingsatisfiability checkingBuchi automataemptiness problemReferencesA. Pnueli, “The temporal logic of programs,” in Proceedings of the 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46-57.A. Pnueli, “The temporal logic of programs,” in Proceedings of the 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46-57.D. Gabbay, A. Pnueli, S. Shelach, and J. Stavi, “The temporal analysis of fairness,” in Proceedings of 7-th ACM Symposium on Principles of Programming Languages, 1980, pp. 163-173.D. Gabbay, A. Pnueli, S. Shelach, and J. Stavi, “The temporal analysis of fairness,” in Proceedings of 7-th ACM Symposium on Principles of Programming Languages, 1980, pp. 163-173.M. Ben-Ari, Z. Manna, and A. Pnueli, “The temporal logic of branching time,” in Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1981, pp. 164-176.M. Ben-Ari, Z. Manna, and A. Pnueli, “The temporal logic of branching time,” in Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1981, pp. 164-176.J. Ouaknine and J. Worrell, “Some recent results in Metric Temporal Logic,” in Proceedings of the 6th International Conference Formal Modeling and Analysis of Timed Systems, 2008, pp. 1-13.J. Ouaknine and J. Worrell, “Some recent results in Metric Temporal Logic,” in Proceedings of the 6th International Conference Formal Modeling and Analysis of Timed Systems, 2008, pp. 1-13.Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer, 1992.Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer, 1992.P. Wolper, “Temporal Logic Can Be More Expressive,” Information and Control, vol. 56, pp. 72-99, 1983.P. Wolper, “Temporal Logic Can Be More Expressive,” Information and Control, vol. 56, pp. 72-99, 1983.T. French, “Quantified propositional temporal logic with repeating states,” in Proceedings of the 10th International Symposium on Temporal Representation and Reasoning, 2003, pp. 155-165.T. French, “Quantified propositional temporal logic with repeating states,” in Proceedings of the 10th International Symposium on Temporal Representation and Reasoning, 2003, pp. 155-165.J. J. Henriksen and P. S. Thiagarajan, “Dynamic linear time temporal logic,” Annals of Pure and Applied Logic, vol. 96, pp. 187-207, 1999.J. J. Henriksen and P. S. Thiagarajan, “Dynamic linear time temporal logic,” Annals of Pure and Applied Logic, vol. 96, pp. 187-207, 1999.G. De Giacomo and M. Y. Vardi, “Linear temporal logic and linear dynamic logic on finite traces,” in Proceedings of the 23th International Joint Conference on Artificial Intelligence, 2013, pp. 854-860.G. De Giacomo and M. Y. Vardi, “Linear temporal logic and linear dynamic logic on finite traces,” in Proceedings of the 23th International Joint Conference on Artificial Intelligence, 2013, pp. 854-860.A. Artale, R. Konchakov, V. Ryzhikov, and M. Zakharyaschev, “Tractable interval temporal propositional and description logics,” in Proceedings of the 29th AAAI Conference on Artificial Intelligence, 2015, pp. 1417-1423.A. Artale, R. Konchakov, V. Ryzhikov, and M. Zakharyaschev, “Tractable interval temporal propositional and description logics,” in Proceedings of the 29th AAAI Conference on Artificial Intelligence, 2015, pp. 1417-1423.S. Merz, M. Wirsing, and J. Zappe, “A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems,” in Proceedings of the 6th International Conference on Fundamental Approaches to Software Engineering, 2003, pp. 87-101.S. Merz, M. Wirsing, and J. Zappe, “A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems,” in Proceedings of the 6th International Conference on Fundamental Approaches to Software Engineering, 2003, pp. 87-101.C. Baier and J. Katoen, Principles of Model Checking. MIT Press, 2008.C. Baier and J. Katoen, Principles of Model Checking. MIT Press, 2008.E. M. Clarke, O. Gramberg, and D. A. Peled, Model Checking. MIT Press, 1999.E. M. Clarke, O. Gramberg, and D. A. Peled, Model Checking. MIT Press, 1999.D. G. Kozlova and V. A. Zakharov, “On the model checking of sequential reactive systems,” in Proceedings of the 25th International Workshop on Concurrency, Specification and Programming (CS&P 2016), CEUR Workshop Proceedings, 2016, vol. 1698, pp. 376-389.D. G. Kozlova and V. A. Zakharov, “On the model checking of sequential reactive systems,” in Proceedings of the 25th International Workshop on Concurrency, Specification and Programming (CS&P 2016), CEUR Workshop Proceedings, 2016, vol. 1698, pp. 376-389.A. R. Gnatenko and V. A. Zakharov, “On the verification of finite transducers over semigroups,” Proceedings of ISP RAS, vol. 30, pp. 303-324, 2018.A. R. Gnatenko and V. A. Zakharov, “On the verification of finite transducers over semigroups,” Proceedings of ISP RAS, vol. 30, pp. 303-324, 2018.A. Gnatenko and V. Zakharov, “On the Model Checking Problem for Some Extension of CTL*,” Modeling and Analysis of Information Systems, vol. 27, pp. 428-441, 2020.A. Gnatenko and V. Zakharov, “On the Model Checking Problem for Some Extension of CTL*,” Modeling and Analysis of Information Systems, vol. 27, pp. 428-441, 2020.A. Gnatenko and V. Zakharov, “On the Expressive Power of Some Extensions of Linear Temporal Logic,” Modeling and Analysis of Information Systems, vol. 25, pp. 506-524, 2018.A. Gnatenko and V. Zakharov, “On the Expressive Power of Some Extensions of Linear Temporal Logic,” Modeling and Analysis of Information Systems, vol. 25, pp. 506-524, 2018.M. Y. Vardi and P. Wolper, “An Automata-Theoretic Approach to Automatic Program Verification,” in Proceedings of the First Symposium on Logic in Computer Science, 1986, pp. 322-331.M. Y. Vardi and P. Wolper, “An Automata-Theoretic Approach to Automatic Program Verification,” in Proceedings of the First Symposium on Logic in Computer Science, 1986, pp. 322-331.J. A. W. Kamp, Tense Logic and the Theory of Linear Order, PhD thesis. University of California, Los Angeles, 1968.J. A. W. Kamp, Tense Logic and the Theory of Linear Order, PhD thesis. University of California, Los Angeles, 1968.K. Etessami and T. Wilke, “An Until Hierarchy and Other Applications of an Ehrenfeucht-Fraisse Game for Temporal Logic,” Information and Computation, vol. 160, pp. 88-108, 2000.K. Etessami and T. Wilke, “An Until Hierarchy and Other Applications of an Ehrenfeucht-Fraisse Game for Temporal Logic,” Information and Computation, vol. 160, pp. 88-108, 2000.M. Leucker and C. Sanchez, “Regular Linear Temporal Logic,” in Proceedings of the 4-th International Colloquium on Theoretical Aspects of Computing, 2007, pp. 291-305.M. Leucker and C. Sanchez, “Regular Linear Temporal Logic,” in Proceedings of the 4-th International Colloquium on Theoretical Aspects of Computing, 2007, pp. 291-305.O. Kupferman, N. Piterman, and M. Y. Vardi, “Extended Temporal Logic Revisited,” in Proceedings of 12-th International Conference on Concurrency Theory, 2001, pp. 519-535.O. Kupferman, N. Piterman, and M. Y. Vardi, “Extended Temporal Logic Revisited,” in Proceedings of 12-th International Conference on Concurrency Theory, 2001, pp. 519-535.A. R. Gnatenko and V. A. Zakharov, “O slozhnosti verifikatsii avtomatov-preobrazovateley nad kommutativnymi polugruppami,” in Trudy 18 Mezhdunarodnoj konferentsii Problemy teoreticheskoy kibernetiki, 2017, pp. 68-70.A. R. Gnatenko and V. A. Zakharov, “O slozhnosti verifikatsii avtomatov-preobrazovateley nad kommutativnymi polugruppami,” in Trudy 18 Mezhdunarodnoj konferentsii Problemy teoreticheskoy kibernetiki, 2017, pp. 68-70.V. A. Zakharov and G. G. Temerbekova, “On the Minimization of Finite State Transducers over Semigroups,” Modeling and Analysis of Information Systems, vol. 23, pp. 741-753, 2016.V. A. Zakharov and G. G. Temerbekova, “On the Minimization of Finite State Transducers over Semigroups,” Modeling and Analysis of Information Systems, vol. 23, pp. 741-753, 2016.V. A. Zakharov, “Equivalence checking problem for finite state transducers over semigroups,” in Proceedings of the 6-th International Conference on Algebraic Informatics, 2015, pp. 208-221.V. A. Zakharov, “Equivalence checking problem for finite state transducers over semigroups,” in Proceedings of the 6-th International Conference on Algebraic Informatics, 2015, pp. 208-221.J. M. Fisher and R. E. Ladner, “Propositional Dynamic Logic of Regular Programs,” Journal of Computer and System Sciences, vol. 18, pp. 194-211, 1979.J. M. Fisher and R. E. Ladner, “Propositional Dynamic Logic of Regular Programs,” Journal of Computer and System Sciences, vol. 18, pp. 194-211, 1979.W. J. Savitch, “Relationships between nondeterministic and deterministic tape complexities,” Journal of Computer and System Science, vol. 4, pp. 177-192, 1970.W. J. Savitch, “Relationships between nondeterministic and deterministic tape complexities,” Journal of Computer and System Science, vol. 4, pp. 177-192, 1970.D. Kozen, “Lower bounds for natural proof systems,” in Proceedings of the 18th International Symposium on the Foundations of Computer Science, 1977, pp. 254-266.D. Kozen, “Lower bounds for natural proof systems,” in Proceedings of the 18th International Symposium on the Foundations of Computer Science, 1977, pp. 254-266.

The authors declare that there are no conflicts of interest present.