?
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 finite state transducers that operate over semigroups. This model of computation is suitable for synthesis, optimization, verification and testing of sequential reactive systems. In this paper we originate a framework for developing verification techniques for sequential reactive systems by utilizing finite state transducers as a formal model. To this end we introduce a LTL-based formal language which may be suitable for specification of the behaviour of sequential reactive systems and adopt a well known LTL-based model checking techniques for verification of finite state transducers against these specifications.