conclusion.tex
\section{Concluding Remarks}
\label{section-conclusion}

We have introduced a family of temporal logics to specify the behavior of systems
by assuming that the sequence of actions is isomorphic to some 
well-ordered linear ordering (see the bouncing ball example in Section~\ref{section-control}).
 Our aim is to control such physical systems by designing
controllers that safely work on $\omega$-sequences but 
interact synchronously with the physical system in order to restrict their behaviors.
We have extended linear-time temporal logic LTL  to $\aordinal$-sequences for any countable ordinal $\aordinal$
closed under addition, 
by considering quantitative operators indexed by ordinals smaller than $\aordinal$. This is a new class of 
linear-time temporal logics for which we have shown that $\logic{\omega^{\omega}}$ is decidable by reduction 
to the monadic second-order theory 
$\pair{\omega^{\omega}}{<}$
and for every $k \geq 1$, $\logic{\omega^{k}}$  
satisfiability problem is \pspace-complete
[resp. \expspace-complete] when the integers are encoded in unary [resp. in binary] generalizing what is known 
about LTL. 
Our proof technique is inspired from~\cite{Vardi&Wolper94} with significant extensions in order to 
deal with the interaction between arithmetics
on ordinals and temporal operators. We have introduced a new class of succinct ordinal automata in 
order to fully characterize  the 
complexity of the logics. The treatment of these  aspects leads to
 the most difficult technical parts of the paper.
Finally, the complexity results for satisfiability can be lifted to model-checking:
the model checking problem for $\logic{\omega^k}$ is \pspace-complete [resp. \expspace-complete]
when the integers are encoded in unary [resp. binary]. 



