=Paper=
{{Paper
|id=Vol-1698/CS&P2016_22_Kozlova&Zakharov_On-the-model-checking-of-sequential-reactive-systems
|storemode=property
|title=On the Model Checking of Sequential Reactive Systems
|pdfUrl=https://ceur-ws.org/Vol-1698/CS&P2016_22_Kozlova&Zakharov_On-the-model-checking-of-sequential-reactive-systems.pdf
|volume=Vol-1698
|authors=Darya Kozlova,Vladimir Zakharov
|dblpUrl=https://dblp.org/rec/conf/csp/KozlovaZ16
}}
==On the Model Checking of Sequential Reactive Systems==
https://ceur-ws.org/Vol-1698/CS&P2016_22_Kozlova&Zakharov_On-the-model-checking-of-sequential-reactive-systems.pdf
On the model checking
of sequential reactive systems
D.G. Kozlova1 V.A. Zakharov2
1
Faculty of Computational Mathematics and Cybernetics,
Lomonosov Moscow State University, Moscow, RU-119899, Russia,
2
Faculty of Computer Science,
National Research University Higher School of Economics,
Moscow, Russia
(Corresponding author: zakh@cs.msu.su)
Abstract. By sequential reactive system we mean a program which op-
erates in the interaction with the environment permanently receiving
data (requests) from it. At receiving a piece of data a program per-
forms a sequence of actions (response) and displays the current result.
Such programs usually arise at implementation of computer drivers, on-
line algorithms, control procedures. Basic actions performed by these
programs may be regarded as generating elements of a certain semi-
group. 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.
1 Introduction
Finite state transducers extend the finite state automata to model functions and
relations on strings or lists. They are used in many fields as diverse as com-
putational linguistics [14] and model-based testing [1, 22]. In software engineer-
ing transducers provide a suitable formal model for various on-line algorithms
and device drivers for manipulating with strings, transforming images, filtering
dataflows, inserting fingerprints, sorting data, etc.
An ordinary model of finite 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 different
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 q 0 .
At some distinguished state qf in 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 non-
deterministic finite state transducer operating on free Abelian group of rank 2.
Next, consider a network switch which receives as input packet flows alternat-
ing with control instructions. Following to its flow table a switch sends modified
copies of every packet into one or another output port. A flow table is updated at
receiving a control instruction. Modifications and forwardings of a data packet
may be regarded as basic actions. When a switch forwards two packets from
different packet flows to different ports, the corresponding actions can be per-
formed in an arbitrary order. Therefore, such a switch can be modeled by a finite
state transducer operating on a partially commutative semigroup. Semigroups
of this kind are also known as traces; they are thoroughly studied in [9].
When designing sequential reactive systems software engineers want to be
confident 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 require-
ments of forwarding policies (see, e.g. [6, 7]) such as the absence of forwarding
loops, non-interference of certain packet flows, etc. To analyze the behaviour of
sequential reactive systems one may use the concept of finite state transducer
over finitely generated semigroups as a formal model of such systems and develop
various verification techniques (equivalence checking, model checking, deductive
verification, etc.) for these class of transducers.
Equivalence checking problem for finite 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 [11] even over 1-letter
input alphabet [12]. But the undecidability displays itself only in the case of un-
bounded transduction when an input word may have arbitrary many images. At
the next stage bound-valued transducers were studied. The equivalence checking
problem was shown also to be decidable for deterministic [4], functional (single-
valued) [3, 18], and k-valued transducers [8, 23]. In a series of papers [16, 17, 19]
techniques for checking bounded valuedness, k-valuedness and equivalence of fi-
nite state transducers over words were developed. Recently in [25] equivalence
checking problem was shown to be decidable for finite state transducers that
operate over finitely generated semigroups embeddable in decidable groups.
There are also papers where equivalence checking problem for transducers
is studied in the framework of program verification. The authors of [20] pro-
posed models of communication protocols as finite state transducers operating
on bit strings. They set up the verification problem as equivalence checking be-
tween the protocol transducer and the specification transducer. The authors of
[22] extend finite state transducers with symbolic alphabets which are repre-
sented as parametric theories. They showed that a number of classical problems
for extended transducers, including equivalence checking problem, are decidable
modulo underlying theories. In [1] a model of streaming transducers was pro-
posed for programs that access and modify sequences of data items in a single
pass. It was shown that a number of verification problems such as equivalence
checking, assertion checking, and checking correctness with respect to pre/post
conditions, are decidable for this transducer model.
Unlike equivalence checking, model checking of (or related with) transduc-
ers is less well studied. Transducers found a usage in regular model checking
of parameterized distributed systems. In some formal models of these systems
configurations are modeled as words over finite alphabet. In such a situation a
transition relation on these configurations is a binary relation on finite words
which can be adequately specified by finite state transducers (see [5, 24]). In this
line of research transducers play the role of verification instrument, but not an
object of verification. As for verification of transducers, to the extend of our
knowledge no special purpose study of model checking problem for finite state
transducers has been conducted so far. In our opinion, this is due the following
reason. Usually, both the influence of the environment upon a reactive system
and its response is defined in terms of a set of basic predicates. The letters of
input and output alphabets of a transducer are regarded as valuations (tuples
of truth values) of these predicates, and transducers are viewed as special pre-
sentation of finite labeled transition system (Kripke structure) (see [2]). From
this viewpoint model checking problem for finite state transducers conforms well
to standard model checking scheme for finite structures, and, therefore, are not
worthy of any particular treatment.
However, these arguments become invalid when a response of a reactive sys-
tem 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 defined on finite 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 re-
quests from the environment (signal flows) 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 flows 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 specification of the behaviour of sequential reactive systems and to adapt
a well known LTL-based model checking techniques [13, 21] for verification of
finite state transducers. The paper is organized as follows. In the next section
a concept of finite state transducer over semigroup (see [25]) as a formal model
of sequential reactive systems is defined. In Section 3 we introduce LP-LT L —
a parameterized version of Linear Temporal Logics — as a formal language for
specifying behaviour of sequential reactive systems. In this section we also set
up model checking problem for finite state transducers. In Section 4 we present
a LP-LT L model checking algorithm for the case when both basic properties of
reactive systems and behaviour patterns of the environment are defined by finite
state automata. Finally, we outline some possible directions for further research.
2 Transducers as models of reactive systems
Let C and A be two finite 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 flows. As
usual, the set of all signal flows is denoted by C ∗ . We write uv for concatenation
of signal flows u and v, and ε for the empty signal flow.
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, ◦) gen-
erated 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 ∈ A, when been applied to a data state
s, s ∈ S, yields the result s ◦ a. Every compound action h = a1 a2 . . . ak is inter-
preted as the composition [h] = a1 ◦ a2 ◦ · · · ◦ ak .
A trajectory on a semigroup (S, e, ◦) is a pair tr = (s0 , α) such that s0 ∈ S
and α is an infinite sequence
α = (c1 , s1 ), (c2 , s2 ), . . . , (ci , si ), . . . ,
where ci ∈ C, si ∈ 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 effect si = si−1 ◦ hi . Given a trajectory tr = (s0 , α)
and an integer i, i ≥ 0, we denote by tr|i the trajectory (si , α|i ), where α|i =
(ci+1 , si+1 ), (ci+2 , si+2 ), . . .
A finite 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 finite 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, q 0 , 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 q 0 and
c,h
performs a compound action h. Such transitions are usually depicted as q −→ q 0 .
It is assumed that T is a total relation: for every control state q and a signal c
c,h
the set T includes at least one transition of the kind q −→ q 0 . A run of π is any
sequence of transitions
c1 ,h1 c2 ,h2 c3 ,h3
run = q0 −→ q1 −→ q2 −→ · · · (1)
which begins from some initial state q0 . We write run|i for the suffix of the
sequence run which begins from the state qi , i ≥ 0. The size |π| of a transducer
π is the number |Q| of its state.
A finite 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 envi-
c,h
ronment and performs a transition q −→ q 0 by passing its control to a state
0
q and executing an action h. Usually behaviour of transducers is defined as
transduction relation between input and output words. But it can be rather
well defined 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, ◦).
3 Specification language
Specification 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
specification 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 specification language.
The formulae of temporal logics are built of basic predicates by means of
Boolean connectives and temporal operators. Basic predicates are defined on
data states. In our model of sequential reactive systems data states are inter-
preted as elements of a semigroup (S, e, ◦). Thus, basic predicates can be re-
garded as certain subsets of S. They can be formally introduced alternatively in
different ways.
1. By means of parameterized algebraic equations in a semigroup: a data state s
satisfies a basic predicate Eq(p, X) iff 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 specifies 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 defining formal languages over a set of basic actions A. A
data state s satisfies a predicate L, where L is a language over A, iff s = [h]
for some compound action h such that h ∈ L. For example, a finite 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 modifies data states in response to incoming
signals. These signals come to an input of a system in conformity with a cer-
tain scenario (pattern) of environment’s behaviour. An environment behaviour
pattern characterizes a set of possible signal flows that may affect a reactive
system. Therefore, a specification of its behaviour must include some references
to signal flows. This can be achieved by using formal descriptions of environment
behaviour patterns as parameters of temporal operators. Since a signal flow is
but a word over a set of signals C, such descriptions can be provided by any
means used for defining formal languages — grammars, equations, automata.
These contemplations bring us to the following concept of formal specification
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 finite words (language) over the alphabet C is an environment
behaviour pattern (or, simply, a pattern), and any subset S 0 , S 0 ⊆ 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 ∈ P, is a LP-LT L formula;
2) if ϕ, ψ are LP-LT L formulae then ¬ϕ, ϕ ∧ ψ and ϕ ∨ ψ belong to F orm;
3) if ϕ ∈ F orm and c ∈ C then Xc ϕ, Yc ϕ belong to F orm;
4) if ϕ ∈ F orm and L ∈ L then FL ϕ, GL ϕ belong to F orm as well.
This definition is constructive, since L and P may be thought of as the set of
names interpreted over patterns and basic predicates. The size |ϕ| of a formula
ϕ is the number of Boolean connectives and temporal operators occurred in ϕ.
The semantics of the specification language is defined in terms of satisfiability
relation |= 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 ∈ P then tr |= P ⇐⇒ s0 ∈ P ;
2) tr |= ¬ϕ ⇐⇒ it is not true that tr |= ϕ;
3) tr |= ϕ ∧ ψ ⇐⇒ tr |= ϕ and tr |= ψ;
4) tr |= ϕ ∨ ψ ⇐⇒ tr |= ϕ or tr |= ψ;
5) tr |= Xc ϕ ⇐⇒ c = c1 and tr|1 |= ϕ;
6) tr |= Yc ϕ ⇐⇒ c 6= c1 or tr|1 |= ϕ;
7) tr |= FL ϕ ⇐⇒ ∃ i ≥ 0 : c1 c2 . . . ci ∈ L and tr|i |= ϕ;
8) tr |= GL ϕ ⇐⇒ ∀ i ≥ 0 : c1 c2 . . . ci ∈ L implies tr|i |= ϕ.
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 specific 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 |= FbL ϕ ⇐⇒ either ∀ i ≥ 0 : c1 c2 . . . ci ∈
/ L, or tr |= FL ϕ.
It is easy to make sure that parameterized temporal operators introduced
above satisfy duality and fixed-point (expansion) properties.
Proposition 1. Let ϕ be an arbitrary LP-LT L formula, c ∈ C, L ⊆ C ∗ , and tr
be an arbitrary trajectory. Then
1) tr |= ¬Xc ϕ ⇐⇒ tr |= Yc ¬ϕ,
2) tr |= ¬Yc ϕ ⇐⇒ tr |= Xc ¬ϕ,
3) tr |= ¬FL ϕ ⇐⇒ tr |= GL ¬ϕ,
4) tr |= ¬GL ϕ ⇐⇒ tr |= FL ¬ϕ.
For every pattern L and a signal c denote by P ref1 (L) the set {c : ∃w ∈ C ∗ :
cw ∈ L} of 1-letter prefixes of signal flows in L, and by Suf fc (L) the pattern
{w : cw ∈ L} which consists of maximal proper suffixes of those signal flows in L
that begin with the signal c. We say that a family of patterns L is suffix-closed iff
for every signal c and every pattern L, L ∈ C, the pattern Suf fc (L) also belongs
to L.
Proposition 2. Suppose that a family of patterns L is suffix-closed, and let ϕ
be a LP-LT L formula, and tr be a trajectory. Then
W
1) if ε ∈ L then tr |= FL ϕ ⇐⇒ tr |= ϕ ∨ Xc FSuf fc (L) ϕ,
c∈P ref1 (L)
W
2) if ε ∈
/ L then tr |= FL ϕ ⇐⇒ tr |= Xc FSuf fc (L) ϕ,
c∈P ref1 (L)
V
3) if ε ∈ L then tr |= GL ϕ ⇐⇒ tr |= ϕ ∧ Yc FSuf fc (L) ϕ,
c∈P ref1 (L)
V
4) if ε ∈
/ L then tr |= GL ϕ ⇐⇒ tr |= Yc FSuf fc (L) ϕ.
c∈P ref1 (L)
As in the case of ordinary LTL these properties are important for building
model checking and satisfiability checking procedures for LP-LT L formulae.
4 Model checking sequential reactive systems against
LP-LT L specifications
Assume that sequential reactive systems are modeled by finite 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 specifications is that of checking, given a finite state transducer
π and a LP-LT L formula ϕ, whether tr |= ϕ holds for every trajectory tr in
T r(π, S) (or, in symbols, T r(π, S) |= ϕ).
It is evident that decidability and complexity of MC problem for sequen-
tial reactive systems against LP-LT L specifications 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 effective 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 flows. LP-LT L formulae of this type will be called Reg-
LT L formulae. The main advantage of Reg-LT L is that the most simple model
of computation — deterministic finite state automata — can be involved to
define basic predicates and patterns occurred in these formulae.
By (non-initialized) deterministic finite state automaton we mean a quadru-
ple K = (Σ, Z, Zacc , Φ), where Σ is a finite input alphabet, Z is a finite 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 ∈ Σ ∗ . 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) ∈ Zacc ; thus, it specifies a regular language
L(K, z0 ) = {w : Φ(z0 , w) ∈ Zacc } of all accepted words.
When finite state automata are used for specification of regular basic predi-
cates they have the set of basic actions A as an input language; automata of this
kind will be called A-automata. When finite state automata are employed for
specification 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 tem-
poral 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 accept-
ing 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 redefined in terms of finite state au-
tomata. Suppose, for example, that a run of a transducer begins with a transition
c,h
q −→ q 0 . Then tr(run) |= Xc (A, z0 ) ⇐⇒ h ∈ (A, z0 ) ⇐⇒ Φ(z0 , h) ∈ Zacc .
This effect 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) |= F(B,z0 ) ϕ ⇐⇒ ∃ i ≥ 0 : Φ(z0 , c1 c2 . . . ci ) ∈ Zacc and
tr(run|i ) |= shif t(ϕ, h1 h2 . . . hi );
tr(run) |= G(B,z0 ) ϕ ⇐⇒ ∀ i ≥ 0 : Φ(z0 , c1 c2 . . . ci ) ∈ Zacc implies
tr(run|i ) |= shif t(ϕ, h1 h2 . . . 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 finite words over A and MC problem T r(π) |= ϕ is studied for finite
state transducers against Reg-LT L specifications.
The main result of this section is
Theorem 1. Let π = (C, A, Q, Q0 , T ) be a finite 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 specified
by a deterministic finite state automata which has N states at the most. Then
there exists a generalized Büchi automaton M [π, ϕ] such that
|ϕ|
– M [π, ϕ] has |π|2O(|ϕ|N ) states at the most;
– M [π, ϕ] can be constructed effectively by π and ϕ in time polynomial of its
size;
– M [π, ϕ] accepts empty ω-language iff T r(π) |= ϕ.
Proof. (Sketch) Our algorithm for the translation of a pair (π, ϕ) to a Büchi
automaton M [π, ϕ] follows the well-known scheme for translation of LTL formu-
lae to Büchi automata which was introduced in [21]. We only emphasize those
aspects of this translation which are specific for Reg-LT L.
1. Consider the formula ψ = ¬ϕ and present it in negation normal form via
duality laws (see Proposition 1). It should be noted that if a basic predicate is
specified by an automaton (A, z0 ) then ¬(A, z0 ) ≡ (Ā, z0 ), where Ā is a comple-
mentation of A. Thus, we eliminate all negations in ψ.
2. Define the closure cl(ψ) of ψ as the minimal set of Reg-LT L formulae which
complies with the following rules:
• ψ ∈ cl(ψ),
• (A, z0 ) ∈ cl(ψ) ⇒ ∀ z ∈ Z : (A, z) ∈ cl(ψ)
• f ∨ g ∈ cl(ψ) ⇒ f, g ∈ cl(ψ),
• f ∧ g ∈ cl(ψ) ⇒ f, g ∈ cl(ψ),
• Xc f ∈ cl(ψ) ⇒ shif t(f, h) ∈ cl(ψ) for every h ∈ A∗ ,
• Yc f ∈ cl(ψ) ⇒ shif t(f, h) ∈ cl(ψ) for every h ∈ A∗ ,
• F(B,z0 ) f ∈ cl(ψ) ⇒ f ∈ cl(ψ) and ∀ c ∈ C : Xc F(B,Φ(z0 ,c)) f ∈ cl(ψ),
• G(B,z0 ) f ∈ cl(ψ) ⇒ f ∈ cl(ψ) and ∀ c ∈ C : Yc G(B,Φ(z0 ,c)) f ∈ cl(ψ).
As it can be seen from the definition of cl(ψ) this set may contain O(|ϕ|N |ϕ| ) 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
satisfies the following requirements:
– if (A, z0 ) ∈ K then z0 ∈ Zacc ;
– if Xc1 f ∈ K and Xc2 f ∈ K then c1 = c2 ,
and it is called saturated if it fulfills the rules listed below:
– if f ∨ g ∈ K then f ∈ K or g ∈ K;
– if f ∧ g ∈ K then f ∈ K and g ∈ K;
– if F(B,z0 ) f ∈ K then either Xc F(B,Φ(z0 ,c)) ∈ K for some signal c, or f ∈ K
in the case of z0 ∈ Facc ;
– if G(B,z0 ) f ∈ K then Yc G(B,Φ(z0 ,c)) ∈ K for every signal c, and, moreover, f
is also in K in the case of z0 ∈ Facc .
4. Build a generalized Büchi automaton M [π, ϕ] = (Q × CS(ψ), Init, ∆, F) over
the input alphabet C × A∗ , where
• Q × CS(ψ) is the set of states of the automaton,
• Init = {(q0 , K) : q0 ∈ Q0 , ψ ∈ K} is the set of initial states,
• ∆ = ∆1 ∪ ∆2 ∪ ∆3 is a transition relation which is defined as follows:
c,h c,h
• (q, K) −→ (q 0 , K 0 ) ∈ ∆1 iff 1) q −→ q 0 ∈ T , 2) a set K contains at least
one formulae Xc ϕ, and 3) {shif t(ϕ, h) : Xc ϕ ∈ K or Yc ϕ ∈ K} ⊆ K 0 ;
c,h c,h
• (q, K) −→ (q 0 , K 0 ) ∈ ∆2 iff 1) q −→ q 0 ∈ T , 2) a set K does not contain
any X-formulae, and 3) {shif t(ϕ, h) : Yc ϕ ∈ K} ⊆ K 0 ;
c,h c,h
• (q, K) −→ (q 0 , K) ∈ ∆3 iff 1) q −→ q 0 ∈ T , and 2) a set K does not
contain neither X-formulae, nor Y -formulae.
• F = {Fϕ : ϕ is a F -formula in cl(ψ)} 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) ∈ K ⇒ shif t(f, h) ∈ K.
5. Following the same line of reasoning as in [21] one could show that M [π, ϕ]
has an accepting computation iff the set T r(π) includes a trace tr such that
tr |= ψ. Thus, M [π, ϕ] is empty iff T r(π) |= ϕ.
Since emptiness of generalized Büchi automata can be checked in polynomial
time we arrived at
Corollary 1. Regular models checking of sequential reactive systems can be per-
formed effectively in time polynomial of the size of a model (finite state trans-
ducer) and double exponential of the size of a specification (Reg-LT L formula).
5 Conclusion
The main contribution of this paper is twofold:
1. we introduce a new framework for formal verification of sequential reactive
systems; it includes a concept of finite 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 finite state transducers operat-
ing 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 L-
specific 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 specification 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-fly approach used in LTL model checking [10] could be
applied to efficient verification of transducers against LP-LT L. In this paper
we presented in some details a solution to verification problem for finite state
transducers over free semigroups. But we believe that this result can be extended
further to comprise the cases of partially commutative semigroups (traces [9]),
free groups and free Abelian groups.
References
1. Alur R., Cerny P.: Streaming transducers for algorithmic verification of single-pass
list-processing programs. Proc. of 38-th ACM SIGACT-SIGPLAN Symposium on
Principles of Programming Languages (2011), p. 599-610.
2. Alur R., Moarref S., and Topcu U.: Pattern-based refinement of assume-guarantee
specifications in reactive synthesis. Proc. of 21-st International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, 2015.
3. Blattner M, Head T.: Single-valued a-transducers. Journal of Computer and Sys-
tem Sciences. 15 (1977), p. 310-327.
4. Blattner M, Head T.: The decidability of equivalence for deterministic finite trans-
ducers. Journal of Computer and System Sciences. 19 (1979), p. 45-49.
5. Bouajjani A., Jonsson B., Nilsson M., Touili T.: Regular Model Checking. Proc.
of 12-th International Conference on Computer Aided Verification, LNCS 1855
(2000), p. 403-418.
6. M. Canini, D. Venzano, P. Peresini, D. Kostic, J. Rexford.: A NICE way to Test
OpenFlow Applications. Proceedings of the 9th USENIX conference on Networked
Systems Design and Implementation, April 2012, p. 1-10.
7. Chemeritsky E. V., Smeliansky R. L., Zakharov V. A.: A formal model and verifi-
cation problems for software defined networks. Automatic Control and Computer
Sciences. 48 (2014), p. 398-406.
8. Culik K., Karhumaki J.: The equivalence of finite-valued transducers (on HDTOL
languages) is decidable. Theoretical Computer Science. 47 (1986), p. 71-84.
9. Diekert V., Metivier Y.: Partial commutation and traces. Handbook of Formal
Languages. 3 (1997), p. 457-533.
10. Gerth R., Peled D., Vardi M. Y., Wolper P.: Simple on-the-fly automatic verifi-
cation of linear temporal logic. Proc. of 15-th IFIP International Symposium on
Protocol Specification, Testing and Verification, (1995), p 3-18.
11. Griffiths T.: The unsolvability of the equivalence problem for ε-free nondetermin-
istic generalized machines. Journal of the ACM 15 (1968), p. 409-413.
12. Ibarra O.: The unsolvability of the equivalence problem for Efree NGSM’s with
unary input (output) alphabet and applications. SIAM Journal on Computing,
1978, v. 4.
13. Kesten Y., Manna Z., McGuire H., Pnueli A.: A decision algorithm for full propo-
sitional temporal logic. Proc. of 5-th International Conference on Computer Aided
Verification, LNCS 697 (1993), p. 97-109.
14. Mohri M.: Finite-state transducers in language and speech processing. Computa-
tional Linguistics. 23 (1997), p. 269-311.
15. Reutenauer C., Schuzenberger M.P.: Minimization of rational word functions.
SIAM Journal of Computing. 30 (1991), p. 669-685.
16. Sakarovitch J., de Souza R.: On the decomposition of k-valued rational relations.
Proc. of 25-th International Symposium on Theoretical Aspects of Computer Sci-
ence. (2008), p.621-632.
17. Sakarovitch J., de Souza R.: On the decidability of bounded valuedness for trans-
ducers. Proc. of the 33-rd International Symposium on MFCS. (2008), p. 588-600.
18. Schutzenberger M. P.: Sur les relations rationnelles. Proc. of Conference on Au-
tomata Theory and Formal Languages. (1975), p. 209-213.
19. de Souza R.: On the decidability of the equivalence for k-valued transducers. Proc.
of 12-th International Conference on Developments in Language Theory. (2008),
p. 252-263.
20. Thakkar J., Kanade A., Alur R.: A transducer-based algorithmic verification of
retransmission protocols over noisy channels. Proc. of IFIP Joint International
Conference on Formal Techniques for Distributed Systems, LNCS, 7892 (2013),
p. 209-224.
21. Vardi M.Y., Wolper P.: Reasoning about infinite computations. Information and
Computation. 115 (1994), p. 137.
22. Veanes M., Hooimeijer P., Livshits B., et al.: Symbolic finite state transducers:
algorithms and applications. Proc. of the 39-th ACM SIGACT-SIGPLAN Sym-
posium on Principles of Programming Languages. ACM SIGPLAN Notices. 147
(2012), p. 137-150.
23. Weber A.: Decomposing finite-valued transducers and deciding their equivalence.
SIAM Journal on Computing. 22 (1993), p. 175-202.
24. Wolper P., Boigelot B.: Verifying systems with innite but regular state spaces.
Proc. 10-th Int. Conf. on Computer Aided Verication (CAV-1998). LNCS. 1427
(1998), p. 8897.
25. Zakharov V.A.: Equivalence checking problem for finite state transducers over
semigroups. Proc. of the 6-th International Conference on Algebraic Informatics
(CAI-2015). LNCS. 9270 (2015), p. 208-221.