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.
Finite state transducers extend the nite state automata to model functions and
relations on strings or lists. They are used in many elds as diverse as
computational linguistics [
An ordinary model of nite state transducers over words can be further extended to encompass a more wide class of sequential reactive programs. These programs operate in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data such program performs a sequence of actions. When certain control points are achieved a program outputs the current results of computation as a response. What matters is that di erent sequences of actions may yield the same result. Therefore, the basic actions of a program may be viewed as generating elements of some appropriate semigroup, and the result of computation may be regarded as the composition of actions performed by the program.
Let us consider some examples. Imagine that a radio-controlled robot moves
on the earth surface. It can make one step moves in any of 4 directions N; E; S; W .
When such robot receives a control signal syg in a state q it must choose and
carry out a sequence of steps (say, N; N; W; S), and enter to the next state q0.
At some distinguished state qfin robot reports its current location. Movements
of the robot may be regarded as basic actions, and the most simple model of
computation which is suitable for analyzing a behaviour of this robot is
nondeterministic nite state transducer operating on free Abelian group of rank 2.
Next, consider a network switch which receives as input packet ows
alternating with control instructions. Following to its ow table a switch sends modi ed
copies of every packet into one or another output port. A ow table is updated at
receiving a control instruction. Modi cations and forwardings of a data packet
may be regarded as basic actions. When a switch forwards two packets from
di erent packet ows to di erent ports, the corresponding actions can be
performed in an arbitrary order. Therefore, such a switch can be modeled by a nite
state transducer operating on a partially commutative semigroup. Semigroups
of this kind are also known as traces; they are thoroughly studied in [
When designing sequential reactive systems software engineers want to be
con dent of their correct behaviour. For example, in the case of radio-controlled
robot it may be required that it never appears in the north-west sector of the
surface, obligatory passes via certain locations, and can be always returned to
the starting point at receiving a particular sequences of control messages. When
a network switch is concerned, its computations should comply with the
requirements of forwarding policies (see, e.g. [
Equivalence checking problem for nite state transducers has been studied in
much details in many papers. Its study for classical transducers that operate on
words began in the early 60s. First, it was shown that the equivalence checking
problem is undecidable for non-deterministic transducers [
There are also papers where equivalence checking problem for transducers
is studied in the framework of program veri cation. The authors of [
Unlike equivalence checking, model checking of (or related with)
transducers is less well studied. Transducers found a usage in regular model checking
of parameterized distributed systems. In some formal models of these systems
con gurations are modeled as words over nite alphabet. In such a situation a
transition relation on these con gurations is a binary relation on nite words
which can be adequately speci ed by nite state transducers (see [
However, these arguments become invalid when a response of a reactive system at every step of its computation is regarded as a composition of actions produced by the system so far. In this case the predicates which specify the basic properties of reactive systems behaviour are de ned on nite sequences of actions, i.e. every such predicate is a language over an alphabet of output actions. More complex dynamic properties can be expressed by LTL formulae. It should be remarked that these formulae must express not only the properties of output sequences of actions but relationships between input sequences of requests from the environment (signal ows) and output sequences of responding actions (compound actions). This can be achieved through the introduction of behaviour patterns of the environment as the sets of signal ows and the using of these patterns as parameters of temporal operators.
In this paper we make an attempt to introduce a LTL-based formal language
for speci cation of the behaviour of sequential reactive systems and to adapt
a well known LTL-based model checking techniques [
Let C and A be two nite sets. The elements of C are called signals ; they may be viewed as abstractions of messages (control instructions, instrument or sensor readings, pieces of data, etc.) received by a reactive system from its environment. Finite sequences of signals (words over alphabet C) are called signal ows. As usual, the set of all signal ows is denoted by C . We write uv for concatenation of signal ows u and v, and " for the empty signal ow.
The elements of A are called basic actions ; they are the abstractions of operations (data processings, movements, etc.) performed by a reactive system in response to received signals. Finite sequences of basic actions (words over alphabet A) are called compound actions.
Actions are interpreted over semigroups. Consider a semigroup (S; e; ) generated by the set A, where S is a set of semigroup elements, e is the neutral element, and is a composition operation. The elements of S may be regarded as data states. Every basic action a; a 2 A, when been applied to a data state s; s 2 S, yields the result s a. Every compound action h = a1a2 : : : ak is interpreted as the composition [h] = a1 a2 ak.
A trajectory on a semigroup (S; e; ) is a pair tr = (s0; ) such that s0 2 S and is an in nite sequence
= (c1; s1); (c2; s2); : : : ; (ci; si); : : : ; where ci 2 C; si 2 S for every i; i 0. This sequence represents a possible behaviour of a reactive system as it becomes visible to an outside observer: every time at receiving a next signal ci the system performs some compound action hi and displays its e ect si = si 1 hi. Given a trajectory tr = (s0; ) and an integer i; i 0, we denote by trji the trajectory (si; ji), where ji = (ci+1; si+1); (ci+2; si+2); : : :
A nite state transducer over a set of signals C and a set of basic actions A is a system = (C; A; Q; Q0; T ), where Q is a nite set of control states, Q0; Q0 Q; is a set of initial states, and T; T Q C Q A , is a transition relation. Every quadruple (q; c; q0; h) in T is called a transition: when a transducer is in a control state q and receives a signal c it passes its control to a state q0 and performs a compound action h. Such transitions are usually depicted as q c!;h q0. It is assumed that T is a total relation: for every control state q and a signal c the set T includes at least one transition of the kind q c!;h q0. A run of sequence of transitions
run = q0 c1!;h1 q1 c2!;h2 q2 c3!;h3 which begins from some initial state q0. We write runji for the su x of the sequence run which begins from the state qi; i 0. The size j j of a transducer is the number jQj of its state.
A nite state transducer can serve as a formal model of a sequential reactive system. At each step of its computation it receives a signal c from the environment and performs a transition q c!;h q0 by passing its control to a state q0 and executing an action h. Usually behaviour of transducers is de ned as transduction relation between input and output words. But it can be rather well de ned in terms of trajectories as follows. Suppose that basic actions of a transducer = (C; A; Q; Q0; T ) are interpreted over a semigroup (S; e; ). Then every run (1) of generates a trajectory tr(run) = (e; ), where the sequence = (c1; s1); (c2; s2); : : : ; (ci; si); : : : ; is such that s1 = e h1, and si = si 1 hi holds for every i; i 2. The set of all trajectories generated by the runs of is denoted by T r( ; S). This set completely characterizes a behaviour of sequential reactive system modeled by a transducer over a semigroup of actions (S; e; ). is any (1) 3
Speci cation languages are intended to describe formally desirable (or erroneous) behaviours of computing systems. Since the behaviour of a sequential reactive system is presented as a set of trajectories, the expressions of an appropriate speci cation language should be interpreted over trajectories. Every trajectory displays how the data states from the set S changes as a reactive system receives signals and performs responding actions with the passage of time. Therefore, it is advantageous to take some variant of temporal logics as a framework of such a speci cation language.
The formulae of temporal logics are built of basic predicates by means of Boolean connectives and temporal operators. Basic predicates are de ned on data states. In our model of sequential reactive systems data states are interpreted as elements of a semigroup (S; e; ). Thus, basic predicates can be regarded as certain subsets of S. They can be formally introduced alternatively in di erent ways. 1. By means of parameterized algebraic equations in a semigroup: a data state s satis es a basic predicate Eq(p; X) i s is such a value of a parameter p that an equation Eq(p; X) has a solution in a semigroup (S; e; ). For example, an equation p X = e speci es a set of data states s from which a computation of a reactive system can be restarted. 2. By any means | formal grammars, language equations, automata of various types, etc. | for de ning formal languages over a set of basic actions A. A data state s satis es a predicate L, where L is a language over A, i s = [h] for some compound action h such that h 2 L. For example, a nite state automaton A distinguishes a set of data states s such that s = [h] for some compound action h accepted by A.
A sequential reactive system modi es data states in response to incoming signals. These signals come to an input of a system in conformity with a certain scenario (pattern) of environment's behaviour. An environment behaviour pattern characterizes a set of possible signal ows that may a ect a reactive system. Therefore, a speci cation of its behaviour must include some references to signal ows. This can be achieved by using formal descriptions of environment behaviour patterns as parameters of temporal operators. Since a signal ow is but a word over a set of signals C, such descriptions can be provided by any means used for de ning formal languages | grammars, equations, automata.
These contemplations bring us to the following concept of formal speci cation language LP-LT L for sequential reactive systems. Given a set of signals C, a set of basic actions A, and a semigroup (S; e; ) generated by basic actions, we say that any set of nite words (language) over the alphabet C is an environment behaviour pattern (or, simply, a pattern), and any subset S0; S0 S; of data states is a basic predicate.
Select a family of patterns L and a family P of basic predicates. Then a set of LP-LT L formulae is the minimal set F orm of expressions which satisfy the following rules: 1) every basic predicate P; P 2 P, is a LP-LT L formula; 2) if '; are LP-LT L formulae then :', ' ^ and ' _ 3) if ' 2 F orm and c 2 C then Xc', Yc' belong to F orm; 4) if ' 2 F orm and L 2 L then FL', GL' belong to F orm as well. belong to F orm; This de nition is constructive, since L and P may be thought of as the set of names interpreted over patterns and basic predicates. The size j'j of a formula ' is the number of Boolean connectives and temporal operators occurred in '.
The semantics of the speci cation language is de ned in terms of satis ability relation j= of LP-LT L formulae on trajectories. Let tr = (s0; ) be a trajectory, where = (c1; s1); (c2; s2); : : : ; (ci; si); : : : ; and ' be a LP-LT L formula. Then 1) if P 2 P then tr j= P () s0 2 P ; 2) tr j= :' () it is not true that tr j= '; 3) tr j= ' ^ () tr j= ' and tr j= ; 4) tr j= ' _ () tr j= ' or tr j= ; 5) tr j= Xc' () c = c1 and trj1 j= '; 6) tr j= Yc' () c 6= c1 or trj1 j= '; 7) tr j= FL' () 9 i 0 : c1c2 : : : ci 2 L and trji j= '; 8) tr j= GL' () 8 i 0 : c1c2 : : : ci 2 L implies trji j= '.
Clearly, some other parameterized temporal operators that are used in LTL like U (until), W (weak until), R (release) can be introduced in the same way. Moreover, some new temporal operators that are speci c for LP-LT L may be introduced. For example, to express some properties of trajectories one may need a weak eventuality operator FbL which has the following semantics: tr j= FbL' () either 8 i 0 : c1c2 : : : ci 2= L; or tr j= FL'.
It is easy to make sure that parameterized temporal operators introduced above satisfy duality and xed-point (expansion) properties.
Proposition 1. Let ' be an arbitrary LP-LT L formula, c 2 C, L be an arbitrary trajectory. Then C , and tr 1) tr j= :Xc' () tr j= Yc:', 2) tr j= :Yc' () tr j= Xc:', 3) tr j= :FL' () tr j= GL:', 4) tr j= :GL' () tr j= FL:'.
For every pattern L and a signal c denote by P ref1(L) the set fc : 9w 2 C : cw 2 Lg of 1-letter pre xes of signal ows in L, and by Suf fc(L) the pattern fw : cw 2 Lg which consists of maximal proper su xes of those signal ows in L that begin with the signal c. We say that a family of patterns L is su x-closed i for every signal c and every pattern L; L 2 C; the pattern Suf fc(L) also belongs to L.
Proposition 2. Suppose that a family of patterns L is su x-closed, and let ' be a LP-LT L formula, and tr be a trajectory. Then 1) if " 2 L then tr j= FL' () tr j= ' _ W c2P ref1(L) 2) if " 2= L then tr j= FL' () tr j= W XcFSuffc(L)',
c2P ref1(L) 3) if " 2 L then tr j= GL' () tr j= ' ^ V c2P ref1(L) 4) if " 2= L then tr j= GL' () tr j= V YcFSuffc(L)'.
c2P ref1(L)
As in the case of ordinary LTL these properties are important for building model checking and satis ability checking procedures for LP-LT L formulae. 4
LP -LT L speci cations Assume that sequential reactive systems are modeled by nite state transducers that operate over a set of signals C and the set of basic actions A interpreted in a semigroup (S; e; ). Let L and P be families of admissible patterns and basic predicates. Then model checking (MC) problem for sequential reactive systems against LP-LT L speci cations is that of checking, given a nite state transducer and a LP-LT L formula ', whether tr j= ' holds for every trajectory tr in T r( ; S) (or, in symbols, T r( ; S) j= ').
It is evident that decidability and complexity of MC problem for sequential reactive systems against LP-LT L speci cations essentially depend on 1) a semigroup (S; e; ) used for interpretation of basic actions, 2) a family of basic predicates P on the set of data states S, and 3) a family of behaviour patterns of the environment L used for parametrization of temporal operators. In some cases this problem has an e ective solution.
Here we consider the most simple case of MC problem when 1) basic actions are interpreted over free monoid (S; e; ), where S is the set of compound actions A , e = ", and is concatenation operation on compound actions, 2) a family P of basic predicates is the collection of all regular sets of compound actions, 3) a family L of behaviour patterns of the environment is the collection of all regular sets of signal ows. LP-LT L formulae of this type will be called RegLT L formulae. The main advantage of Reg-LT L is that the most simple model of computation | deterministic nite state automata | can be involved to de ne basic predicates and patterns occurred in these formulae.
By (non-initialized) deterministic nite state automaton we mean a quadruple K = ( ; Z; Zacc; ), where is a nite input alphabet, Z is a nite set of states, Zacc; Zacc Z; is a subset of accepting states, and : Z ! Z is a total transition function. A transition function can be extended to the set in the usual fashion: (z; ") = z, and (z; bw) = ( (z; b); w) for every state z, a letter b in and a word w; w 2 . By initialized automaton we mean a pair (K; z0), where z0 is a state of an automaton K. An initialized automaton (K; z0) accepts a word w if (z0; w) 2 Zacc; thus, it speci es a regular language L(K; z0) = fw : (z0; w) 2 Zaccg of all accepted words.
When nite state automata are used for speci cation of regular basic predicates they have the set of basic actions A as an input language; automata of this kind will be called A-automata. When nite state automata are employed for speci cation of regular patterns of the environment they have the set of signals C as an input alphabet; automata of this sort will be called C-automata. Thus, every atomic formula of Reg-LT L is an initialized A-automaton (A; z0), and temporal operators used in Reg-LT L are those of the form Xc; Yc; F(B;z0); G(B;z0), where c is a signal, and (B; z0) is an initialized C-automaton. In what follows we will use letters Z, Zacc and as generic names of a set states, a subset of accepting states and a transition functions in automata that specify basic predicates and patterns of the environment.
The rules of Reg-LT L semantics can be rede ned in terms of nite state automata. Suppose, for example, that a run of a transducer begins with a transition q c!;h q0. Then tr(run) j= Xc(A; z0) () h 2 (A; z0) () (z0; h) 2 Zacc. This e ect also manifests itself for other formulae. Given a A-automaton (A; z0) and a compound action h, we say that the A-automaton (A; (z0; h)) is h-shift of basic predicate (A; z0). In more general case, a h-shift of a Reg-LT L formula ' is a formula shif t('; h) which is obtained from ' by replacing every basic predicate (A; z0) occurred in ' with its h-shift (A; (z0; h)). Consider a run (1) of a transducer . Then tr(run) j= F(B;z0)' tr(run) j= G(B;z0)' () 9 i 0 : (z0; c1c2 : : : ci) 2 Zacc and
tr(runji) j= shif t('; h1h2 : : : hi); () 8 i 0 : (z0; c1c2 : : : ci) 2 Zacc implies
tr(runji) j= shif t('; h1h2 : : : hi); These relationships are crucial in the designing of Reg-LT L model checking algorithm in Theorem 1.
For the sake of brevity we will skip references to a semigroup (S; e; ) in our notation till the end of the section. It is assumed that this semigroup is a free monoid of nite words over A and MC problem T r( ) j= ' is studied for nite state transducers against Reg-LT L speci cations.
The main result of this section is Theorem 1. Let = (C; A; Q; Q0; T ) be a nite state transducer operating on a free monoid of words, and ' be a Reg-LT L formula. Suppose that every regular component (a basic predicate or a pattern of the environment) of ' is speci ed by a deterministic nite state automata which has N states at the most. Then there exists a generalized Buchi automaton M [ ; '] such that { M [ ; '] has j j2O(j'jNj'j) states at the most; { M [ ; '] can be constructed e ectively by and ' in time polynomial of its size; { M [ ; '] accepts empty !-language i T r( ) j= '.
Proof. (Sketch) Our algorithm for the translation of a pair ( ; ') to a Buchi
automaton M [ ; '] follows the well-known scheme for translation of LTL
formulae to Buchi automata which was introduced in [
2 cl( ), (A; z0) 2 cl( ) ) 8 z 2 Z : (A; z) 2 cl( ) f _ g 2 cl( ) ) f; g 2 cl( ), f ^ g 2 cl( ) ) f; g 2 cl( ), Xcf 2 cl( ) ) shif t(f; h) 2 cl( ) for every h 2 A , Ycf 2 cl( ) ) shif t(f; h) 2 cl( ) for every h 2 A , F(B;z0)f 2 cl( ) ) f 2 cl( ) and 8 c 2 C : XcF(B; (z0;c))f 2 cl( ), G(B;z0)f 2 cl( ) ) f 2 cl( ) and 8 c 2 C : YcG(B; (z0;c))f 2 cl( ). As it can be seen from the de nition of cl( ) this set may contain O(j'jN j'j) at the most. 3. Build the collection CS( ) of all subsets of cl( ) which are both locally consistent and saturated. A subset K of cl( ) is called locally consistent if it satis es the following requirements: { if (A; z0) 2 K then z0 2 Zacc; { if Xc1 f 2 K and Xc2 f 2 K then c1 = c2, and it is called saturated if it ful lls the rules listed below: { if f _ g 2 K then f 2 K or g 2 K; { if f ^ g 2 K then f 2 K and g 2 K; { if F(B;z0)f 2 K then either XcF(B; (z0;c)) 2 K for some signal c, or f 2 K in the case of z0 2 Facc; { if G(B;z0)f 2 K then YcG(B; (z0;c)) 2 K for every signal c, and, moreover, f is also in K in the case of z0 2 Facc. 4. Build a generalized Buchi automaton M [ ; '] = (Q the input alphabet C A , where CS( ); Init; ; F) over Q CS( ) is the set of states of the automaton, Init = f(q0; K) : q0 2 Q0; 2 Kg is the set of initial states, = 3 is a transition relation which is de ned as follows: 1 [ 2 [ (q; K) c!;h (q0; K0) 2 1 i 1) q c!;h q0 2 T , 2) a set K contains at least one formulae Xc', and 3) fshif t('; h) : Xc' 2 K or Yc' 2 Kg K0; (q; K) c!;h (q0; K0) 2 2 i 1) q c!;h q0 2 T , 2) a set K does not contain any X-formulae, and 3) fshif t('; h) : Yc' 2 Kg K0; (q; K) c!;h (q0; K) 2 3 i 1) q c!;h q0 2 T , and 2) a set K does not contain neither X-formulae, nor Y -formulae.
F = fF' : ' is a F -formula in cl( )g is a family of acceptance conditions, where for every ' = F(B;z)f the acceptance condition F' is a set of all such pairs (q; K) that satisfy a requirement:
F(B;z0)shif t(f; h) 2 K ) shif t(f; h) 2 K.
5. Following the same line of reasoning as in [
Since emptiness of generalized Buchi automata can be checked in polynomial time we arrived at Corollary 1. Regular models checking of sequential reactive systems can be performed e ectively in time polynomial of the size of a model ( nite state transducer) and double exponential of the size of a speci cation (Reg-LT L formula).
The main contribution of this paper is twofold: 1. we introduce a new framework for formal veri cation of sequential reactive systems; it includes a concept of nite state transducer over semigroups as a formal model of sequential reactive systems, and a formal language for specifying behaviour of transducers. 2. we set up a model checking problem for nite state transducers operating over semigroups and show that conventional model checking techniques is applicable to this problem (at least in the case of transducers over free monoids).
There are questions and problems that still remain open for further research.
What is an expressive power of LP-LT L? We surmise that some LP-LT
Lspeci c operators could be introduced to make this language more convenient
in practice. We believe also that other temporal logics (say, CTL) could be also
adapted appropriately for speci cation of sequential reactive systems behaviour.
Model checking algorithm presented in Theorem 1 needs further improvement.
To this end complexity issues of LP-LT L need to be studied. We are sure that
a more advanced on-the- y approach used in LTL model checking [