?
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 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.