Equivalence of pointwise and continuous semantics for FO with linear constraints

with timestamps recorded along with it. Formally, an (in_nite) timed word _
over _ is an element of (_ _ R_0)! of the form (a0; t0)(a1; t1) _ _ _ , satisfying
the conditions that: for each i 2 N; ti < ti+1 (monotonicity), and for each
t 2 R_0 there exists an i 2 N such that t < ti (progressiveness).
We can model the properties of timed words using _rst-order logic with lin-
ear constraints (FO). Here variables in the FO sentence are interpreted over the
timeline of the model. Action predicates a(x) are unary predicates which asserts
to true i_ action a has happened at time x. Linear constraints are ternary pred-
icates de_ned over x; y; c where x and y are variables and c is a constant belongs
to R_0 and it evaluates to true if and only if x _ (y + c), where addition is a
binary function de_ned over reals in usual way. A timed word satis_es a property
expressed by FO sentence if and only if the sentence evaluates to true in that in-
terpretation. In the \continuous" interpretation of FO sentences, domain of the
variables can be as broad as total real time line where as in the \pointwise" in-
terpretation domain of variables is restricted to only timestamps where event has
happened. To illustrate this di_erence, consider the class of timed words which
have a time point x in the interval [0; 1] such that there is an action a exactly one
unit after that point. FO sentence 9x(0 _ x^x _ 1^9y(a(y)^y = x+1)) iden-
ti_es this property if variables x; y are interpreted in the continuous semantics.
But if the variables of this sentence are interpreted in the pointwise semantics
then timed words such as (a; 1:5) will not be accepted by the sentence. However
a di_erent sentence 9x(a(x) ^ 1 _ x ^ x _ 2) recognizes same class of languages
in any of these interpretations.
By interpreting the sentences in the pointwise semantics, the domain of the
variables is reduced from a dense one to a countably in_nite subset domain.
In this talk, we show that even then the expressive powers of pointwise and
continuous interpretations remain the same. That is, any property expressed by
the FO sentence interpreted in the continuous semantics can also be expressed
by a di_erent sentence in the pointwise interpretation.
It is not di_cult to see that the continuous semantics is at least as expressive
as the pointwise one, since one can ask for a time point to be an action point by
asserting
W
a2_ a(x) at each quanti_ed time point x. To prove the converse, we
_rst note that, if every variable is of the form 9x(a(x) ^ _), then the domain of
those variables are anyway restricted by a(x) clause, they will be interpreted in
the same way in both interpretation.We call these variables as \active" variables.
If the variables are not active, then we show that, it is possible to eliminate those
variables and replace them by set of active variables such that they recognizes
same timed language. If the sentence does not contain any active variables, then
we can use Fourier-Motzkin elimination to eliminate those variables. We use
Fourier-Motzkin elimination as the base case and then extend the arguments
inductively over the structure of the formulas.