On the Expressive Power of Some Extensions of Linear Temporal Logic
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. The behaviour of such a reactive system displays itself in th...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2018-10-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/746 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849241023036784640 |
|---|---|
| author | Anton Gnatenko Vladimir Zakharov |
| author_facet | Anton Gnatenko Vladimir Zakharov |
| author_sort | Anton Gnatenko |
| collection | DOAJ |
| description | 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. The 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 the behaviour of this kind requires more suitable and expressive means for formal specifications than the conventional LT L. In this paper, we define some new (as far as we know) extension LP-LT L 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 represent distinguished flows of control signals that impact on a reactive system. Basic predicates in our variant of the temporal logic are also languages in the alphabet of basic actions of a transducer; they represent the expected response of the transducer to the specified environmental influences. In our earlier papers, we considered a model checking problem for LP-LT L and LP-CT L and showed that this problem has effective solutions. The aim of this paper is to estimate the expressive power of LP-LT L by comparing it with some well known logics widely used in the computer science for specification of reactive systems behaviour. We discovered that a restricted variant LP-1-LT L of our logic is more expressive than LTL and another restricted variant LP-n-LT L has the same expressive power as monadic second order logic S1S. |
| format | Article |
| id | doaj-art-33d1820a3abb4cdcb4a44ded22f3ad7e |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2018-10-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-33d1820a3abb4cdcb4a44ded22f3ad7e2025-08-20T04:00:19ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172018-10-0125550652410.18255/1818-1015-2018-5-506-524522On the Expressive Power of Some Extensions of Linear Temporal LogicAnton Gnatenko0Vladimir Zakharov1Lomonosov Moscow State University.National Research University Higher School of Economics (HSE).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. The 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 the behaviour of this kind requires more suitable and expressive means for formal specifications than the conventional LT L. In this paper, we define some new (as far as we know) extension LP-LT L 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 represent distinguished flows of control signals that impact on a reactive system. Basic predicates in our variant of the temporal logic are also languages in the alphabet of basic actions of a transducer; they represent the expected response of the transducer to the specified environmental influences. In our earlier papers, we considered a model checking problem for LP-LT L and LP-CT L and showed that this problem has effective solutions. The aim of this paper is to estimate the expressive power of LP-LT L by comparing it with some well known logics widely used in the computer science for specification of reactive systems behaviour. We discovered that a restricted variant LP-1-LT L of our logic is more expressive than LTL and another restricted variant LP-n-LT L has the same expressive power as monadic second order logic S1S.https://www.mais-journal.ru/jour/article/view/746temporal logicsexpressive powerspecificationverificationbuchi automatainfinite words |
| spellingShingle | Anton Gnatenko Vladimir Zakharov On the Expressive Power of Some Extensions of Linear Temporal Logic Моделирование и анализ информационных систем temporal logics expressive power specification verification buchi automata infinite words |
| title | On the Expressive Power of Some Extensions of Linear Temporal Logic |
| title_full | On the Expressive Power of Some Extensions of Linear Temporal Logic |
| title_fullStr | On the Expressive Power of Some Extensions of Linear Temporal Logic |
| title_full_unstemmed | On the Expressive Power of Some Extensions of Linear Temporal Logic |
| title_short | On the Expressive Power of Some Extensions of Linear Temporal Logic |
| title_sort | on the expressive power of some extensions of linear temporal logic |
| topic | temporal logics expressive power specification verification buchi automata infinite words |
| url | https://www.mais-journal.ru/jour/article/view/746 |
| work_keys_str_mv | AT antongnatenko ontheexpressivepowerofsomeextensionsoflineartemporallogic AT vladimirzakharov ontheexpressivepowerofsomeextensionsoflineartemporallogic |