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...
Saved in:
| 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 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849241022571216896 |
|---|---|
| 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. |
| format | Article |
| id | doaj-art-325d3b2edc7c4ccbb8546903d0b057eb |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2020-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-325d3b2edc7c4ccbb8546903d0b057eb2025-08-20T04:00:19ZengYaroslavl 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 Zakharov1Research University Higher School of EconomicsResearch University Higher School of Economics; Ivannikov Institute for System Programming of the RASSequential 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/1434reactive systemmodel checkingfinite state transducertemporal logicregular languagespecification |
| spellingShingle | Anton Romanovich Gnatenko Vladimir Anatolyevich Zakharov On the Model Checking Problem for Some Extension of CTL* Моделирование и анализ информационных систем reactive system model checking finite state transducer temporal logic regular language specification |
| 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 | reactive system model checking finite state transducer temporal logic regular language specification |
| url | https://www.mais-journal.ru/jour/article/view/1434 |
| work_keys_str_mv | AT antonromanovichgnatenko onthemodelcheckingproblemforsomeextensionofctl AT vladimiranatolyevichzakharov onthemodelcheckingproblemforsomeextensionofctl |