|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
Using an extension of CT L∗ for specification and verification of sequential reactive systemsстатья
- Авторы: Gnatenko A.R., Zakharov V.A.
- Журнал: Системная информатика
- Том: 17
- Год издания: 2020
- Первая страница: 21
- Последняя страница: 32
- Аннотация: Sequential reactive systems such as controllers, device drivers, computer interpretersoperate with two data streams and transform input streams of data (control signals, instructions) into output streams of control signals (instructions, data). Finite state transducers are widely used as an adequate formal model for information processing systems ofthis kind. Since runs of transducers develop over time, temporal logics, obviously, couldbe used as both simple and expressive formalism for specifying the behavior of sequential reactive systems. However, the conventional applied temporal logics (HML, LTL,CTL, µ-calculus) do not suit this purpose well, since their formulae are interpreted overω-languages, whereas the behavior of transducers are represented by binary relations oninfinite sequences, i.e. by ω-transductions. To provide temporal logics with the ability tospecify the property of transductions that characterize the behavior of reactive systems, weintroduced new extensions of these logics. Two principal features distinguish these extension: 1) temporal operators are parameterized by sets of streams (languages) admissiblefor input, and 2) sets (languages) of expected output streams are used as basic predicates.In our previous papers we studied the expressive power and the model checkingproblem for Reg-LTL and Reg-CTL which are the extensions of LTL and CTL where thelanguages mentioned above are regular ones. We discovered that parametrization of thiskind increases expressive power of temporal logics though retains the decidability of themodel checking problem. Our next step in the systematic exploration of new extensionsof temporal logics intended for specication and verication of sequential reactive systemsis the study of the model checking problem for nite state transducers against Reg-CTL∗formulae. In this paper we develop a model checking algorithm for Reg-CTL∗ and showthat this problem is in ExpSpace.
- Добавил в систему: Захаров Владимир Анатольевич