?
О задаче верификации моделей программ для одного расширения логики CTL*
Sequential reactive systems include programs and devices that work with two streams of data and convert input streams ofdata into output streams. Such information processing systems include controllers, device drivers, computer interpreters.e result of the operation of such computing systems are innite sequences of pairs of events of the request–responsetype, and, therefore, nite transducers are most oen used as formal models for them. e behavior of transducers isrepresented by binary relations on innite sequences, and so, traditional applied temporal logics (like HML, LTL, CTL,mu-calculus) are poorly suited as specication languages, since omega-languages, not binary relations on omega-words areused for interpretation of their formulae. To provide temporal logics with the ability to dene properties of transformationsthat characterize the behavior of reactive systems, we introduced new extensions of these logics, which have two distinctivefeatures: 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 powerof new extensions Reg-LTL and Reg-CTL of the well-known temporal logics of linear and branching time LTL and CTL, inwhich it was allowed to use only regular languages for parameterization of temporal operators and basic predicates. Wediscovered that such a parameterization increases the expressive capabilities of temporal logic, but preserves the decidabilityof the model checking problem. For the logics mentioned above, we have developed algorithms for the verication of nitetransducers. At the next stage of our research on the new extensions of temporal logic designed for the specication andverication of sequential reactive systems, we studied the verication problem for these systems using the temporal logicReg-CTL*, which is an extension of the Generalized Computational Tree Logics CTL*. In this paper we present an algorithmfor checking the satisability of Reg-CTL* formulae on models of nite state transducers and show that this problem belongsto the complexity class ExpSpace.