A lot of work remains to be done even though our logics 
%\iftechrep
working on $\omega^k$-sequences
%\fi
have been shown
to admit reasoning tasks of complexity similar to that of LTL. 
Synthesis of controllers working on $\omega$-sequences on the line of 
Section~\ref{section-control} is on the top of our priority list
as well as the search for well-motivated examples where ordinals greater than $\omega^2$ are needed.  
%\iftechrep
%% Ste 22/03/06
%% Extensions of some results  in~\cite{Arnold&Vincent&Walukiewicz02} is a possible direction. 
It is also natural to wonder whether $\logic{\omega^{\omega}}$ satisfiability is an elementary problem and whether
for every countable ordinal $\aordinal$, $\logic{\aordinal}$ is decidable. Observe  
that the monadic second-order theory
of every countable ordinal $\aordinal$ is known to be decidable~\cite{Buchi&Siefkes73} but this theory has no addition
and we need it in some way in $\logic{\aordinal}$ to deal with the operators $\next{\aordinalbis}$.
Finally, LTL is known to be initially equivalent to the first-order theory of $\pair{\omega}{<}$ 
by Kamp's theorem~\cite{Kamp68}
and by the separation theorem~\cite{Gabbay&Pnueli&Shelah&Stavi80}.
Is $\logic{\omega^{k}}$ also initially equivalent to   the first-order theory of $\pair{\omega^k}{<}$?
It is unlikely the case since by~\cite{Hirshfeld&Rabinovich03}, the future fragment of MLO over the class of ordinals does not have the finite base property.
%\else
%Moreover, LTL is known to be initially equivalent to the first-order theory of $\pair{\omega}{<}$ 
%by Kamp's theorem~\cite{Kamp68}
%and by the separation theorem~\cite{Gabbay&Pnueli&Shelah&Stavi80}.
%Is $\logic{\omega^{k}}$ also initially equivalent to   the first-order theory of $\pair{\omega^k}{<}$?%
%\fi
%%
%%  
%% \subsection{Summary}
%% 
%% \subsection{Open problems}
%% 
%% \begin{itemize}
%% \itemsep 0 cm
%% \item Is $\logic{\omega^k}$ initially equivalent to the first-order theory of $\pair{\omega^k}{<}$?
%%       (as LTL is initially equivalent to $\pair{\omega}{<}$ by Kamp's theorem~\cite{Kamp68}
%%        and Separation Theorem~\cite{Gabbay&Pnueli&Shelah&Stavi80}).
%%        % \marginpar{Il faut au moins rajouter
%%        % $\Box$. Nicolas Bedon semble penser que la logique de Rhode a laquelle 
%%        % on ajoute les predicats
%%        % ``etat initial'' et ``etat limite'' serait complete.}
%% \item  Is $\logic{\aordinal}$ decidable for every countable ordinal $\aordinal$?
%% \item We know that $\logic{\omega^{\omega}}$ is decidable.
%%        Is it elementary? 
%%        % \marginpar{J'ai l'impression que 
%%        % $\aformula \in \logic{\omega^{\omega}}$ est satisfaisable ssi
%%        % $\aformula[\omega^{\omega} \leftarrow \omega^{k_{max} +1}]$ est 
%%        % $\logic{\omega^{\omega^{k_{max} +1}}}$ satisfaible ou
%%        % tous les ordinaux apparaissant dans $\aformula$ à part $\omega^{\omega}$
%%        % sont strictement inferieurs a $\omega^{k_{max} + 1}$. Je n'arrive cependant pas a le prouver.
%%        % La complexite de $\logic{\omega^{\omega}}$ serait alors completement caracterisee.}
%%        %     
%% \item Controller synthesis (B\"uchi automata).
%% \end{itemize}



%\iftechrep
\vspace{0.1in}

{\bf Acknowledgments.}
Thanks
to Peter van Emde Boas and Eric Allender for  pointing out us
the existence of~\cite[Corollary 3.36]{Balcazar&Diaz&Gabarro88} that
happens to be a key argument in the
proof of Theorem~\ref{theorem-main},
to Paul Schupp and Paul Gastin for providing us essential parts of Rohde's
thesis (we have now the whole document),
to Claudine Picaronny for providing us articles on ordinal automata,
to Nicolas Bedon for many electronical discussions, to Jean-Michel
Couvreur for fruitful discussions.
We would like to warmly thank Thierry Cachat for his comments
on earlier versions of this work and for so helpful and fruitful discussions.
We thank also Alexander Rabinovich for pointing us
to~\cite{Hirshfeld&Rabinovich03}
and for suggesting a simpler proof strategy for Theorem~\ref{theorem-main}.
Finally, we would like to thank the anonymous referees for their helpful
remarks and suggestions
on earlier versions.
%\fi

introduction.tex

\section{Introduction}
\label{section-introduction}


\paragraph{Control of physical systems.}


Modelling interaction between a computer system and a
physical system has to overcome the difficulty of the different time scales.
For example, reasoning 
about the connection between the
physical description of an electric circuit and its logical
description in VHDL 
(standard language designed and optimized for describing the behavior
of digital systems)
needs to take into account 
that the two descriptions are dealing with objects running at distinct speeds.
The speeds can be so different that some abstraction consists in  assuming
 one system evolves infinitely quicker than the other one.
Another kind of interaction consists of controlling  a physical system by a computer
system.
Usually, a physical system is modelled by differential
equations. Solving those equations can then involve computations of
limits.  
For instance, in the bouncing ball example~\cite{Cuijpers&Reniers&Engels01},
in a finite amount of time an infinite number of actions can be performed.
It is a Zeno sequence of actions. 
Similar behaviors have also been considered 
 to solve the
car-bee problem \cite{Hansen&Pandya&Zhou95}.
However, Zeno behaviors are usually excluded from the modelling of
real-time controllers, which is a  reasonable requirement (see e.g.~\cite{Bouyeretal03}),
but also from the modelling of the physical systems, see some exception 
in~\cite{Berard&Picaronny97,Heymannetal02}.
This is a quite drastic limitation, since  Zeno sequences are
often  acceptable behaviors for physical systems.


\paragraph{Beyond $\omega$-sequences.}


Our main motivation in this paper is to model Zeno behaviors and ultimately to control 
physical systems admitting such behaviors. To  do so, we introduce 
a specification logical language that is interpreted on
well-ordered linear orderings. 
Reasoning problems based on this logical language should admit efficient algorithms, as good as 
those for standard specification languages as  linear-time temporal logic LTL, see 
e.g.~\cite{Clarke&Grumberg&Peled00}. 
The $\omega$-sequences are already familiar objects in model-checking, see e.g.~\cite{Vardi&Wolper94}, even though
such infinite objects are never manipulated when model-checking
 finite-state programs. Indeed, most problems on
B\"uchi automata reduce to standard reachability questions on finite graphs.
In a similar fashion, the behaviors of physical systems are modeled in the paper by sequences
indexed by countable
%\iftechrep
ordinals (see e.g.~\cite{Rosenstein82}),
%\else
%ordinals,
%\fi
i.e. equivalence classes of well-ordered
linear orderings,   
even though as we will show most problems will also reduce to questions
on finite graphs. 
%% For instance, the law of movement of the pendulum is modelled by a set of
%% sequences of length $\omega^2$.
For instance, the law of movement of the bouncing ball is modelled by a set of
sequences of length $\omega^2$.
%
%% The specification of the pendulum, i.e. the set of acceptable
%% behaviors, is also characterized as  a set of sequences of the same
%% length $\omega^2$.
The specification of the ball, i.e. the set of acceptable
behaviors, is also characterized as  a set of sequences of the same
length $\omega^2$.
%
On the other hand, the controller is a computer system whose complete executions
are $\omega$-sequences.
In this paper, we allow Zeno behaviors of physical systems and we will present a specification language
working on sequences indexed by ordinals greater than the usual first infinite ordinal~$\omega$.



%% 
%% Various logics have been proposed to reason about temporal behaviors
%% of systems. Amongst them there is the Linear-time Temporal Logic (LTL)
%% for which a lot of technics have been developped, including B\"uchi
%% automata. 
%% 

\paragraph{Our contribution.}

We introduce a class of logics $\logic{\aordinal}$ indexed by a countable ordinal $\aordinal$ closed
under addition whose models are sequences of length $\aordinal$. 
Quantitative extensions of the standard next-time $\next{}$ and until $\until{}$ operators are considered
by allowing operators of the form $\next{\aordinalbis}$ and $\until{\aordinalbis}$ with $\aordinalbis$ smaller
than $\aordinal$.  
As shown in the paper, for every $\aordinal \leq \omega^{\omega}$, 
$\logic{\aordinal}$ can be viewed as a fragment of the monadic second-order theory $\pair{\omega^{\omega}}{<}$
known to be decidable, see e.g.~\cite{Buchi&Siefkes73}. 
For every $k \geq 1$, we show that $\logic{\omega^{k}}$ satisfiability is
\pspace-complete with an unary encoding of integers and \expspace-complete 
with a binary encoding. This generalizes non-trivially what is known about LTL.
We reduce the satisfiability problem to the non-emptiness problem of ordinal automata
recognizing transfinite words
\cite{Buchi64,Choueka78,Wojciechowski84,Hemmer&Wolper91,Bruyere&Carton01}.
The reduction entails that the satisfiability problem has an elementary complexity (by using~\cite{Carton02}) 
but does not guarantee the optimal upper bound.
We introduce a class of succinct ordinal automata of level $k$, $k \geq 1$ in which the 
 $\logic{\omega^{k}}$ formulae can be translated into and we prove that the
non-emptiness problem is in \nlogspace.
Succinctness allows us to reduce by one exponential the size of the automata obtained by translation which
provides us the optimal upper bound.
Analogous complexity results are  shown for model checking. 
Finally, we introduce and motivate 
a control problem with inputs a physical system 
$\mathcal{S}$ modelled by an ordinal automaton working on $\omega^k$-sequences,
and an $\logic{\omega^{k}}$ formula $\aformula$ describing the desirable behaviors of the system.
The problem we introduce is the existence of a controller $\mathcal{C}$ working on $\omega$-sequences
such that all the behaviors of  $\mathcal{S} \times \mathcal{C}$ satisfy  
the property $\aformula$. The synchronization
operation $\times$ takes into account the different time scales between 
$\mathcal{S}$ and $\mathcal{C}$ and the set of synchronization vectors depending on the set
of observable actions of the controller $\mathcal{C}$.
As a by-product of our results, checking whether a controller satisfies the above conditions can be
done effectively but we leave the question of the existence and synthesis of such controllers for future work.


\paragraph{Related work.} 
%Control:
%     \begin{itemize}
%     \item Synthesis of Rabin tree automata?~\cite{Arnold&Vincent&Walukiewicz02}
%     \item Control of Open systems in reactive environments~\cite{Kupfermanetal00}
%     \item to be completed
%     \end{itemize}

Our original motivation in this work is the control of systems with legal Zeno behaviors  by
systems whose complete executions are $\omega$-sequences.
The theory of control of discrete event systems was introduced in~\cite{Ramadge&Wonham89}.
In this theory, a process is a deterministic non-complete
finite automaton over an alphabet of events. The control problem
consists in, given a process $P$ and a set $S$ of admissible
behaviors, finding a process $Q$ such that the behaviors of $P
\times Q$ are in $S$ and such that $Q$ reacts to all uncontrollable
events and cannot detect unobservable events.
Extension to specifications from the modal $\mu$-calculus can be found in~\cite{Arnold&Vincent&Walukiewicz02}
whereas the control of timed systems (without Zeno behaviors) is for instance studied 
%\iftechrep
in~\cite{Asarin&Maler&Pnueli95,Henzinger&Kopke99,Bouyeretal03}.
%\else
%in~\cite{Asarin&Maler&Pnueli95,Bouyeretal03}.
%\fi
It is plausible that the techniques from the above-mentioned works 
%\iftechrep
(see also~\cite{Pnueli&Rosner89,Thomas95,Alur&LaTorre01}) 
%\else
%(see also~\cite{Pnueli&Rosner89})
%\fi
can be adapted 
to the control problem we have introduced but the technical contribution of this paper is mainly
oriented towards satisfiability and model-checking issues.





%% 
%% The theory of control of discrete event systems was introduced in
%% \cite{Ramadge&Wonham89}. In this theory, a process is a deterministic non-complete
%% finite automaton over an alphabet of events. The control problem
%% consists in, given a process $P$ and a set $S$ of admissible
%% behaviors, finding a process $Q$ such that the behaviors of $P
%% \times Q$ are in $S$ and such that $R$ reacts to all uncontrollable
%% events and cannot detect unobservable events.
%% %
%% %In \cite{Arnold&Vincent&Walukiewicz02}, the set of admissible events
%% %is replaced by a formula of the $\mu$-calculus.
%% 
%% % Automata-based approach for temporal logics and complexity:
%% %     \cite{Sistla&Clarke85,Vardi&Wolper94,Schnoebelen03}
%% 

The logics we have introduced belong to the long tradition of quantitative versions of LTL.
LTL-like logics having models non isomorphic to $\omega$ can be found 
in
%\iftechrep
\cite{Alur&Feder&Henzinger96,Rohde97,Reynolds03,Davorenatal04,Hirshfeld&Rabinovich04,Lutz&Walther&Wolter05}.
%\else
%\cite{Alur&Feder&Henzinger96,Rohde97,Reynolds03,Hirshfeld&Rabinovich04,Lutz&Walther&Wolter05}.
%\fi
Temporal operators in the real-time logics 
from \cite{Alur&Feder&Henzinger96,Hirshfeld&Rabinovich04,Lutz&Walther&Wolter05} are indexed by intervals as
our logics $\logic{\aordinal}$. However, among the above-mentioned works,  Rohde's thesis~\cite{Rohde97}
contains a LTL-like logic interpreted over $\aordinal$-sequences with ordinal $\aordinal$
but the temporal operators are simply
the standard next-time 
and  until operators without any decoration. It is shown in~\cite{Rohde97} that the satisfiability
problem for such a logic can be decided in exponential-time when the inputs are the formula to be tested and the countable
ordinal from which the model is built. 
Similarly, in~\cite{Baaz&Leitsch&Zach96} a temporal logic with next-time and sometimes operators but interpreted over 
well-founded trees of $\omega$-segments  is shown decidable by designing a cut-free sequent-style calculus. 
The concept of time gaps in~\cite{Baaz&Leitsch&Zach96} can be put naturally in correspondence with
limits for ordinals. No complexity issues are discussed in~\cite{Baaz&Leitsch&Zach96} even though the 
temporal logic with only temporal operator next-time is shown equivalent to the famous modal logic S4
interpreted over reflexive and transitive Kripke frames and known to
be \pspace-complete. 


%% 
%% 
%% \item[LTL-like logics over non $\omega$-sequences] \
%%      \begin{itemize} 
%%      \item propositional temporal logics~\cite{Rohde97}
%%      \item temporal logic for general linear time~\cite{Reynolds03}
%%      \item Temporal logics for general flow systems~\cite{Davorenatal04}.
%%      \item LTL over real with temporal operators U and S indexed by intervals 
%%       (no next)~\cite{Lutz&Walther&Wolter05}.
%%      \item MITL in \cite{Alur&Feder&Henzinger96}
%%      \item QTL in \cite{Hirshfeld&Rabinovich04}
%%      \end{itemize}
%% 

In the paper, we follow the automata-based approach for temporal logics from~\cite{Vardi&Wolper94} but
 we  deal with ordinal automata recognizing words of length $\aordinal$ for some countable ordinal
$\aordinal$. So, we extend  the reduction from LTL into generalized B\"uchi automata to
the reduction from $\logic{\omega^k}$ into ordinal automata recognizing words of length $\omega^k$.
Many classes of ordinal automata 
have been introduced in the literature. 
\ifijfcs
\else We recall below some of them.
\fi
In~\cite{Buchi64,Choueka78} automata recognizing $\omega^k$-sequences for some $k \geq 1$ are introduced making essential
the concept of layer. In~\cite{Buchi&Siefkes73,Wojciechowski84,Hemmer&Wolper91}, such automata are generalized to recognize
$\aordinal$-sequences for $\aordinal$ countable.
Correspondences between these different classes can be found in~\cite{Bedon98}. 
In the paper, we mainly adopt the definitions from~\cite{Hemmer&Wolper91}.
An elegant and powerful extension to automata recognizing words indexed elements from a linear ordering can be found
in~\cite{Bruyere&Carton01}. As far as we know, automata recognizing sequences of length greater than $\omega$
designed to solve verification problems 
have been first used in~\cite{Godefroid&Wolper94} to model concurrency by limiting the state explosion problem.
Similarly, timed automata accepting Zeno words are introduced in~\cite{Berard&Picaronny97} in order to model physical
phenomena with convergent executions. The non-emptiness problem for such automata is shown to be decidable~\cite{Berard&Picaronny97}.

%% \item[Automata for $\aordinal$-sequences] \
%%      \begin{itemize}
%%      \item Automata recognizing $\omega^k$-sequences~\cite{Buchi64,Choueka78}
%%      \item Automata recognizing $\aordinal$-sequences (countable $\aordinal$)
%%            \cite{Buchi&Siefkes73,Wojciechowski84,Hemmer&Wolper91}
%%      \item Correspondences between classes of automata~\cite{Bedon98}
%%      \item Automata on linear orderings~\cite{Bruyere&Carton01}
%%     \item Ordinal automata~\cite{Hemmer&Wolper91} 
%%      \item Trace automata~\cite{Godefroid&Wolper94}.
%%      \item Timed automata accepting Zeno words~\cite{Berard&Picaronny97}.
%%     \end{itemize}


As LTL can be viewed as the first-order fragment of 
monadic second order theory over $\pair{\Nat}{<}$,  
theories over $\pair{\aordinal}{<}$ for some countable ordinal
            $\aordinal$ have been also studied by B\"uchi~\cite{Buchi64}, see also~\cite{Buchi&Siefkes73,Bedon98}.
For instance, decidability of monadic second order theories over $\pair{\aordinal}{<}$ for some countable ordinal
            $\aordinal$  is shown in~\cite{Buchi&Siefkes73}. 
\ifijfcs
Decidability status of elementary theories
over countable ordinals have been established in~\cite{Bes02,Choffrut02}. 
\else
Decidability status of elementary theories
over countable ordinals have been established in~\cite{Bes02,Choffrut02} whereas relationships with other theories
are shown in~\cite{Maurin97}.
\fi

%% 
%% \item[Theories over ordinals] \
%%      \begin{itemize}
%%       \item Monadic second order theories of $\pair{\aordinal}{<}$ for some countable ordinal
%%             $\aordinal$~~\cite{Buchi64,Buchi&Siefkes73,Bedon98}
%%       \item Decidability status of elementary 
%%             theories of countable ordinals~\cite{Bes02,Choffrut02}.
%%       \item Links with other theories~\cite{Maurin97}.
%%       \item \cite{Bes02}
%%       \end{itemize}
%% 




\paragraph{Plan of the paper.} 
In Sect.~\ref{section-temporal-logics}, we recall  basic definitions about ordinals and we introduce a class
of linear-time temporal logics parameterized by the length of the models. In Sect.~\ref{section-decidability},
we show that any logic admitting models of length $\aordinal$ with $\aordinal \leq \omega^{\omega}$ is 
decidable by translation into the decidable monadic second order theory $\pair{\omega^\omega}{<}$. 
Sect.~\ref{section-translation} shows how the class of models of a given formula from a logic
working on $\omega^k$-sequences ($k < \omega$) can be recognized by an ordinal automaton.
To do so, we substantially extend what is known about LTL with generalized B\"uchi automata.
In order to fully characterize the complexity of logics working on 
$\omega^k$-sequences (\expspace-completeness or \pspace-completeness depending on the way integers are
encoded), in Sect.~\ref{section-complexity} 
we introduce a class of succinct ordinal automata of level $k$, extending  generalized
B\"uchi automata, and we show that the emptiness problem is \nlogspace-complete.
In Sect.~\ref{section-control}, since we have at this point all the necessary background, 
 we present the control problem that motivates 
our investigations. We prove that we can decide whether a given controller
satisfies the properties stated in our logical framework.
Sect.~\ref{section-conclusion} contains concluding remarks and open problems. \\

\noindent
This paper is a completed version of~\cite{Demri&Nowak05a}.
Full proofs can be found \ifxarchiv  in the technical appendix \else in~\cite{Demri&Nowak05}.\fi 
%Because of lack of space, the proofs can be found in~\cite{Demri&Nowak05}. 


macros.tex

\newcommand{\set}[1]{\{ #1 \}} 
\newcommand{\sequence}[2]{\langle #1, \ldots, #2 \rangle}
\newcommand{\couple}[2]{\langle #1,#2 \rangle}
\newcommand{\pair}[2]{\langle #1,#2 \rangle}
\newcommand{\triple}[3]{\langle #1,#2,#3 \rangle}
\newcommand{\quadruple}[4]{\langle #1,#2,#3,#4 \rangle}
\newcommand{\Nat}{\ensuremath{\mathbb{N}}}
\newcommand{\Rat}{\ensuremath{\mathbb{Q}}}
\newcommand{\Rea}{\ensuremath{\mathbb{R}}}
\newcommand{\Zed}{\ensuremath{\mathbb{Z}}}
\newcommand{\true}{\top}
\newcommand{\false}{\perp}
\newcommand{\bottom}{\perp}
\newcommand{\powerset}[1]{2^{#1}}
\newcommand{\npowerset}[2]{{\cal P}^{#1}(#2)}
\newcommand{\finitepowerset}[1]{{\cal P}_f(#1)}
\newcommand{\card}[1]{{\rm card}(#1)}
\newcommand{\amap}{f}
\newcommand{\amapbis}{g}
\newcommand{\aset}{X}
\newcommand{\asetbis}{Y}
\newcommand{\asetter}{Z}
\newcommand {\length}[1] {\ensuremath{|#1|}}
\newcommand {\lenght}[1] {\ensuremath{|#1|}}









% formulae
\newcommand{\avarprop}{p}
\newcommand{\avarpropbis}{q} 
\newcommand{\avarpropter}{r} 
\newcommand{\varprop}{{\rm AP}} % Set of atomic propositions (for a given logic)
\newcommand{\aformula}{\phi} % a formula
\newcommand{\aformulabis}{\psi} % another formula (when at least 2 are present)
\newcommand{\aformulater}{\varphi} % another formula (when at least 3 are present)
\newcommand{\next}[1]{{\tt X}^{#1}}
\newcommand{\mynext}[1]{\next{#1}}
\newcommand{\until}[1]{{\tt U}^{#1}}
\newcommand{\sometimes}[1]{{\tt F}^{#1}}
\newcommand{\always}[1]{{\tt G}^{#1}}


% Functions with formulae as arguments
\newcommand{\subf}[1]{sub(#1)} % set of subformulae in a broad sense
\newcommand{\cl}[1]{cl(#1)} % set of subformulae in a broad sense
\newcommand{\maxcons}[1]{maxcons(#1)}
\newcommand{\themodels}[1]{{\rm Mod}(#1)} % set of models
\newcommand{\maxexpo}[1]{{\rm exp}(#1)} % maximal exponent + 1


% Models
\newcommand{\amodel}{\sigma}


% Languages

\newcommand{\ainfword}{\sigma}
\newcommand{\aletter}{a}
\newcommand{\aletterbis}{b}
\newcommand{\aalphabet}{\Sigma}
\newcommand{\lang}[1]{{\rm L}(#1)}

% Automata
\newcommand{\aautomaton}{{\mathcal A}}
\newcommand{\aautomatonbis}{{\mathcal B}}


% Equivalences 
\newcommand{\egdef}{\stackrel{\mbox{\begin{tiny}def\end{tiny}}}{=}} % =def=
\newcommand{\eqdef}{\stackrel{\mbox{\begin{tiny}def\end{tiny}}}{\equiv}} % =def=
\newcommand{\equivdef}{\stackrel{\mbox{\begin{tiny}def\end{tiny}}}{\equivaut}} % <=def=>
\newcommand{\equivaut}{\;\Leftrightarrow\;}





\newcommand{\step}[1]{\xrightarrow{\!\!#1\!\!}}
\newcommand{\backstep}[1]{\xleftarrow{\!\!#1\!\!}}



% Complexity classes
\newcommand {\pspace} {\textsc{pspace}}
\newcommand {\nlogspace} {\textsc{nlogspace}}
\newcommand {\expspace} {\textsc{expspace}}
\newcommand {\np} {\textsc{np}}
\newcommand {\threeexptime} {\textsc{3exptime}}
\newcommand {\polytime} {\textsc{P}}
\newcommand{\twoexpspace}{\textsc{2expspace}}



% Ordinals
\newcommand{\aordinal}{\alpha}
\newcommand{\aordinalbis}{\beta}
\newcommand{\aordinalter}{\gamma}



\newcommand{\logic}[1]{{\rm LTL}(#1)}
\newcommand{\mainlogic}{\logic{\omega^{\omega}}}

% \newcommand{\qed}{\mbox{$\Box$}}

\newcommand{\aHsequence}{\rho}

\newcommand{\alanguage}{{\rm L}}
\newcommand{\alang}{{\rm L}}

\newcommand{\defplus}[3]{+_{#2}(#1,#3)}

\newcommand{\sstate}{{\rm q}_0}
\newcommand{\estate}{{\rm q}_{k'}}
\newcommand{\rstate}{{\rm q}_{k'}^{{\rm repeat}}}

\pagestyle{plain} % Sera a retirer de la version finale


\newcommand{\ourmult}{\times} 


proof-corollary-model-checking.tex
The proof is a slight variant of the LTL case.
Let $\aautomaton$ be an ordinal automaton and $\aformula$ be an $\logic{\omega^k}$ formula.
The only difference with LTL is that $\alang(\aautomaton)$ may contain words of length different from
$\omega^k$. Those words are excluded in the following way. 
By considering a natural intersection operator $\times$ on ordinal automata (see e.g. details in
Sect.~\ref{section-synchronous-product}), it is easy to show that
$\aautomaton \not \models \aformula$ iff
$\alang(\aautomaton \times \aautomaton_{\neg \aformula}) \neq \emptyset$.
\qed

proof-lemma-cantor.tex
First suppose that $\aordinal = \omega^{\aordinalbis}$ and 
take $\aordinalbis_1 \leq \aordinalbis_2 < \omega^{\aordinalbis}$.
The Cantor's normal form of $\aordinalbis_1$ [resp. $\aordinalbis_2$] is of the form
$\omega^{\aordinalter_1} n_1 + \aordinalter'_1$ [resp. $\omega^{\aordinalter_2} n_2 + \aordinalter'_2$]
with either $\aordinalter_2 > \aordinalter_1$ or $n_2 \geq n_1$. 
Hence,
$$\aordinalbis_1 + \aordinalbis_2 \leq \aordinalbis_2 +  \aordinalbis_2 < 
  \omega^{\aordinalter_2} \times n$$
for some $n > 1$. Consequently, $\aordinalbis_1 + \aordinalbis_2 <  \omega^{\aordinalbis}$ since
$\omega^{\aordinalter_2} \times n < \omega^{\aordinalter_2+1} \leq \omega^{\aordinalbis}$.

Now suppose that the Cantor normal form of $\aordinal$ is
$\omega^{\aordinalbis_1} . n_1 + \cdots + \omega^{\aordinalbis_p}
. n_p$ where $p>1$ and $n_p \not= 0$.
%
The ordinals 
$\omega^{\aordinalbis_1} . n_1$ and  $\omega^{\aordinalbis_1}$ are strictly less 
than $\aordinal$, but their sum is strictly greater.
 \qed

proof-proposition-lifting.tex
The proof is by an easy verification by observing that
$q \step{a} q'$ in $\aautomaton$ iff
there is a path $r: \omega^{k-1} +1 \rightarrow Q$  in $\mbox{\it lift}_k(\aautomaton)$
such that
$r(0) = \pair{k-1}{q}$,
$r(1) = \pair{0}{q'}$
 and $r(\omega^{k-1}) = \pair{k-1}{q'}$.\qed

proof-theorem-main.tex
In the unary case, the \pspace \ lower bound is a consequence of the \pspace-hardness of LTL~\cite{Sistla&Clarke85}
whereas in the binary, \expspace-hardness is a corollary of  Lemma~\ref{lemma-omega}.

As far as the upper bound is concerned,
in the unary [resp. binary] case, 
$\aautomaton_{\aformula}'$ is of size exponential [resp. doubly exponential] in $\length{\aformula}$ 
and requires only polynomial [resp.  exponential] space to be built. 
By adapting the proof of~\cite[Corollary 3.36]{Balcazar&Diaz&Gabarro88} and by considering 
Corollary~\ref{corollary-nlogspace-succinct} and Lemma~\ref{lemma-main-translation},
we obtain that given $\aformula$, testing the emptiness of $\alang(\aautomaton_{\aformula})$ can be done
in \pspace \ [resp. \expspace]. \qed

proof-theorem-model-checking.tex
Hardness is by an easy verification from the complexity of the standard
complexity results for the model checking fo  $\logic{\omega^k}$.


As far as the upper bound is concerned,
in the unary [resp. binary] case, 
$\aautomaton \times \aautomaton_{\aformula}'$ is of size exponential [resp. doubly exponential] in $\length{\aformula}$ 
and requires only polynomial [resp.  exponential] space to be built, see 
Lemma~\ref{lemma-x-succinct}. 
By adapting the proof of~\cite[Corollary 3.36]{Balcazar&Diaz&Gabarro88} and by considering 
Corollary~\ref{corollary-nlogspace-succinct} and Lemma~\ref{lemma-main-translation},
we obtain that given an $x$-succinct ordinal automata $\aautomaton$ of level $k$
and a formula $\aformula$ in $\logic{\omega^k}$, testing the emptiness of $\aautomaton \times \aautomaton_{\aformula}'$
 can be done
in \pspace \ [resp. \expspace]. \qed

final-demri-nowak-ijfcs.bbl
\begin{thebibliography}{10}

\bibitem{Alur&Feder&Henzinger96}
R.~Alur, T.~Feder, and T.~Henzinger.
\newblock The benefits of relaxing punctuality.
\newblock {\em Journal of the Association for Computing Machinery},
  43:116--146, 1996.

\bibitem{Alur&LaTorre01}
R.~Alur and S.~L. Torre.
\newblock Deterministic generators and games for {LTL} fragments.
\newblock In {\em LICS'2001}, pages 291--300. IEEE Computer Society Press,
  2001.

\bibitem{Arnold&Vincent&Walukiewicz02}
A.~Arnold, A.~Vincent, and I.~Walukiewicz.
\newblock Games for synthesis of controllers with partial observation.
\newblock {\em Theoretical Computer Science}, 303(1):7--34, 2003.

\bibitem{Asarin&Maler&Pnueli95}
E.~Asarin, O.~Maler, and A.~Pnueli.
\newblock Symbolic controller synthesis for discrete and timed systems.
\newblock In {\em Hybrid systems II}, volume 999 of {\em Lecture Notes in
  Computer Science}, pages 1--20. Springer, 1995.

\bibitem{Baaz&Leitsch&Zach96}
M.~Baaz, A.~Leitsch, and R.~Zach.
\newblock Completeness of a first-order temporal logic with time-gaps.
\newblock {\em Theoretical Computer Science}, 160(1--2):241--270, 1996.

\bibitem{Balcazar&Diaz&Gabarro88}
J.~Balc{\'a}zar, J.~D{\' i}az, and J.~Gabarr{\' o}.
\newblock {\em Structural Complexity I}.
\newblock Springer, Berlin, 2nd edition, 1988.

\bibitem{Bedon98}
N.~Bedon.
\newblock {\em Langages reconnaissables de mots index\'es par des ordinaux}.
\newblock PhD thesis, Universit\'e Marne-la-Vall\'ee, 1998.

\bibitem{Berard&Picaronny97}
B.~B\'erard and C.~Picaronny.
\newblock Accepting {Z}eno words: a way toward timed refinements.
\newblock In {\em MFCS'97}, volume 1295 of {\em Lecture Notes in Computer
  Science}, pages 149--158. Springer, 1997.

\bibitem{Bes02}
A.~B{\`es}.
\newblock Decidability and definability results related to the elementary
  theory of ordinal multiplication.
\newblock {\em Fundamenta Mathematicae}, 171:197--211, 2002.

\bibitem{Bouyeretal03}
P.~Bouyer, D.~D'Souza, P.~Madhusudan, and A.~Petit.
\newblock Timed control with partial observability.
\newblock In {\em CAV'03}, volume 2725 of {\em Lecture Notes in Computer
  Science}, pages 180--192. Springer, 2003.

\bibitem{Bruyere&Carton01}
V.~Bruy{\`e}re and O.~Carton.
\newblock Automata on linear orderings.
\newblock In {\em MFCS 2001}, volume 2136 of {\em Lecture Notes in Computer
  Science}, pages 236--247. Springer-Verlag, 2001.

\bibitem{Buchi64}
J.~B\"uchi.
\newblock Transfinite automata recursions and weak second order theory of
  ordinals.
\newblock In {\em Int. Cong. Logic, Methodology and Philosophy of Science,
  Jerusalem}, pages 3--23, 1964.

\bibitem{Buchi&Siefkes73}
J.~B\"uchi and D.~Siefkes.
\newblock {\em The monadic second order theory of all countable ordinals},
  volume 328 of {\em Lecture Notes in Mathematics}.
\newblock Springer, 1973.

\bibitem{Cachat06}
T.~Cachat.
\newblock Controller synthesis and ordinal automata.
\newblock In {\em ATVA'06}, Lecture Notes in Computer Science. Springer, 2006.
\newblock To appear.

\bibitem{Carton01}
O.~Carton.
\newblock Automates et mots infinis.
\newblock Universit{\'e} de Marne-la-Vall{\'e}e, 2001.
\newblock Habilitation thesis.

\bibitem{Carton02}
O.~Carton.
\newblock Accessibility in automata on scattered linear orderings.
\newblock In {\em MFCS 2002}, volume 2420 of {\em Lecture Notes in Computer
  Science}, pages 155--164. Springer, 2002.

\bibitem{Choffrut02}
C.~Choffrut.
\newblock Elementary theory of ordinals with addition and left translation by
  $\omega$.
\newblock In {\em DLT'01}, volume 2295 of {\em Lecture Notes in Computer
  Science}, pages 15--20. Springer, 2002.

\bibitem{Choueka78}
Y.~Choueka.
\newblock Finite automata, definable sets, and regular expressions over
  $\omega^n$-tapes.
\newblock {\em Journal of Computer and System Sciences}, 17:81--97, 1978.

\bibitem{Clarke&Grumberg&Peled00}
E.~Clarke, O.~Grumberg, and D.~Peled.
\newblock {\em Model checking}.
\newblock The MIT Press Books, 2000.

\bibitem{Cuijpers&Reniers&Engels01}
P.~Cuijpers, M.~Reniers, and A.~Engels.
\newblock Beyond {Z}eno-behaviour.
\newblock Technical report, TU of Eindhoven, 2001.

\bibitem{Davorenatal04}
J.~Davoren, V.~Coulthard, N.~Markey, and T.~Moor.
\newblock Non-deterministic temporal logics for general flow systems.
\newblock In {\em In Proc. 7th Int. Workshop on Hybrid Systems: Computation and
  Control (HSCC 2004), Philadelphia, PA, USA}, volume 2993 of {\em Lecture
  Notes in Computer Science}, pages 280--295. Springer, Berlin, 2004.

\bibitem{Demri&Nowak05a}
S.~Demri and D.~Nowak.
\newblock Reasoning about transfinite sequences (extended abstract).
\newblock In D.~Peled and Y.-K. Tsay, editors, {\em ATVA'05}, volume 3707 of
  {\em Lecture Notes in Computer Science}, pages 248--262. Springer, 2005.

\bibitem{Fischer&Ladner79}
M.~Fischer and R.~Ladner.
\newblock Propositional dynamic logic of regular programs.
\newblock {\em Journal of Computer and System Sciences}, 18:194--211, 1979.

\bibitem{Gabbay&Pnueli&Shelah&Stavi80}
D.~Gabbay, A.~Pnueli, S.~Shelah, and J.~Stavi.
\newblock On the temporal analysis of fairness.
\newblock In {\em POPL'80}, pages 163--173. ACM Press, 1980.

\bibitem{Godefroid&Wolper94}
P.~Godefroid and P.~Wolper.
\newblock A partial approach to model checking.
\newblock {\em Information and Computation}, 110(2):305--326, 1994.

\bibitem{Hansen&Pandya&Zhou95}
M.~Hansen, P.~Pandya, and C.~Zhou.
\newblock Finite divergence.
\newblock {\em Theoretical Computer Science}, 138:113--139, 1995.

\bibitem{Harel83}
D.~Harel.
\newblock Recurring dominoes: making the highly undecidable highly
  understandable.
\newblock In {\em Foundations of Computing Theory}, volume 158 of {\em Lecture
  Notes in Computer Science}, pages 177--194. Springer-Verlal, 1983.

\bibitem{Hemmer&Wolper91}
J.~Hemmer and P.~Wolper.
\newblock Ordinal finite automata and languages (extended abstract).
\newblock Technical report, Universit{\'e} of Li{\`e}ge, 1991.

\bibitem{Henzinger&Kopke99}
T.~Henzinger and P.~Kopke.
\newblock Discrete-time control for rectangular hybrid automata.
\newblock {\em Theoretical Computer Science}, 1999:369--392, 1999.

\bibitem{Heymannetal02}
M.~Heymann, F.~Lin, G.~Meyer, and S.~Resmerita.
\newblock Analysis of {Z}eno behaviors in hybrid systems.
\newblock In {\em Proceedings of the 41st IEEE Conference on Decision and
  Control, Las Vegas, Nevada, USA}, pages 2379--2384, 2002.

\bibitem{Hirshfeld&Rabinovich03}
Y.~Hirshfeld and A.~Rabinovich.
\newblock Future temporal logic needs infinitely many modalities.
\newblock {\em Information and Computation}, 187(2):196--208, 2003.

\bibitem{Hirshfeld&Rabinovich04}
Y.~Hirshfeld and A.~Rabinovich.
\newblock Logics for real time: decidability and complexity.
\newblock {\em Fundamenta Informaticae}, 62:1--28, 2004.

\bibitem{Kamp68}
J.~Kamp.
\newblock {\em Tense Logic and the theory of linear order}.
\newblock PhD thesis, UCLA, USA, 1968.

\bibitem{Lutz&Walther&Wolter05}
C.~Lutz, D.~Walther, and F.~Wolter.
\newblock Quantitative temporal logics: {PSPACE} and below.
\newblock In {\em TIME'05}, pages 138--146, 2005.

\bibitem{Meyer73}
A.~Meyer.
\newblock Weak second order theory of successor is not elementary-recursive.
\newblock Technical Report MAC TM-38, MIT, 1973.

\bibitem{Pnueli&Rosner89}
A.~Pnueli and R.~Rosner.
\newblock On the synthesis of a reactive module.
\newblock In {\em 16th ACM POPL, Austin, Texas}, pages 179--190, 1989.

\bibitem{Rabinovich06}
A.~Rabinovich.
\newblock Private communication, August 2006.

\bibitem{Ramadge&Wonham89}
P.~J.~G. Ramadge and W.~M. Wonham.
\newblock The control of discrete event systems.
\newblock {\em Proceedings of the IEEE}, 77:81--98, 1989.

\bibitem{Reynolds03}
M.~Reynolds.
\newblock The complexity of the temporal logic with until over general linear
  time.
\newblock {\em Journal of Computer and System Sciences}, 66(2):393--426, 2003.

\bibitem{Rohde97}
S.~Rohde.
\newblock {\em Alternating Automata and The Temporal Logic of Ordinals}.
\newblock PhD thesis, University of Illinois, 1997.

\bibitem{Rosenstein82}
J.~Rosenstein.
\newblock {\em Linear Ordering}.
\newblock Academic Press, New York, 1982.

\bibitem{Sistla&Clarke85}
A.~Sistla and E.~Clarke.
\newblock The complexity of propositional linear temporal logic.
\newblock {\em Journal of the Association for Computing Machinery},
  32(3):733--749, 1985.

\bibitem{Thomas95}
W.~Thomas.
\newblock On the synthesis of strategies in infinite games.
\newblock In {\em STACS'95}, volume 900 of {\em Lecture Notes in Computer
  Science}, pages 1--13. Springer, 1995.

\bibitem{vanEmdeBoas97}
P.~van Emde~Boas.
\newblock The convenience of tilings.
\newblock In {\em Complexity, Logic, and recursion Theory}, volume 187 of {\em
  Lecture Notes in Pure and Applied Logic}, pages 331--363. Marcel Dekker,
  Inc., 1997.

\bibitem{Vardi&Wolper94}
M.~Vardi and P.~Wolper.
\newblock Reasoning about infinite computations.
\newblock {\em Information and Computation}, 115:1--37, 1994.

\bibitem{Wojciechowski84}
J.~Wojciechowski.
\newblock Classes of transfinite sequences accepted by nondeterministic finite
  automata.
\newblock {\em Annales Societatid Mathematicae Polonae}, pages 191--223, 1984.

\end{thebibliography}
