Finite variability interpretation of monadic logic of order.
We consider an interpretation of monadic second-order logic of order in the continuous time structure of finitely variable signals. We provide a characterization of the expressive power of monadic logic. As a by-product of our characterization we show that many fundamental theorems which hold in the discrete time interpretation of monadic logic are still valid in the continuous time interpretation.
Introduction
In the recent years systems whose behavior change in the continuous (real)
time were extensively investigated. Hybrid and control systems are prominent
examples of real time systems.
A run of a real time system is represented by a function from non-negative
reals into a set of values - the instantaneous states of a system. Such a function
will be called a signal. Usually, there is a further restriction on behavior of
continuous time systems. For example, a function that gives value q 0 for the
rationals and value q 1 for the irrationals is not accepted as a 'legal' signal.
A requirement that is often imposed in the literature is that in every bounded
time interval a system can change its state only finitely many times. This
requirement is called a finite variability (or a non-Zeno) requirement. A function
from the non-negative real into a set # that satisfies this requirement is called a
finitely variable signal. If in addition such function x satisfies the requirement
that for every t there is # > 0 such that x is constant on [t, t+#), then it is called
a right continuous signal. It is clear that finite variability and right continuous
requirements are not metric requirements.
Recall that the language L <
2 of monadic second order logic of order contains
individual variables, second order variables and the binary predicate <. In the
discrete time structure # (this structure will be defined precisely in section 3),
the individual variables are interpreted as natural numbers, the second order
variables as monadic predicates (monadic functions from the natural numbers
into the booleans), and < is the standard order on the set of natural numbers.
A monadic formula #(X) with one free predicate variable X defines a set
of #-strings over {0, 1} that satisfies #. There exists a natural one-one correspondence
between the set of #-strings over the alphabet {0, 1} n and the set of
n-tuples of monadic predicates over the set of natural numbers. With a formula
the set of #-strings which satisfies # through this correspondence
can be associated. Such a set of #-strings is called the #-language definable by
#. So, monadic logic can be considered as a formalism for the specification of
the behavior (set of runs) of discrete time systems. This logic is accepted as a
kind of an universal formalism among decidable formalisms for the specification
of discrete time behavior [13].
In this paper we consider interpretations of monadic logic in the continuous
time structures of the finitely variable signals and the right continuous signals.
In these structures the individual variables range over the non-negative real
numbers, the second order variables range over the finitely variable (respectively,
right continuous) boolean signals, and < is the standard order relation on the set
of real numbers. Similar to the discrete case, monadic logic can be considered
as a formalism for the specification of the behavior of continuous time systems.
Note that metric properties of reals cannot be specified in this logic.
We provide (see Theorem 1) a characterization of signal languages definable
in the monadic logic of order. The result is significant due to the fact that many
specification formalisms for reasoning about real time which were considered in
the literature can be e#ectively embedded in L <
2 . In [10] we illustrated the
expressive power of L <
2 by providing meaning preserving compositional translations
from Restricted Duration Calculus [4], Propositional Mean Value Calculus
[5] and Temporal Logic of Reals - TLR [3] into the first-order fragment of L <
.
We apply Theorem 1, for the analysis of a number of fundamental problems.
First, as an immediate consequence of our main result we obtain the decidability
of L <
under finitely variable and right continuous interpretations. These decidability
results were obtained in [9, 10] by the method of interpretation [7]. We
reduced in [9, 10] these decidability problem to the decidability problem for L <under F # interpretation. In F # interpretation the monadic predicate variables
range over the countable unions of closed subsets of reals. The decidability of
2 under under F # interpretation was shown to be decidable in [7].
Second, we show that under finitely variable and right continuous interpretations
the existential fragment of L <
2 is expressive complete, i.e. for every L <formula # there is an equivalent formula of the form #X 1 . #Xn#, where # is
a first-order monadic formula.
Then we reconsider two fundamental problems of Classical Automata The-
ory: (1) Automata characterization of the L <
definable languages and (2) The
uniformization problem.
The classical result of B-uchi provides an automata theoretical characterization
of the L <
definable languages It says that an #-language is definable by a
monadic formula (under the discrete interpretation) i# it is accepted by a finite
state automaton.
Let #(X, Y ) be a formula such that #X#Y # holds. The uniformization
problem for # is to find a finite state input-output automaton (transducer) such
that the function F computable by the automata satisfies #X.#(X, F (X)). The
uniformization problem for the monadic second order theory of order of the
structure # was solved positively by B-uchi and Landweber [2].
We check whether these classical results can be extended to continuous time.
In [11] automata that accept finitely variable languages were defined. It was
announced there that a finitely variability language is definable in monadic logic
i# it is accepted by a finite state automata. Here we show that this theorem is
a consequence of Theorem 1. In [11] it was announced that the uniformization
problem has a positive solution in the continuous time. We found a bug in our
proof. In the last section we show that the failure of the uniformization is a
consequence of Theorem 1.
The rest of this paper is organized as follows. In Section 2 terminology and
notations are fixed. In Section 3 the syntax and semantics of monadic second
order logic of order is recalled. Theorem 1 provides reductions between definable
#-languages and definable signal languages; it is stated in Section 4. In Section
5 we collect some simple lemmas and in Section 6 we prove the Theorem 1.
Section 7 gives some important corollaries.
2 Terminology and Notations
N is the set of natural numbers; R is the set of real numbers, R #0 is the set
of non negative reals; BOOL is the set of booleans and # is a finite non-empty
set. We use f # g for the composition of f and g.
A function from N to # is called an #-string over #. A function h from the
non-negative reals into a finite set # is called a finitely variable signal over # if
there exists an unbounded increasing sequence #
such that h is constant on every interval Below we will use 'signal'
for 'finitely variable signal'. We say that a signal x is right continuous at t i#
there is t 1 > t such that We
say that a signal is right continuous if it is right continuous at every t.
A set of #-strings over # is called an #-language over #. Similarly, a set of
finitely variable (respectively, right continuous) signals over # is called a finitely
variable (respectively, right continuous) #-signal language.
3 Monadic Second Order Theory of Order
3.1
The language L <
2 of monadic second order theory of order has individual vari-
ables, monadic second order variables, a binary predicate < , the usual propositional
connectives and first and second order quantifiers # 1 and # 2 . We use
t, v for individual variables and X, Y for second order variables. Often it will
be clear from the context whether a quantifier is the first or the second
in such cases we will drop the superscript. We use the standard abbreviations,
in particular, "#!" means "there is a unique".
The atomic formulas of L <are formulas of the form: t < v and X(t). The
formulas are constructed from atomic formulas by using logical connectives and
first and second order quantifiers.
We write #(X, Y, t, v) to indicate that the free variables of a formula # are
among X, Y, t, v.
3.2 Semantics
A structure
2 consists of a set A partially ordered by <K
and a set B of monadic functions from A into BOOL. The letters # and x, y
will range over the elements of A and B respectively. We will not distinguish
between a subset of A and its characteristic function. The satisfiability relation
defined in a standard way.
We sometimes use K
We will be interested in the following structures:
1. Structure #N, 2 N , <N #, where 2 N is the set of all monadic functions
from N into BOOL.
2. The signal structure Sig is defined as
SIG is the set of finitely variable boolean signals.
3. The right continuous signal structure Rsig is defined as
where RSIG is the set of right continuous boolean signals.
3.3 Definability
Let #(X) be an L <
be a structure. We say that
a set C # B is definable by #(X) if x # C if and only if K, x |= #(X).
Example (Interpretations of Formulas).
1. The formula #t
defines the #-language {(01) # ,
} in the structure # and defines the
set of all signals in the signal and right continuous signal structures.
2. The formula #Y. #t # .Y (t #t. X(t) # Y
defines in the structure # the set of
strings in which between any two occurrences of 1 there is an occurrence
of 0. In the signal structure the above formula defines the set of signals
that receive value 1 only at isolated points. The formula defines the empty
language under the right continuous signal interpretation.
In the above examples, all formulas have one free second order variable and they
define languages over the alphabet {0, 1}. A formula #(X 1 , .
second order variables defines a language over the alphabet {0, 1} n .
We say that an #-languages (finitely variable or right continuous signal lan-
guage) is definable if it is definable by a monadic formula in the structure #
(respectively in the structure Sig or Rsig).
4 Characterization of Definable Signal Languages
Recall that a function x from the non-negative reals into a finite set # is called a
finitely variable signal over # if there exists an unbounded increasing sequence
. such that x is constant on every interval
In this case there exists an #-string #a
alphabet # such that x(# i #-string
is said to represent a finite variable signal x. We denote by FV (s) the set
of finitely variable signals represented by an #-string s. For an #-language L
we use FV (L) for # s#L FV (s). Similarly, an #-string a 0 a 1 . an . over the
alphabet # represents a right continuous signal x if there is an unbounded
increasing sequence of reals such that
It is clear that every right continuous signal over # is represented
by an #-string over #. We denote by RC(s) the set of right continuous signals
represented by an #-string s. For an #-language L we use RC(L) for # s#L RC(s).
Theorem 1
1. A finitely variable signal language S is definable if and only if there is a
definable #-language L such that
2. A right continuous signal language S is definable if and only if there is a
definable #-language L such that
Our proof of Theorem 1 is constructive. In the proof of the if direction of
Theorem 1(2) we will provide a compositional mapping
2 such
that T r(#) defines the right continuous signal language RC(L), where L is an
#-language defined by #. From the proof of the only-if direction of Theorem
1(2), one can also extract an e#ective mapping T r
2 such that
the right continuous signal language defined by # is equal to RC(L), where
L is . the #-language defined by T r #). However, T r # is not compositional.
It is not di#cult to show that there is no n such that the length of T r #)
is bounded by expn (|#|), where expm (k) is the m-times iterated exponential
function (e.g. exp 2
). We do not know whether there exists a more
e#cient translation. Similar remarks hold for the proof of Theorem 1(1).
A natural question is whether Theorem 1 holds if we replace "definable" by
"definable in first-order monadic logic of order". The proof method used in this
paper does not allow to establish directly this result. However, the question has
a positive answer. The proof is based on the Shelah's compositional method
and will be given somewhere else.
In the next section some preliminary lemmas are collected. The proof of
Theorem 1 is given in Section 6.
5 Representation of signals by #-strings
In this section some basic notions and lemmas about the representation of signals
by #-languages are collected. The proofs of some lemmas are straightforward
and we omit them.
Lemma 2 Suppose that an #-string #a 0 , b 0 #a 1 , b 1 #a n , b n # . represents a
finitely variable signal x. Then x is right continuous if and only if a
all i.
Lemma 3 Let # be an order preserving bijection from R #0 to R #0 . An #-
string s represents x if and only if s represents x #.
5.1 Stuttering and Speed-Independence
#-strings that represent the same right continuous signal are said to be stuttering
equivalent. We will use # 1 for stuttering equivalence. It is easy to see that
the stuttering equivalence on #-strings is the smallest equivalence such that
a 0 a 1 . anan+1 . is equivalent to a 0 a 1 . ananan+1 .
#-strings over an alphabet # that represent the same finitely variable
language are said to be # 2 -equivalent. It is easy to see that the
-equivalence on #-strings over alphabet # is the smallest equivalence
such that #a 0 , b 0 #a 1 , b 1 #a n , b n #a n+1 , b n+1 # . is equivalent to
An #-language L is stuttering closed if whenever s # L and s # 1 s then
s # L. We use Stut 1 (L) for the stuttering closure of L, i.e. for the #-language
-closure of the languages over # is defined
similarly.
A finitely variable (right continuous) signal language L is speed-independent
if for every order preserving bijection #, x # L i# x # L. We use SI(L)
for speed-independent closure of L, i.e. for the language {x
L and # is an order preserving bijection}. Recall that FV (L) (respectively RC(L))
denotes the set of finitely variable (respectively right continuous) signals represented
by the #-strings of L. It is clear that FV (L) and RC(L) are speed-
independent.
We say that an #-language L represents a finitely variable (right continuous)
signal language S if for every x # S there is s # L that represents x and for
every s # L there is x # S represented by s.
The following is straightforward.
Lemma 4 1. If RC(s 1
2. if s 1
3. If FV
4. if s 1
5. A finite variable (right continuous) signal language S is speed-independent
6. An #-language L represents a finitely variable (respectively, right contin-
uous) signal language S i# Stut 2 (L) (respectively, Stut 1 (L)) represents
S.
7. An #-language L represents S i# L represents SI(S).
8. FV induces bijection between the set of Stut 2 -closed #-languages and the
set of speed-independent finitely variable languages.
9. RC induces bijection between the set of Stut 1 -closed #-languages and the
set of speed-independent right continuous languages.
Lemma 5 Every definable finitely variable (respectively right continuous) language
is speed-independent.
Proof: Let K be the finitely variable signal structure or the right continuous
signal structure. Let # : R #0 # R #0 be an order preserving bijec-
tion. By the structural induction on L <
formulas it is easy to show that
#. This implies the lemma. #
Lemma 6 (1) If L is a definable #-language, then Stut 1 (L) is definable. (2) If
L is a definable #-language over an alphabet #, then Stut 2 (L) is definable.
Moreover, there exists an algorithm that for every # constructs # such that the
#-language definable by # is the stuttering closure of the #-language definable
by #.
Proof: Lemma 6(1) was proved in [9]. The proof of Lemma 6(2) is almost the
same and is sketched below.
Recall [1], that a set L of #-strings is L <
definable i# L is a regular #-
language (see [13, 12] for a survey of automata on infinite objects). More-
over, there exist algorithms for translations between #-regular expressions and
2 formulas (see [13]). Let h be a regular language substitution defined as
h(#a, b#
the lemma follows from the the fact that regular #-languages are closed under
the regular morphisms and the inverse images of the regular morphisms.
Actually, the proof of this fact gives an algorithm for constructing an #-
regular expression for the image (pre-image) of an #-language L from an #-
regular expression that defines L and regular expressions that define a morphism

Hence, there is an algorithm that for every # constructs # such that the
#-language definable by # is the stuttering closure of the #-language definable
by #
Remark 7 The complexity of the algorithm extracted from the proof is non-
elementary, i.e. there is no n such that for every formula #, the run time of
the algorithm on # is bounded by expn (|#|), where expm (k) is m-time iterated
exponential function.
5.2 Set theoretical operations on languages
Let f be a function from a set A into # 1 - # 2 - . #n . We use the notation
(f) for the projection of f onto # is clear from the context
we sometimes will drop the subscript. Similarly for an #-string s over
use P roj #1-#1 (s) for the corresponding projection onto
Projections are extended pointwise to sets, i.e. for a set F of functions
we use P roj # for the set {P roj Below we use # , FV# and
RC# for the sets of all #-strings over #, finitely variable signals over #, and
right continuous signals over #, respectively.
Lemma 8 (operations on finitely variable signal languages and stuttering)
1. (Union) Let L 1 , L 2 be #-languages over # and let S 1 , S 2 be finitely
variable signal languages over #. If L i represents S i
represents
2. (Complementation) Let S be a speed-independent language. If L represents
S then the complementation of Stut 2 (L) represents the complementation
of S.
3. (Projection) Let L be an #-language (over
a finitely variable signal language S (over the alphabet # 1
represents P roj # i
(S).
4. (Cylindrification) Let L be an #-language that represents a finitely variable
signal language S (over an alphabet # 1 ). Then the language {x #
represented by {s
Lemma 9 (operations on right continuous signal languages and stuttering)
1. (Union) Let L 1 , L 2 be #-languages over # and let S 1 , S 2 be right continuous
signal languages over #. If L i represents S i
represents
2. (Complementation) Let S be a speed-independent language. If L represents
S then the complementation of Stut 1 (L) represents the complementation
of S.
3. (Projection) Let L be an #-language that represents a right continuous
signal language S (over an alphabet # 1 -# 2 ). Then P roj # i
(L) represents
(S).
4. (Cylindrification) Let L be an #-language that represents a right continuous
signal language S (over an alphabet # 1 ). Then the language {x #
represented by {s # 1
6 Proof of Theorem 1
6.1 The if direction
Let Cont(X, t) be the formula #t
be defined as -Cont(X, t). If x is a finitely variable
signal and # R #0 , then Jump(x, #) holds under the finitely variable interpretation
or x is not continuous at # . Such # are called jump points of x.
Similarly, if x is a right continuous and # R #0 , then Jump(x, #) holds under
the right continuous interpretation if or x is not continuous at # .
Scale) be the
formula obtained from # when the first order quantifiers are relativized to
the jump points of Scale, i.e., when "#t." and "#t." are replaced by
"#t. Jump(Scale, t) # ." and by "#t. Jump(Scale, t) # ." respectively.
The following lemma is immediate
Assume that # is obtained from # as described above. Let s
a i
1 . be #-strings for Assume that the set
of jump points of finitely variable (respectively right continuous) signal scale is
infinite. Let x i be finitely variable (respectively, right continuous) signals such
that x i
Let Infjump(X) be #t#t # .t # > t # (X(t) # -X(t # )). It is cleat that under
both the finitely variable and the right continuous interpretations, Infjump(x)
holds i# the set of jump points of x is infinite.
obtained
from # as above by relativizing the first order quantifiers to the jump
points of Scale. Lemma 10 implies that the right continuous signal language
definable by
#Scale. Infjump(Scale) #(X 1 , . ,
#t. Cont(Scale,
is equal to RC(L), where L is the #-language definable by #. This completes
the proof of the if direction of Theorem 1(2).
jump point of x.
m ) be a monadic formula. Let the formula # be
obtained from # by relativizing the first order quantifiers to the jump points of
implies that the finitely variable language definable by
#Scale. Infjump(Scale) #X j
#t. Cont(Scale, t) # (Cont(X j
#(-Jump(Scale,
is equal to FV (L), where L is the #-language definable by #.
Remark 11 Note that for every formula # we constructed a formula # such
that the #-language definable by # represents the right continuous signal language
definable by # . In our construction (1) the length of # is linear in the
length of #; (2) if # has the form Q does not have
the second order quantifiers and Q i are the second order quantifiers, then #
has the form #Scale.Q 1 X 1 . QnXn# , where # does not have the second order
quantifiers. Hence, we added one existential second order quantifier; (3) An alternative
proof of the if-direction: first, construct an automaton A # that accepts
the #-language L definable by # and then from A # construct a monadic formula
# that defines the signal language RC(L). However, the size of # extracted from
this proof is proportional to the size of A # and is non-elementary in the size of
#.
Similar remarks hold for the translation to formulas interpreted over finitely
variable signal structure, however, in this case several existential second order
quantifiers are added.
6.2 Proof of the only-if direction of Theorem 1(1)
Let L be an #-language. Lemma 4(5) implies that FV (L) (respectively RC(L))
is the unique speed-independent finitely variable (respectively, right continuous)
signal language represented by L. Therefore, by Lemma 5, in order to show the
only-if direction of Theorem 1 it is su#cient to prove that if a finitely variable
(right continuous) language is definable, then it is representable by a definable
#-language.
It is convenient instead of the finitely variable signal structure to consider
the first order structure #SIG; Sing, <, #, where SIG is the set of
finitely variable signals,
and # is interpreted as the usual inclusion relation.
be the formula in the first order language appropriate
for M , which is obtained from a monadic formula #(X 1 , . relativizing
the first order quantifiers to Sing (i.e., through the replacement of "# 1 t." by
"#t. Sing(t)#"), and by the replacement of "X(t)" by "t # X ". It is easy to see
that the signal language definable in Sig by # is the same as the signal language
definable in M by # .
Therefore, to establish the only-if direction of Theorem 1 it is su#cient to
show
Proposition 12 A language definable in M is representable by a definable #-
language.
Proof: Let LM be the the first order language appropriate for M . The proof
proceeds by the structural induction on the LM formulas. For every LM formula
that the #-language definable by # represents the signal language definable by
#.
Basis. The formula sing(X
#t. -X s (t) #!t. X j (t) corresponds
to the atomic formula Sing(X). The formula sing(X j
corresponds to X 1 < X 2 . The formula #t. X j
2 (t) corresponds to X 1 # X 2 .
Inductive Step. The inductive step is immediately obtained from Lemma
8 and Lemma 6. Indeed, negation corresponds to the complementation, the
existential quantifier corresponds to the projection and disjunction is easily expressible
from union and cylindrification. #
6.3 Proof of the only-if direction of Theorem 1(2)
The proof is obtained by the method of interpretation [7] as follows. Let
First, we construct a monadic formula
such that the language definable by # under the finitely variable
interpretation coincides with the language definable by # under the right
continuous interpretation.
Let rsignal(X) be the formula #t#t # . t # > t #t # .t < t # < t #
It is clear that a finitely variable signal satisfies rsignal(X) i# it is right
continuous.
Let # be obtained from # by relativizing all the second order quantifiers to
right continuous signals, i.e. by replacing "#X." (respectively "#X.")
by "#X. rsignal(X) # ." (respectively, "#X. It is easy to see that
a right continuous signal satisfies # under right continuous interpretation i# it
satisfies # under finitely variable interpretation. Hence, the required formula
can be defined as rsignal(X 1 )#rsignal(X 2 )#rsignal(Xn )#
# .
Now, by Theorem 1(1), there exists a #(X j
n ) such that
the #-language definable by # represents the language definable by # under
the finitely variable interpretation. Lemma 2 and the fact that the language
definable by # under the right continuous interpretation is the same as the right
continuous language definable by # under the finitely variable interpretation,
imply that the #-language definable by #X j
. # represents the language
definable by # under the right continuous interpretation.
7 Fundamental Corollaries
In this section we re-examine four fundamental theorems that hold in the structure
#. Three of these theorems still hold in the finitely variable and the right
continuous structures. Their proofs are easily derivable from Theorem 1. In [11]
we announced that the uniformization problem has a positive solution in the
structures Rsig and Sig. We found a bug in our proof, and here we will show
that in contrast to the discrete case of #-structure, the uniformization fails in
the Rsig and Sig structures.
7.1 Decidability
The satisfiability problem of the monadic second order theory of the structure
# is decidable ( B-uchi [1]). As a consequence of the B-uchi theorem and the
e#ectiveness of the proof of Theorem 1 we obtain a new proof of
Theorem 13 The monadic second order theory of the right continuous structure
is decidable. The monadic second order theory of the finitely variable structure
is decidable.
Note that the proofs of Theorem 13 given in [9, 10] is obtained by interpreting the
monadic theories of the right continuous and finitely variable signal structures
in the monadic theory of two successors. No characterizations of definable signal
languages can be extracted from these proofs.
7.2 Completeness of the Existential Fragment of Monadic
Logic
An existential monadic formula is a formula of the form #X 1 . #Xn .#, where
# does not contain the second order quantifiers. It is well known that every
equivalent (in the structure #) to an existential formula
#. Moreover, # can be constructed e#ectively from #. This together with
Theorem 1 and Remark 11 imply
Theorem 14 For every monadic formula # there exists an existential monadic
formula # such that # is equivalent to # in Rsig. Moreover, # can be constructed
e#ectively from #.
Theorem 15 For every monadic formula # there exists an existential monadic
formula # such that # is equivalent to # in Sig. Moreover, # can be constructed
e#ectively from #.
In the F # interpretation of monadic logic, the monadic predicates range over
subsets of the real line. The decidability of the monadic logic under F #
interpretation was established by Rabin [7].
As far as we know the following is an open problem
Open Question: Is the existential fragment of monadic logic complete for F #
Note that the existential fragment is in the first level of the alternation
hierarchy.
Open Question: Does the alternation hierarchy collapse for F # interpretation?
7.3 Failure of Uniformization
The uniformization problem for a theory Th in a language L can be formulated
as follows [6]: Suppose Th #
is an L-formula and
Y are tuples of variables. Is there another formula # such that
Y .#
Y ) and Th #
Y .#
Here #! means "there is a unique". Hence, # defines the graph of a function
which lies inside the set definable by #.
The uniformization problem for the monadic second order theory of order
of the structure # was solved positively by B-uchi and Landweber [2]. Below
we show that the uniformization fails in both the finitely variable and the right
continuous signal structures.
First observe that if for every order preserving bijection # on R #0 ,
then x is constant on the positive reals. Recall that the languages definable in
Rsig and in Sig are speed-independent (see Lemma 5). Therefore,
Lemma If a singleton language {x} is definable in Rsig or in Sig, then x
is constant on the positive reals.
Remark 17 (Contrast with a discrete case) Note that a singleton #-language
{x} is definable in the structure # i# x is quasiperiodic, i.e.,
As a consequence we have
Theorem The uniformization fails for the monadic second order theory of
order of the finitely variable structure. The uniformization fails for the monadic
second order theory of order of the right continuous structure.
Proof: Let #(Y ) be the formula #t#t # . t # > t # (Y (t) # -Y (t # )).
It is clear that Sig |= #Y.#(Y ) and that if Sig |= #(y) then y changes
infinitely often.
Assume that Sig |= #!Y. # (Y ). Then Lemma implies that the unique y
that satisfies # (Y ) is constant on the positive reals. Therefore, it cannot satisfy
To sum up, there is no # (Y ) such that
Hence, the uniformization fails for the monadic second order theory of order
of the finitely variable structure. The proof for the right continuous structure
signals is the same. #
7.4 Characterization of definable Languages by Automata
In this section we provide an automata theoretical characterization of the finitely
variable and the right continuous signal languages definable in monadic logic.
The characterization is a simple consequence of Theorem 1 and the automata
theoretical characterization of #-languages definable in monadic logic.
7.4.1 Syntax
A Labeled Transition System T is a triple #Q, # that consists of a set Q
of states, a finite alphabet # of actions and a transition relation # which is a
subset of Q-Q; we write q a
finite we say that
the LTS is finite;
Sometimes the alphabet # of T will be the Cartesian product # 1 - # 2 of
other alphabets; in such a case we will write q a,b
for the transition from q to
labeled by the pair (a, b).
An automaton A over # is a triple #T , INIT (A), FAIR(A)#, where
#Q, # is an LTS over the alphabet #; INIT (A) # Q - the initial states
of A. and FAIR(A) - a collection of fairness conditions (subsets of Q).
7.4.2 Semantics
A run of an automaton A is an #-sequence q 0 a 0 q 1 a 1 . such that q i
a i
all i. Such a run meets the initial conditions if q 0 # INIT (A). A run meets
the fairness conditions if the set of states that occur in the run infinitely many
times is a member of FAIR(A).
An #-string a 0 , a 1 . over # is accepted by A if there is a run q 0 a 0 q 1 a 1 .
that meets the initial and fairness conditions of A. The #-language accepted by
A is the set of all #-strings acceptable by A.
Theorem 19 (B-uchi [1]) An #-language is acceptable by a finite state automaton
i# it is definable by a monadic formula.
7.4.3 Automata as acceptors of signal languages
A right continuous signal x over # is accepted by an automaton A if there are
an #-string a 0 a 1 . an . over alphabet # acceptable by A and an unbounded
increasing sequence of reals such that
A finitely variable signal x over # is accepted by an automaton A if
A is an automaton over the alphabet # and there are an #-string
acceptable by A and an unbounded increasing sequence
of reals such that x(# i
A version of the next theorem was announced in [11] and it is immediately
derived from Theorem 1 and Theorem 19.
Theorem 20 A finitely variable (respectively, right continuous) signal language
is acceptable by a finite state automaton if and only if it is definable by a monadic
formula under the finitely variable (respectively, right continuous) interpretation

Acknowledgements

I would like to thank the anonymous referee for his very helpful suggestions.



--R

On a decision method in restricted second order arithmetic
Solving sequential conditions by finite-state strategies
A really abstract concurrent model and its fully abstract semantics.
Decidability and undecid- ablity results for Duration Calculus
A mean value calculus of duration.
Rabin's uniformization problem.
Decidability of second order theories and automata on infinite trees.
Decidable theories.
On translation of temporal logic of actions into monadic second order logic.
On the Decidability of Continuous Time Specification Formalisms.
From Finite Automata toward Hybrid Systems.
Automata on Infinite Objects.
Finite Automata
--TR
Automata on infinite objects
A mean value calculus of durations
On translations of temporal logic of actions into monadic second-order logic
A really abstract concurrent model and its temporal logic
Decidability and Undecidability Results for Duration Calculus
From Finite Automata toward Hybrid Systems (Extended Abstract)

--CTR
B. A. Trakhtenbrot, Understanding Basic Automata Theory in the Continuous Time Setting, Fundamenta Informaticae, v.62 n.1, p.69-121, January 2004
monadic logic of order;continuous time specification;definability