О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени

Моделирование и анализ информационных систем. 2021. Т. 28. № 4. С. 356–371.

Gnatenko A., Zakharov V.

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 𝑅𝑒𝑔-𝐿𝑇𝐿 and introduced a model checking algorithm for 𝑅𝑒𝑔-𝐿𝑇𝐿, 𝑅𝑒𝑔-𝐶𝑇𝐿, and 𝑅𝑒𝑔-𝐶𝑇𝐿∗. 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 𝑅𝑒𝑔-𝐿𝑇𝐿 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 satis€ability of checking 𝑅𝑒𝑔-𝐿𝑇𝐿 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.

Keywords: model checking, finite state transducer, конечный автомат-преобразователь, автомат Бюхи, верификация моделей программ, темпоральные логики, regular language, регулярный язык, Buchi automaton, Satisfiability problem, temporal logic

Publication based on the results of: Process models: checking conformance with the observed behavior, automated discovery and behavioral analysis (2021)