摘要 : 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 i... 展开 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 results of 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 formulas. To provide temporal logics with the ability to define properties of transformations that characterize the behavior of reactive systems, we introduced new extensions of these logics, which have two distinctive features: (1) temporal operators are parameterized, and languages in the input alphabet of transducers are used as parameters; (2) languages in the output alphabet of transducers are used as basic predicates. Previously, we studied the expressive power of new extensions Reg-LTL and Reg-CTL of the well-known temporal logics of linear 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 of temporal 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 of the generalized computational tree logics CTL*. In this paper we present an algorithm for checking the satisfiability of Reg-CTL* formulas on models of finite state transducers and show that this problem belongs to the complexity class ExpSpace. 收起