|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
Satisfiability and Model Checking for One Parameterized Extension of Linear Temporal Logicстатья
- Авторы: Gnatenko A.R., Zakharov V.A.
- Журнал: Automatic Control and Computer Sciences
- Том: 56
- Номер: 7
- Год издания: 2022
- Издательство: Allerton Press Inc.
- Местоположение издательства: United States
- Первая страница: 649
- Последняя страница: 660
- DOI: 10.3103/S0146411622070057
- Аннотация: Sequential reactive systems are computer programs or hardware devices which process theflows of input data or control signals and output the streams of instructions or responses. Whendesigning 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 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 this paper we give a complete solution to satisfiability checking and modelchecking problems for Reg-LTL and prove that both problems are Pspace-complete. The computationalhardness of the problems under consideration is easily proved by reducing to them the intersectionemptyness problem for the families of regular languages. The main result of the paper is analgorithm for reducing the satisfiability checking Reg-LTL formulas to the emptiness problem forBuchi 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.
- Добавил в систему: Захаров Владимир Анатольевич