On the Model Checking Problem for Some Extension of CTL*
Sequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output streams. Such information processing systems include controllers, device drivers, computer interpreters. The result of the operation of such computing systems are...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2020-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1434 |
| _version_ | 1797877789805772800 |
|---|---|
| author | Anton Romanovich Gnatenko Vladimir Anatolyevich Zakharov |
| author_facet | Anton Romanovich Gnatenko Vladimir Anatolyevich Zakharov |
| author_sort | Anton Romanovich Gnatenko |
| collection | DOAJ |
| description | Sequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output streams. Such information processing systems include controllers, device drivers, computer interpreters. The result of the operation of such computing systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite transducers are most often used as formal models for them. The behavior of transducers is represented by binary relations on infinite sequences, and so, traditional applied temporal logics (like HML, LTL, CTL, mu-calculus) are poorly suited as specification languages, since omega-languages, not binary relations on omega-words are used for interpretation of their formulae. To provide temporal logics with the ability to define properties of transformations that characterize the behavior ofreactive systems, we introduced new extensions ofthese logics, which have two distinctive features: 1) temporal operators are parameterized, and languages in the input alphabet oftransducers are used as parameters; 2) languages in the output alphabet oftransducers are used as basic predicates. Previously, we studied the expressive power ofnew extensions Reg-LTL and Reg-CTL ofthe well-known temporal logics oflinear and branching time LTL and CTL, in which it was allowed to use only regular languages for parameterization of temporal operators and basic predicates. We discovered that such a parameterization increases the expressive capabilities oftemporal logic, but preserves the decidability of the model checking problem. For the logics mentioned above, we have developed algorithms for the verification of finite transducers. At the next stage of our research on the new extensions of temporal logic designed for the specification and verification of sequential reactive systems, we studied the verification problem for these systems using the temporal logic Reg-CTL*, which is an extension ofthe Generalized Computational Tree Logics CTL*. In this paper we present an algorithm for checking the satisfiability of Reg-CTL* formulae on models of finite state transducers and show that this problem belongs to the complexity class ExpSpace. |
| first_indexed | 2024-04-10T02:23:54Z |
| format | Article |
| id | doaj.art-325d3b2edc7c4ccbb8546903d0b057eb |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:23:54Z |
| publishDate | 2020-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-325d3b2edc7c4ccbb8546903d0b057eb2023-03-13T08:07:35ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172020-12-0127442844110.18255/1818-1015-2020-4-428-4411090On the Model Checking Problem for Some Extension of CTL*Anton Romanovich Gnatenko0Vladimir Anatolyevich Zakharov1Национальный исследовательский университет «Высшая школа экономики»Национальный исследовательский университет «Высшая школа экономики»; Институт системного программирования имени В.П. Иванникова РАНSequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output streams. Such information processing systems include controllers, device drivers, computer interpreters. The result of the operation of such computing systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite transducers are most often used as formal models for them. The behavior of transducers is represented by binary relations on infinite sequences, and so, traditional applied temporal logics (like HML, LTL, CTL, mu-calculus) are poorly suited as specification languages, since omega-languages, not binary relations on omega-words are used for interpretation of their formulae. To provide temporal logics with the ability to define properties of transformations that characterize the behavior ofreactive systems, we introduced new extensions ofthese logics, which have two distinctive features: 1) temporal operators are parameterized, and languages in the input alphabet oftransducers are used as parameters; 2) languages in the output alphabet oftransducers are used as basic predicates. Previously, we studied the expressive power ofnew extensions Reg-LTL and Reg-CTL ofthe well-known temporal logics oflinear and branching time LTL and CTL, in which it was allowed to use only regular languages for parameterization of temporal operators and basic predicates. We discovered that such a parameterization increases the expressive capabilities oftemporal logic, but preserves the decidability of the model checking problem. For the logics mentioned above, we have developed algorithms for the verification of finite transducers. At the next stage of our research on the new extensions of temporal logic designed for the specification and verification of sequential reactive systems, we studied the verification problem for these systems using the temporal logic Reg-CTL*, which is an extension ofthe Generalized Computational Tree Logics CTL*. In this paper we present an algorithm for checking the satisfiability of Reg-CTL* formulae on models of finite state transducers and show that this problem belongs to the complexity class ExpSpace.https://www.mais-journal.ru/jour/article/view/1434реагирующая системаверификация моделей программконечный автомат-преобразовательтемпоральная логикарегулярный языкспецификация |
| spellingShingle | Anton Romanovich Gnatenko Vladimir Anatolyevich Zakharov On the Model Checking Problem for Some Extension of CTL* Моделирование и анализ информационных систем реагирующая система верификация моделей программ конечный автомат-преобразователь темпоральная логика регулярный язык спецификация |
| title | On the Model Checking Problem for Some Extension of CTL* |
| title_full | On the Model Checking Problem for Some Extension of CTL* |
| title_fullStr | On the Model Checking Problem for Some Extension of CTL* |
| title_full_unstemmed | On the Model Checking Problem for Some Extension of CTL* |
| title_short | On the Model Checking Problem for Some Extension of CTL* |
| title_sort | on the model checking problem for some extension of ctl |
| topic | реагирующая система верификация моделей программ конечный автомат-преобразователь темпоральная логика регулярный язык спецификация |
| url | https://www.mais-journal.ru/jour/article/view/1434 |
| work_keys_str_mv | AT antonromanovichgnatenko onthemodelcheckingproblemforsomeextensionofctl AT vladimiranatolyevichzakharov onthemodelcheckingproblemforsomeextensionofctl |