|
ИСТИНА |
Войти в систему Регистрация |
ФНКЦ РР |
||
On the expressive power of some extensions of Linear Temporal Logicстатья
- Авторы: Gnatenko Anton, Zakharov Vladimir
- Сборник: Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018
- Год издания: 2018
- Издательство: Яросл. гос. ун-т
- Местоположение издательства: Ярославль
- Первая страница: 29
- Последняя страница: 36
- Аннотация: One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a finite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. A behaviour of such a reactive system displays itself in the correspondence between flows of control signals and compositions of basic actions performed by the system. We believe that behaviour of this kind requires more suitable and expressive means for formal specifications than conventional LTL. In this paper we define some new (as far as we know) extension LP-LTL of Linear Temporal Logic specifically intended for describing the properties of transducers computations. In this extension the temporal operators are parameterized by sets of words (languages) which â˘A ´ Nâ˘AN´ represent distinguished flows of control signals that impact on a reactive system. Basic predicates in our variant of temporal logic are also languages in the alphabet of basic actions of a transducer; they represent the expected response of a transducer to the specified environmental influences. In our earlier papers we considered model checking problem for LP-LTL and LP-CTL and showed that this problem has effective solutions. The aim of this paper is to estimate the expressive power of LP-LTL by comparing it with some well known logics widely used in computer science for specification of reactive systems behaviour. We discovered that a restricted variant LP-1-LTL of our logic is more expressive than LTL and another restricted variant LP-n-LTL has the same expressive power as monadic second order logic S1S.
- Добавил в систему: Захаров Владимир Анатольевич
Прикрепленные файлы
| № | Имя | Описание | Имя файла | Размер | Добавлен |
|---|---|---|---|---|---|
| 1. | Полный текст | article-Gnatenko-Zakharov-pssv18-3.pdf | 318,9 КБ | 24 июня 2018 [Vladimir_Zakharov] |