On the model checking of sequential reactive systems
By sequential reactive system we mean a program which operates in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data a program performs a sequence of actions (response) and displays the current result. Such programs usually arise at implementation of computer drivers, online algorithms, control procedures. Basic actions performed by these programs may be regarded as generating elements of a certain semigroup. This consideration opens the way to model sequential reactive systems by ﬁnite state transducers that operate over semigroups. This model of computation is suitable for synthesis, optimization, veriﬁcation and testing of sequential reactive systems. In this paper we originate a framework for developing veriﬁcation techniques for sequential reactive systems by utilizing ﬁnite state transducers as a formal model. To this end we introduce a LTL-based formal language which may be suitable for speciﬁcation of the behaviour of sequential reactive systems and adopt a well known LTL-based model checking techniques for veriﬁcation of ﬁnite state transducers against these speciﬁcations.