IIT Bombay, Mumbai<EMAIL_ADDRESS>MPI-SWS, Kaiserslautern,
Germanykmadnani@mpi-sws.orghttps://orcid.org/0000-0003-0629-3847 MPI-SWS,
Kaiserslautern<EMAIL_ADDRESS>IIT Bombay, Mumbai,
<EMAIL_ADDRESS>Shankara Narayanan Krishna, Khushraj Madnani, Rupak
Majumdar and Paritosh K. Pandya [500]Theory of computation Logic This research
was sponsored in part by the Deutsche Forschungsgemeinschaft project 389792660
TRR 248—CPEC.

###### Acknowledgements.

We thank Tom Henzinger for an insightful discussion on Timed Logics and for
encouraging us to explore non-punctual subclasses for multi-clock TPTL and
ATA. We also thank Hsi-Ming Ho for an interesting discussion on handling
freeze quantifiers.

# Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals is
PSPACE-complete.

Shankara Narayanan Krishna  Khushraj Nanik Madnani  Rupak Majumdar  Paritosh
K. Pandya

###### Abstract

We investigate the decidability of the ${0,\infty}$ fragment of Timed
Propositional Temporal Logic (TPTL). We show that the satisfiability checking
of $\text{TPTL}^{0,\infty}$ is PSpace -complete. Moreover, even its 1-variable
fragment (1-$\text{TPTL}^{0,\infty}$) is strictly more expressive than Metric
Interval Temporal Logic (MITL) for which satisfiability checking is ExpSpace
complete. Hence, we have a strictly more expressive logic with computationally
easier satisfiability checking. To the best of our knowledge,
$\text{TPTL}^{0,\infty}$ is the first multi-variable fragment of TPTL for
which satisfiability checking is decidable without imposing any
bounds/restrictions on the timed words (e.g. bounded variability, bounded
time, etc.). The membership in PSpace is obtained by a reduction to the
emptiness checking problem for a new “non-punctual” subclass of Alternating
Timed Automata with multiple clocks called Unilateral Very Weak Alternating
Timed Automata (${\text{VWATA}^{0,\infty}}$) which we prove to be in PSpace .
We show this by constructing a simulation equivalent non-deterministic timed
automata whose number of clocks is polynomial in the size of the given
${\text{VWATA}^{0,\infty}}$.

###### keywords:

TPTL, Satisfiability, Non-Punctuality, Decidability, Expressiveness, ATA

##  1 Introduction

Metric Temporal Logic ($\text{MTL}[\mathsf{U}_{I},\mathsf{S}_{I}]$) and Timed
Propositional Temporal Logic
($\text{TPTL}[\mathsf{U}_{I},\mathsf{S}_{I}]$) are natural extensions of
Linear Temporal Logic ($\mathsf{LTL}$) for specifying real-time properties
[6]. MTL extends the $\mathsf{U}$ and $\mathsf{S}$ modality of $\mathsf{LTL}$
by associating a time interval with these. Intuitively, $a\mathsf{U}_{I}b$ is
true at a point in the given behaviour iff event $a$ keeps on occurring until
at some future time point within relative time interval $I$, event $b$ occurs.
(Similarly, $a\mathsf{S}_{I}b$ is its mirror image specifying the past
behaviour.) On the other hand, TPTL uses freeze quantifiers to store the
current time stamp. A freeze quantifier [4][6] has the form $x.\varphi$ with
freeze variable $x$ (also called a clock [7][27]). When it is evaluated at a
point $i$ on a timed word, the time stamp of $i$ (say $\tau_{i}$) is frozen or
registered in $x$, and the formula $\varphi$ is evaluated using this value for
$x$. Variable $x$ is used in $\varphi$ in a constraint of the form $T-x\in I$;
this constraint, when evaluated at a point $j$, checks if
$\tau_{j}-\tau_{i}\in I$, where $\tau_{j}$ is the time stamp at point $j$.
Here $T$ can be seen as a special variable giving the timestamp of the present
point. For example, the formula
$\varphi=\mathsf{F}x.(a\wedge\mathsf{F}(b\wedge
T-x\in[1,2]\wedge\mathsf{F}(c\wedge T-x\in[1,2])))$ asserts that there is a
point $i$ in the future where $a$ holds and in its future there is a $b$
within interval $[1,2]$ followed by a $c$ within interval $[1,2]$ from $i$. In
this paper, we restrict ourselves to future time modalities only. Hence, we
use the term MTL and TPTL for $\text{MTL}[\mathsf{U}_{I}]$ and
$\text{TPTL}[\mathsf{U}]$, respectively, and MTL+Past and TPTL+Past for
$\text{MTL}[\mathsf{U}_{I},\mathsf{S}_{I}]$ and
$\text{TPTL}[\mathsf{U},\mathsf{S}]$, respectively. We also confine ourselves
to the _pointwise_ interpretation of these logics [7].

While these logics are natural formalisms to express real-time properties, it
is unfortunate that both the logics have an undecidable satisfiability
checking problem, making automated analysis of these logics difficult in
general. Exploring natural decidable variants of these logics has been an
active area of research since their advent [5][30][13][35][29][14][15]. One of
the most celebrated such logics is the _Metric Interval Temporal Logic_ (MITL)
[1], a subclass of MTL where the timing intervals are restricted to be non-
punctual i.e. non-singular (intervals of the form $\langle x,y\rangle$ where
$x<y$). The satisfiability checking for MITL formulae is ExpSpace complete [1]
(the result also holds for MITL \+ Past).

Every formula in MTL can be expressed in the 1-variable fragment of TPTL
(denoted 1-TPTL). Moreover, the above-mentioned property $\varphi$ is not
expressible in MTL \+ Past [26]. Hence, 1-TPTL is strictly more expressive
than MTL [27, 7]. The Logic 1-TPTL can also express MTL augmented with richer
counting and Pnueli modalities. Hence, TPTL is a logic with high expressive
power. However, decidable fragments of TPTL are harder to find. While 1-TPTL
has decidable satisfiability over finite timed words [10] (albeit with non-
primitive recursive complexity), it is undecidable over infinite words [25].
There are no known fragments of multi-variable TPTL which are decidable
(without artificially restricting the class of timed words). In this paper, we
propose one such logic, which is efficiently decidable over both finite and
infinite timed words.

We propose a fragment of TPTL, called $\text{TPTL}_{0,\infty}$, where, for any
formula $\phi$ in negation normal form, each of its closed subformula $\kappa$
has _unilateral_ intervals; that is, intervals of the form $\langle
0,u\rangle$, or of the form $\langle l,\infty)$ (where $\langle\in\\{[,(\\}$
and $\rangle\in\\{],)\\}$). The main result of this paper is to show that
satisfiability checking for $\text{TPTL}_{0,\infty}$ is PSpace complete.
Moreover, we show that even the 1-variable fragment of this logic is strictly
more expressive than MITL. PSpace completeness for satisfiability checking is
proved as follows: We define a sub-class of Alternating Timed Automata (ATA
[24] [20]) called _Very Weak Alternating Timed Automata with Unilateral
Intervals_(${\text{VWATA}^{0,\infty}}$), and show that
${\text{VWATA}^{0,\infty}}$ have PSpace -complete emptiness checking. A
language preserving reduction from $\text{TPTL}_{0,\infty}$ to
${\text{VWATA}^{0,\infty}}$, similar to [10][24][34], completes the proof. To
our knowledge, ${\text{VWATA}^{0,\infty}}$ is amongst the first known fragment
of multi-clock alternating timed automata (ATA) with efficiently decidable
emptiness checking. Thus, we believe that $\text{TPTL}_{0,\infty}$ and
${\text{VWATA}^{0,\infty}}$ are interesting novel additions to logics and
automata for real-time behaviours.

One of the key challenges in establishing the decidability of
${\text{VWATA}^{0,\infty}}$ is to show that the configuration sizes can be
bounded. In an ATA, a configuration can be unboundedly large owing to several
conjunctive transitions, each spawning a state with a new clock valuation. We
provide a framework for compressing the configuration sizes of
${\text{VWATA}^{0,\infty}}$ based on simulation relations amongst states of
the ${\text{VWATA}^{0,\infty}}$. We then prove that such compression yields a
simulation-equivalent transition system whose configuration sizes are bounded.
This bound allows us to give a subset-like construction resulting in a
simulation equivalent (hence, language equivalent) timed automata with
polynomially many clocks.

The paper is organized as follows. Section 2 defines the TPTL and ATA, and
$(0,\infty)$ fragments of these formalisms. In Section 3, we prove the PSpace
emptiness checking of $\text{TPTL}^{0,\infty}$. Section 4 discusses the
expressiveness of $\text{TPTL}_{0,\infty}$. Section 5 concludes our work with
a discussion on the implication of our work in the field of timed logics and
some interesting problems that we leave open.

##  2 Preliminaries

Let $\mathbb{Z},\mathbb{Z}_{\geq 0},\mathbb{N},\mathbb{R},\mathbb{R}_{\geq 0}$
respectively denote the set of integers, non-negative integers, natural
numbers (excluding 0), real numbers, and non-negative real numbers. Given a
sequence $\mathbf{a}=a_{1}a_{2}\ldots$, $\mathbf{a}[i]=a_{i}$ denotes the
$i^{th}$ element of the sequence, $a[i..j]$ represents $a_{i}a_{i+1}\ldots
a_{j}$, $a[i..]$ represents $a_{i}a_{i+1}\ldots$ and $a[..i]$ represents
$=a_{1}a_{2}\ldots a_{i}$. Let $\mathcal{I}_{\mathsf{int}}$ be the set of all
the open, half-open, or closed intervals (i.e. convex subsets of real
numbers), such that the endpoints of these intervals are in
$\mathbb{N}\cup\\{0,\infty\\}$. Intervals of the form $[x,x]$ are called
punctual; a non-punctual interval is one which is not punctual. For,
$\langle{\in}\\{(,[\\}$ and $\rangle{\in}\\{],)\\}$, an interval of the form
$\langle 0,u\rangle$ for $u>0$ is called _right-sided_ while an interval of
the form $\langle l,\infty)$ is called _left-sided_. A _unilateral_ interval
is either left-sided or right-sided. Let
$\mathcal{I}_{\mathsf{int}}^{0},\mathcal{I}_{\mathsf{int}}^{\infty}\subseteq\mathcal{I}_{\mathsf{int}}$
respectively be the set of all _right sided_ and _left sided_ intervals of the
form $\langle 0,u\rangle$, $\langle l,\infty)$, for any
$l,u\in\mathbb{Z}_{\geq 0}$. Let
$\mathcal{I}_{\mathsf{int}}^{0,\infty}=\mathcal{I}_{\mathsf{int}}^{0}\cup\mathcal{I}_{\mathsf{int}}^{\infty}$.
For $\tau{\in}\mathbb{R}$ and interval $\langle a,b\rangle$, ${\tau+\langle
a,b\rangle}$ stands for the interval ${\langle\tau+a,\tau+b\rangle}$.
Timed Words. Let $\Sigma$ be a finite alphabet. A finite (infinite) word over
$\Sigma$ is a finite (infinite) sequence over $\Sigma$. The set of all the
finite (infinite) words over $\Sigma$ is denoted by $\Sigma^{*}$
($\Sigma^{\omega}$). A finite timed word $\mathbf{\rho}$ over $\Sigma$ is a
finite sequence of pairs $(\sigma,\tau)\in(\Sigma\times\mathbb{R}_{\geq
0})^{*}$ : $\mathbf{\rho}=(\sigma_{1},\tau_{1}),\ldots,(\sigma_{n},\tau_{n})$
where $\tau_{i}\leq\tau_{j}$ for all $1\leq i\leq j\leq n$. Let
$dom(\mathbf{\rho})=\\{1,2,\ldots n\\}$ be the set of points in
$\mathbf{\rho}$. Likewise, an infinite timed word is an infinite sequence
$\mathbf{\rho}=(\sigma_{1},\tau_{1})(\sigma_{2},\tau_{2})\ldots\in(\Sigma\times\mathbb{R}_{\geq
0})^{\omega}$, where $\sigma_{1}\sigma_{2}\ldots\in\Sigma^{\omega}$, and
$\tau_{1}\tau_{2}\ldots$ is a monotonically increasing infinite sequence of
real numbers approaching $\infty$ (i.e. non-zeno). A finite (infinite) timed
language is a set of all finite (infinite) timed words over $\Sigma$ denoted
$T\Sigma^{*}$ ($T\Sigma^{\omega}$).
Timed Propositional Temporal Logic (TPTL). The logic TPTL extends
$\mathsf{LTL}$ with freeze quantifiers and is evaluated on timed words.
Formulae of TPTL are built from a finite alphabet $\Sigma$ using Boolean
connectives, as well as the temporal modalities of $\mathsf{LTL}$. In
addition, TPTL uses a finite set of real-valued variables called freeze
variables or _clocks_ $X=\\{x_{1},\ldots,x_{n}\\}$. Let
$\nu:X\rightarrow\mathbb{R}_{\geq 0}$ represent a valuation assigning a non-
negative real value to each clock. Without loss of generality, we work with
TPTL in the negation normal form, where all the negations appear only with
atomic formulae. Formulae of TPTL are defined as follows.

$\varphi::=a\leavevmode\nobreak\ |\leavevmode\nobreak\ \neg
a\leavevmode\nobreak\ |\top\leavevmode\nobreak\ |\leavevmode\nobreak\
\bot\leavevmode\nobreak\ |\leavevmode\nobreak\ x.\varphi\leavevmode\nobreak\
|\leavevmode\nobreak\ T-x\in I\leavevmode\nobreak\ |\leavevmode\nobreak\
\varphi\wedge\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\varphi\vee\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\varphi\mathsf{U}\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathsf{G}\varphi,$
where $x\in X$, $a\in\Sigma$, $I\in\mathcal{I}_{\mathsf{int}}$111Notice that
duals of Until; “Unless” and “Release” operators can be expressed using a
$\mathsf{G}$ and an $\mathsf{U}$ operator without compromising on
succinctness.. $T$ denotes the time stamp of the position where the formula is
evaluated. The construct $x.\varphi$ is called a _freeze quantifier_ , which
stores in $x$, the time stamp of the current position and then evaluates
$\varphi$. $T-x\in I$ is a constraint on the clock variable $x$, which checks
if the time elapsed since the time $x$ was frozen is in the interval $I$.
Notice that, in aid of brevity, we will typically abbreviate subformula
$T-x\in I$ to $x\in I$. For a timed word
$\rho=(\sigma_{1},\tau_{1})\dots(\sigma_{n},\tau_{n})$, $i\in dom(\rho)$ and a
TPTL formula $\varphi$, we define the satisfiability
$\rho,i,\nu\models\varphi$ at a position $i$ of $\rho$, given a valuation
$\nu$ of the clock variables.

$\displaystyle\rho,i,\nu$ $\displaystyle\;\;\;\models$ $\displaystyle
a\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$ $\displaystyle\iff$
$\displaystyle\sigma_{i}=a,\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$
$\displaystyle\rho,i,\nu$ $\displaystyle\;\;\;\models$ $\displaystyle
x.\varphi\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$
$\displaystyle\iff$
$\displaystyle\rho,i,\nu[x\leftarrow\tau_{i}]\models\varphi,\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$
$\displaystyle\rho,i,\nu$ $\displaystyle\;\;\;\models$ $\displaystyle{T-x\in
I}\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$ $\displaystyle\iff$
$\displaystyle\tau_{i}-\nu(x)\in
I,\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$
$\displaystyle\rho,i,\nu$ $\displaystyle\;\;\;\models$
$\displaystyle\mathsf{G}\varphi\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$
$\displaystyle\iff$ $\displaystyle\forall j>i,\rho,j,\nu\ \models\
\varphi,\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$
$\displaystyle\rho,i,\nu$ $\displaystyle\;\;\;\models$
$\displaystyle\varphi_{1}\mathsf{U}\varphi_{2}\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$
$\displaystyle\iff$ $\displaystyle\exists j>i,\rho,j\
\models\varphi_{2},\text{ and }\forall i<k<j,\rho,k\ \models\ \varphi_{1}.$

The $\mathsf{F}$ and $\mathsf{Next}$ operator is defined in terms of
$\mathsf{U}$; $\mathsf{F}\phi=\top\mathsf{U}\phi$ and
$\mathsf{Next}\phi=\bot\mathsf{U}\phi$. $\mathbf{0}$ denotes a valuation that
maps every variable to $0$. A TPTL formula $\varphi$ is said to be closed iff
every variable $x$ used in the timing constraint is quantified (or bound) by a
freeze quantifier. A formula that is not closed is _open_. Similarly, in any
formula $\varphi$, a constraint of the form $x\in I$ is open if $x$ is not
quantified. For example, $x.y.(a\mathsf{U}(b\wedge x\in(1,2)\wedge
y\in(2,3)))$ is a closed formula while
$x.(a\wedge\underline{y\in(2,3)})\mathsf{U}y.(b\wedge x\in(1,2))$ is open as
the clock $y$ used in the underlined clock constraint is not in the scope of a
freeze quantifier for $y$. Moreover, the underlined constraint
$\underline{y\in(2,3)})$ is an open constraint. Notice that open constraints
appear only (and necessarily) in open formulae. Satisfaction of closed
formulae is independent of the clock valuation; that is, if $\psi$ is a closed
formula, then for a timed word $\rho$ and a position $i$ in $\rho$, either for
every valuation $\nu$, $\rho,i,\nu\models\psi$; or for every valuation $\nu$,
$\rho,i,\nu\not\models\psi$. Hence, for a closed formula $\psi$, we drop the
valuation $\nu$ while evaluating satisfaction, and simply write $\rho,i\
\models\psi$. As an example, the closed formula
$\varphi{=}x.(a\mathsf{U}(b\mathsf{U}(c\wedge x{\in}[1,2])))$ is satisfied by
the timed word $\rho{=}(a,0)(a,0.2)(b,1.1)(b,1.9)(c,1.91)(c,2.1)$ since
$\rho,1\models\varphi$. The word
$\rho^{\prime}=(a,0)(a,0.3)(b,1.4)(c,2.1)(c,2.5)$ does not satisfy $\varphi$.
However, $\rho^{\prime},2\models\varphi$: if we start from the second position
of $\rho^{\prime}$, the value 0.3 is stored in $x$ by the freeze quantifier,
and when we reach the position 4 of $\rho^{\prime}$ with $\tau_{4}=2.1$ we
obtain $T-x=2.1-0.3\in[1,2]$.

Given any closed TPTL formula $\varphi$, its language,
$L(\varphi)=\\{\rho|\rho,1\models\varphi\\}$, is set of all the timed words
satisfying it. We say that a closed formula $\varphi$ is satisfiable iff
$L(\varphi)\neq\emptyset$.
Size of a TPTL formula. Given a TPTL formula $\varphi$, the size of $\varphi$
denoted by $|\varphi|$ is defined as $B+M+C$ where $B$ is the number of
Boolean operators in $\varphi$, $M$ is the number of temporal modalities
($\mathsf{G},\mathsf{U},\mathsf{Next},\mathsf{F}$) and freeze quantifiers in
$\varphi$, and $C$ is obtained by multiplying the number of time constraints
in $\varphi$ with $2\times(\lfloor\log(c_{max})\rfloor+1)$ where $c_{max}$ is
the maximal constant appearing in the time constraints of $\varphi$. For
example, for $\varphi=x.(a\wedge bU(c\vee x\leq(1,2)))$,
$|\varphi|=2+2+2\times(1+1)=8$ as it contains two boolean operators, one
temporal modality, one freeze quantifier and one timing constraint where
$c_{max}=2$.

The subclass of TPTL that uses only k-clock variables is known as k-TPTL. By
[10] [25], satisfiability checking for 1-TPTL is decidable over finite models
but non-primitive recursive hard, and undecidable over infinite models.
Satisfiability checking for 2-TPTL is undecidable over both finite and
infinite models [6] [17]. Towards the main contribution of this paper, we
propose a ‘non-punctual’ fragment of TPTL with unilateral intervals, called
$\text{TPTL}^{0,\infty}$, and show that its satisfiability checking is
decidable with multiple variables over both finite and infinite timed words
(PSpace -complete). Further, 1-$\text{TPTL}^{0,\infty}$ is already more
expressive than MITL, which has an ExpSpace -complete satisfiability checking.

###  2.1 Multi-clock TPTL with unilateral intervals : $\text{TPTL}^{0,\infty}$

We say that a formula $\varphi$ is of the type $\leq$ ($\geq$), iff all the
intervals appearing in the open constraints of $\varphi$ are in
$\mathcal{I}_{\mathsf{int}}^{0}$ ($\mathcal{I}_{\mathsf{int}}^{\infty}$).
Notice that a closed formula belongs to both types $\leq$ and $\geq$. There
are open formulae that are neither of type $\leq$ nor $\geq$. A TPTL formula
$\varphi$ in negation normal form is a $\text{TPTL}^{0,\infty}$ formula iff
every subformula of $\varphi$ is either of the type $\leq$ or $\geq$. For
example, $x.y.(a\mathsf{U}(b\mathsf{U}(c\wedge x<3\wedge y\leq 2\wedge
x.(\mathsf{Next}(c\wedge x>1)))))$ is a $\text{TPTL}^{0,\infty}$ formula since
there is no subformula that doesn’t belong to either types $\leq$ or $\geq$.
However, $x.y.(a\mathsf{U}(b\wedge x\leq 3\wedge y\geq 5))$ is not
$\text{TPTL}^{0,\infty}$, since $(b\wedge x\leq 3\wedge y\geq 5)$ is of
neither type $\leq$ or $\geq$ as the open constraints within this subformula
use both left-sided as well as right-sided intervals. This restriction is
inspired by that of $\text{MITL}^{0,\infty}$. Any $\text{MITL}^{0,\infty}$
formula can be expressed in $1$-$\text{TPTL}^{0,\infty}$ by applying the same
reduction from MITL to $1$-TPTL (see Remark 4.1). Next, we introduce
alternating timed automata which are useful in proving the main result, i.e.,
Theorem 3.1.

####  2.1.1 Alternating Timed Automata

An Alternating Timed Automata (ATA) is a 7-tuple
$\mathcal{A}=(Q,\Sigma,\delta,q_{0},\mathsf{Q_{acc}},X,\mathcal{G})$, where,
$Q$ is a finite set of locations, $X$ is a finite set of clock variables,
$\mathcal{G}$ is a finite set of guards of the form $x\in I$ where
$I\in\mathcal{I}_{\mathsf{int}}$ and $x\in X$, $\delta$ is a transition
function, $q_{0}\in Q$ is the initial location, and $\mathsf{Q_{acc}}\subseteq
Q$ is a set of accepting locations. The transition function is defined as
$\delta:Q\times\Sigma\mapsto\Phi(Q,\mathcal{G})$ where $\Phi(Q,\mathcal{G})$
is defined by the grammar
$\varphi::=\top|\bot|\varphi_{1}\wedge\varphi_{2}|\varphi_{1}\vee\varphi_{2}|q|x\in
I|Y.q$ with $q\in Q$, $x\in X$, $(x\in I)$ is a guard in $\mathcal{G}$,
$Y\subseteq X$, $Y$ is not the empty set. $\top,\bot$ respectively denote
$\mathsf{True}$ and $\mathsf{False}$. $Y.q$ is a _binding construct_ which
resets all clocks in $Y$ to zero after taking the transition.

Figure 1: Graphical Representation of ATA transitions.

Let $p,q\in Q$ and $Y\subseteq X$. We say that there is a transition from $p$
to $q$ iff $q$ appears in $\delta(p,b)$ for some $b\in\Sigma$. We say that
there is a strong reset transition, non-reset transition, and a Y-reset
transition from location $p$ to $q$ iff for some $b\in\Sigma$, $X.q$, $q$, and
$Y.q$, respectively, appears in $\delta(p,b)$ for some $b\in\Sigma$. The
1-clock restriction of ATA has been considered in [24] and [20].
Evaluation of $\Phi(Q,\mathcal{G})$. Given an ATA $\mathcal{A}$, a state $s$
is defined as a pair consisting of a location and a valuation over $X$, i.e.,
$s\in Q\times\mathcal{V}_{X}$. A configuration $C$ of an ATA is a finite set
of states. Let $S$ and $\mathcal{C}$ respectively denote the set of all states
and configurations of $\mathbb{A}$. A configuration $C$ and a clock valuation
$\nu$ define a Boolean valuation for $\Phi(Q,\mathcal{G})$ as follows:
$C\models_{\nu}q$ iff $(q,\nu)\in C$, $C\models_{\nu}Y.q$ iff $(q,\nu)\in C$,
and $\forall x\in Y.\nu(x)=0,$ $C\models_{\nu}x\in I$ iff $\nu(x)\in I$,
$C\models_{\nu}\varphi_{1}\wedge\varphi_{2}$ iff
$C\models_{\nu}\varphi_{1}\wedge C\models_{\nu}\varphi_{2},$
$C\models_{\nu}\top$ for all $C\in\mathcal{C}$,
$C\models_{\nu}\varphi_{1}\vee\varphi_{2}$ iff $C\models_{\nu}\varphi_{1}\vee
C\models_{\nu}\varphi_{2}.$
Finally, $C\not\models_{\nu}\bot$ for all possible configurations. We say that
$C$ is a minimal model for $\varphi\in\Phi(Q,\mathcal{G})$ with respect to
$\nu$ (denoted by $C\models^{\mathsf{min}}_{\nu}\varphi$) iff
$C\models_{\nu}\varphi$ and no proper subset $C^{\prime}$ of $C$ is such that
$C^{\prime}\models_{\nu}\varphi$. We represent the transition function of ATA
(and hence by extension the ATA) graphically as shown in figure 1.

Semantics of ATA. Given a state $s=(q,\nu)$, a time delay
$t\in\mathbb{R}_{\geq 0}$ and $a\in\Sigma$, the successors of $s=(q,\nu)$ on
time delay $t$ followed by $a$ is any configuration $C$ such that
$C\models^{\mathsf{min}}_{\nu+t}\delta(q,a)$.
$\mathsf{Succ}_{\mathcal{A}}^{st}(s,t,a)$ is the set of all such successors.
The notion of a successor is extended to a configuration in a straightforward
manner. A configuration $C^{\prime}$ is a successor of configuration
$C=\\{s_{1},s_{2},\ldots s_{k}\\}$ on time delay $t$ and $a\in\Sigma$ (denoted
by $C\xrightarrow{(t,a)}_{\mathcal{A}}C^{\prime}$) iff
$C^{\prime}=C_{1}\cup\ldots\cup C_{k}$ such that $\forall 1\leq i\leq
k,C_{i}\in\mathsf{Succ}_{\mathcal{A}}^{st}(s_{i},t,a)$. We denote by
$\mathsf{Succ}_{\delta}(C,t,a)$ set of all such successors $C^{\prime}$.

The initial configuration is defined by $C_{init}=\\{(q_{0},\mathbf{0})\\}$,
and a configuration $C$ is accepting iff for all $s\in C$, $s$ is an accepting
state, that is $s=(q,\nu)$ for $q\in\mathsf{Q_{acc}}$. Let $\mathcal{C}_{acc}$
be the set of all the accepting configurations. Hence, the empty configuration
is an accepting configuration. We define the semantics of ATA using a Labelled
Transition System (LTS). An LTS is a 5-tuple
$T=(S,s_{0},\Sigma,\delta,S_{f})$, where $S$ is a finite or infinite set of
states, $s_{0}\in S$ is the initial state, $\Sigma$ is set of symbols,
$\delta:S\times\Sigma\times S$ is a transition relation, and $S_{f}\subseteq
S$ is a set of final states. A (finite) run $\mathbf{R}$ of an LTS is a
(finite) sequence of the form $s_{0},a_{1},s_{1},a_{2},s_{2},a_{3}\ldots$
where $s_{1},s_{2},\ldots\in S$ are states of $T$, and $a_{1},a_{2},\ldots$
are symbols in $\Sigma$ such that for all $i>0$,
$s_{i}\in\delta(s_{i-1},a_{i})$. We say that a run
$R=s_{0},a_{1},s_{1},a_{2},s_{2},a_{3}\ldots$ visits a state $s$ (or visits a
set of states $S^{\prime}$) iff the sequence $R$ contains $s$ (or contains
states in $S^{\prime}$). A run is said to be accepting iff it ends in some
state $s\in S_{f}$. Similarly, an infinite run is said to be Büchi accepting
iff it visits $S_{f}$ infinitely often.

Runs of $\mathcal{A}=(Q,\Sigma,\delta,q_{0},\mathsf{Q_{acc}},X,\mathcal{G})$
starting from a configuration $C$ are the runs of LTS
$TS(\mathcal{A},C)=(\mathcal{C},C,\mathbb{R}_{\geq
0}\times\Sigma,\rightarrow,$ $\mathcal{C}_{acc}$ $)$. Notice that the states
of LTS $TS(\mathcal{A},C)$ are configurations of $\mathcal{A}$ (i.e., a set of
states of $\mathcal{A}$ and not just the states of $\mathcal{A}$). Let
$\mathbf{\rho}=(a_{1},\tau_{1})(a_{2},\tau_{2})\ldots$ be any timed word over
$\Sigma$. We say that a run $R=C,(t_{1},a_{1}),C_{1},(t_{2},a_{2})\ldots$ is
produced by $\mathcal{A}$ on $\mathbf{\rho}$ starting from a configuration $C$
iff $C\xrightarrow{(t_{1},a_{1})}C_{1}\xrightarrow{(t_{2},a_{2})}C_{2}\ldots$
where $t_{i}=\tau_{i}-\tau_{i-1}$ for $i>0$ and $\tau_{0}=0$. Let
$\mathcal{A}(\mathbf{\rho},C)$ be the set of all the runs produced by
$\mathcal{A}$ on $\mathbf{\rho}$, starting from the configuration $C$. We
denote $TS(\mathcal{A},C_{init})$ as simply $TS(\mathcal{A})$. A run starting
from the initial configuration $C_{init}$ is called an initialized run. We
denote $\mathcal{A}(\mathbf{\rho},C_{init})$ by $\mathcal{A}(\mathbf{\rho})$.
$\mathbf{\rho},i$ is said to be accepted (Büchi accepted) by $\mathcal{A}$
starting with configuration $C$, denoted by
$\mathbf{\rho},i\models\mathcal{A},C$, iff there exists a run in
$\mathcal{A}(\mathbf{\rho}[i..],C)$ accepted (Büchi accepted) by
$TS(\mathcal{A})$ (i.e., simulating $\mathcal{A}$ on the suffix of $\rho$
starting at position $i$ we obtain an accepting run). We say that
$\mathbf{\rho}$ is accepted by $\mathcal{A}$ iff $\mathbf{\rho},1\models
C_{init}$.

We define the finite (infinite) language of $\mathcal{A}$, denoted by
$L_{fin}(\mathcal{A})$ ($L_{inf}(\mathcal{A})$), as a set of all the finite
(infinite) timed words accepted by $\mathcal{A}$. When clear from context, we
drop the subscript in $L_{fin}$ and $L_{inf}$.

Non-Deterministic Timed Automata (NTA) is a subclass of ATA where
$\Phi(Q,\mathcal{G})$ is restricted to be in disjunctive normal form (DNF),
where each disjunct is of the form $(q\wedge x\in I)$ or $(X^{\prime}.q\wedge
x\in I)$. Hence, for any $s\in S$, $t\geq 0$, $a\in\Sigma$ and any
configuration $C\in\mathsf{Succ}_{\delta}^{st}(s,t,a)$ implies $C\leq 1$.

We call the ATA $\mathcal{A}$ a Very Weak ATA (VWATA) iff (1) there is a
partial order $\ll_{\mathcal{A}}\subseteq Q\times Q$ such that there is a
transition from $p$ to $q$ iff $q\ll_{\mathcal{A}}p$, (2) all the self-loop
transitions (transitions entering and exiting into the same location) are non-
reset transitions, and (3) For every location $q$, there is at most one
location $p\neq q$ such that there is a transition from $p$ to $q$. Moreover,
all the transitions from $p$ to $q$ reset the same set of clocks. This makes
the transition diagram of VWATA a tree and not a DAG (excluding self-loops).

######  Remark 2.1.

In the literature, VWATA (also called Partially-Ordered Alternating Timed
Automata in [19]) and their corresponding untimed version [9][31](also called
as Linear [21], Linear-Weak [11], 1-Weak [32], and Self-Loop [33] Alternating
Automata) are required to satisfy only conditions (1) and (2). It can be shown
that condition (3) does not affect the expressiveness of the machine. We
notice that this version of VWATA is enough to express TPTL formulae
efficiently (linear in the size of TPTL formulae). In case of translation from
TPTL to VWATA satisfying condition (3) the number of locations in the
resulting ATA will depend on the size of the formula tree. On the other hand,
the total number of locations depends on the formula DAG on similar
translation from TPTL to VWATA satisfying only (1) and (2) making it
exponentially more succinct. Hence, we consider a less succinct representation
(i.e., tree or string, which is standard) of TPTL formulae for computing its
size as compared to the DAG representation.

####  2.1.2 ATA with Unilateral Intervals: ${\text{ATA}^{0,\infty}}$

Similar to the unilateral version of TPTL (i.e. $\text{TPTL}^{0,\infty}$), we
define a unilateral version of ATA as follows. Let
$\mathcal{A}=(Q,\Sigma,\delta,q_{0},\mathsf{Q_{acc}},X,\mathcal{G})$ be any
ATA. Let $\mathcal{G}^{\geq}$ ($\mathcal{G}^{\leq}$) be the subset of
$\mathcal{G}$ containing all the guards of the form $x\in I$ where
$I\in\mathcal{I}_{\mathsf{int}}^{\infty}$
($I\in\mathcal{I}_{\mathsf{int}}^{0}$). $\mathcal{A}$ is said to be an
${\text{ATA}^{0,\infty}}$ iff, $Q$ can be partitioned into $\mathsf{Q^{\geq}}$
and $\mathsf{Q^{\leq}}$ any transition exiting from any location
$q\in\mathsf{Q^{\geq}}$ ($q\in\mathsf{Q^{\leq}}$) is guarded by a guard in
$\mathcal{G}^{\geq}$ ($\mathcal{G}^{\leq}$), and any transition from any
location in $\mathsf{Q^{\geq}}$ to a location in $\mathsf{Q^{\leq}}$, or vice-
versa, is a strong reset transition. $\mathcal{A}$ is said to be
${\text{VWATA}^{0,\infty}}$ iff it is also a VWATA. From this point onwards,
for any set of locations $Q$ of any ${\text{ATA}^{0,\infty}}$,
$\mathsf{Q^{\geq}}$ and $\mathsf{Q^{\leq}}$ will denote partitions of $Q$
satisfying the above condition.

##  3 Satisfiability Checking for $\text{TPTL}^{0,\infty}$

This section is dedicated to proving the following main theorem of this paper.

######  Theorem 3.1.

PSpace hardness follows from the hardness of satisfiability checking of the
sublogics $\mathsf{LTL}$ and $\text{MITL}^{0,\infty}$ (see section 4.1 for the
details on $\text{MITL}^{0,\infty}$). To show membership in PSpace we propose
the following steps: (1) We reduce any given $k$-$\text{TPTL}^{0,\infty}$
formula $\varphi$, to an equivalent ${\text{VWATA}^{0,\infty}}$,
$\mathcal{A}$, with $k$ clock variables and at most $|\varphi|+1$ number of
locations. (2) We give a novel on-the-fly construction from any
${\text{VWATA}^{0,\infty}}$ to simulation equivalent NTA $\mathbb{A}$ with
exponential blow-up in the number of locations and polynomial blow-up in the
number of clocks. Hence, the region automata corresponding to $\mathbb{A}$ has
at most exponentially many states, and thus each state can be represented in
polynomial space.

######  Remark 3.2.

Notice that while the reduction from ${\text{VWATA}^{0,\infty}}$ to timed
automata results in an exponential blow-up in the number of locations we can
directly construct the region automaton of the corresponding timed automaton
on-the-fly making sure that we need at most polynomial space to solve its
emptiness checking problem.

We demonstrate our steps of construction using a running example and defer the
formal constructions to the Appendices A, D. In our running example, we start
with the given formula $\varphi=\mathsf{G}(\neg a\vee x.(\mathsf{F}(a\wedge
T-x\leq 2\wedge y.\mathsf{Next}(b\wedge T-x\leq 3\wedge T-y\leq 2)))$.

###  3.1 $\text{TPTL}^{0,\infty}$ to ${\text{VWATA}^{0,\infty}}$

Figure 2:  ${\text{VWATA}^{0,\infty}}$ equivalent to $\varphi$. Location
$q_{i}$ corresponds to the subformula $\varphi_{i}$ :
$\mathbf{\rho},i,\nu\models\varphi_{i}$ iff
$\mathbf{\rho},i\models(q_{i},\nu)$.

This step is a straightforward multi-clock generalization of translation from
MTL and $1$-TPTL to 1-ATA in [24] and [10], respectively, (which are
themselves timed generalization of reduction from $\mathsf{LTL}$ to Very Weak
Alternating Automata [34] [9]). We give the reduction in Appendix A for
completeness. The proof of equivalence is identical to that in [24] and [10]
resulting in the following Theorem 3.3. We give the
${\text{VWATA}^{0,\infty}}$ corresponding to the formula $\varphi$ of the
running example in Figure 2. Hence, to prove the main theorem it suffices to
show that emptiness checking for ${\text{VWATA}^{0,\infty}}$ is in PSpace
(i.e. Theorem 3.4).

######  Theorem 3.3.

Any $k$ variable TPTL formula $\varphi$ over $\Sigma$ can be reduced to an
equivalent VWATA,
$\mathcal{A}=(Q,2^{\Sigma},\delta,\text{init},\mathsf{Q_{acc}},X,\mathcal{G})$,
with $|X|=k$, $|Q|\leq|\varphi|+1$, and $\mathcal{G}$ is the set of all the
guards appearing in $\varphi$. Moreover, if $\varphi$ is a
$\text{TPTL}^{0,\infty}$ formula, then the $\mathcal{A}$ is
${\text{VWATA}^{0,\infty}}$.

###  3.2 Emptiness Checking for ${\text{VWATA}^{0,\infty}}$

The following theorem is the main technical result.

######  Theorem 3.4.

Emptiness Checking for ${\text{VWATA}^{0,\infty}}$ is in PSpace .

We give a translation from ${\text{VWATA}^{0,\infty}}$
$\mathcal{A}=(Q,\Sigma,\delta,q_{0},\mathsf{Q_{acc}},X,\mathcal{G})$ to an
equivalent timed automaton,
${\mathbb{A}=(\mathcal{Q},\Sigma,\Delta,\mathsf{q}_{0},\mathcal{Q}_{acc},\mathcal{X},\mathcal{G})}$,
such that the transition system of $\mathcal{A}$ (i.e., $TS(\mathcal{A})$) is
simulation equivalent to that of $\mathbb{A}$ (i.e., $TS(\mathbb{A})$). Hence,
by the Proposition 3.5, ${L(\mathcal{A})=L(\mathbb{A})}$.

Moreover, $\mathcal{Q}=O(2^{Poly(Q)})$ and $|\mathcal{X}|=|X|\times|Q|$.
Hence, the number of states in the corresponding region automaton is
exponential to the size of $\mathcal{A}$ (i.e.
$O(2^{Poly(|Q|,|X|)})\times(2\times c_{max}+1)$ where $c_{max}$ is the maximum
constant used in the constraints appearing in $\mathcal{G}$). Hence, each
state of the region automata (when encoded in binary) can be represented in
polynomial space proving membership in PSpace . We prove the above by giving a
translation from ${\text{VWATA}^{0,\infty}}$ to timed automata with polynomial
blowup in the number of clocks and exponential blowup in the set of locations.
As a side-effect, we also show that emptiness checking for
1-${\text{ATA}^{0,\infty}}$ is in PSpace (using the same construction)
generalizing the result of [16]. We first briefly discuss the concept of
simulation relations and preorder.

####  3.2.1 Simulation Relations and Preorder

We fix a pair of labeled transition system,
$TS^{1}=(S^{1},s^{1}_{0},\Sigma,\delta^{1},S_{f}^{1})$ and
$TS^{2}=(S^{2},s^{2}_{0},\Sigma,\delta^{2},S^{2}_{f})$. A relation
${\preceq}\subseteq S^{1}\times S^{2}$ is a simulation relation iff (1)
$s^{1}_{0}{\preceq}s^{2}_{0}$, (2) for every $s_{1}\preceq s_{2}$, (2.1) if
$s_{1}\in S^{1}_{f}$ then $s_{2}\in S^{2}_{f}$, and (2.2) for every
$a\in\Sigma$, for every $s_{1}^{\prime}\in\delta(s_{1},a)$ there exists
$s_{2}^{\prime}\in\delta(s_{2},a)$ such that $s_{1}^{\prime}\preceq
s_{2}^{\prime}$. If $s_{1}\preceq s_{2}$, then we say that $s_{2}$ simulates
$s_{1}$ wrt $\preceq$.

Let $S=S^{1}\cup S^{2}$. Notice that simulation relations are closed under
union. Hence, there is a unique maximal simulation relation, ${\leq}\subseteq
S\times S$, which is the union of all the simulation relations amongst states
of $TS^{1}$ and $TS^{2}$ (i.e. all the simulation relations between $TS^{1}$
and itself, between $TS^{2}$ and itself, and from $TS^{1}$ to $TS^{2}$ and
vice-versa). Notice that $\leq$ is a preorder relation (i.e. reflexive and
transitive), and hence also called simulation preorder. Similarly, simulation
equivalence relation, $\cong$ is defined as the largest symmetric subset of
simulation preorder, $\leq$. I.e., $s\cong s^{\prime}$ iff $s\leq s^{\prime}$
and $s^{\prime}\leq s$. Hence, it is clear that $\cong$ is an equivalence
relation. If $s\leq s^{\prime}$ we say that $s^{\prime}$ simulates $s$. Recall
that the states of $TS(\mathcal{A},C)$ for any ATA $\mathcal{A}$ and its
configuration $C$ are configurations of $\mathcal{A}$. The following
Proposition is then straightforward.

######  Proposition 3.5.

Let $\mathcal{A}$ and $\mathcal{A}^{\prime}$ be any ATA, and
$s_{0},s^{\prime}_{0}$ be their initial states, respectively.
$TS(\mathcal{A},\\{s\\})\leq TS(\mathcal{A}^{\prime},\\{s^{\prime}\\})$
implies $L_{fin}(\mathcal{A})\subseteq L_{fin}(\mathcal{A}^{\prime})$ and
$L_{inf}(\mathcal{A})\subseteq L_{inf}(\mathcal{A}^{\prime})$. Hence,
$TS(\mathcal{A},\\{s\\})\cong TS(\mathcal{A}^{\prime},\\{s^{\prime}\\})$
implies $L_{fin}(\mathcal{A})=L_{fin}(\mathcal{A}^{\prime})$ and
$L_{inf}(\mathcal{A})=L_{inf}(\mathcal{A}^{\prime})$

We fix an ATA
$\mathcal{A}=(Q,\Sigma,\delta,q_{0},\mathsf{Q_{acc}},X,\mathcal{G})$. Let $C$
and $C^{\prime}$ be arbitrary configurations of $\mathcal{A}$. Let
$\leq_{\mathcal{A}}$, $\cong_{\mathcal{A}}$ be the simulation preorder and
simulation equivalence amongst configurations of $\mathcal{A}$. That is,
$C\leq_{\mathcal{A}}C^{\prime}$ iff $C^{\prime}$ simulates $C$, and
$C\cong_{\mathcal{A}}C^{\prime}$ iff $C$ is simulation equivalent to
$C^{\prime}$ in $TS(A)$, the transition system corresponding to ATA
$\mathcal{A}$. Then, by Proposition 3.5:

######  Remark 3.6.

For any configuration $C$ and $C^{\prime}$ of $A$,
$C\leq_{\mathcal{A}}C^{\prime}$ implies $L(\mathcal{A},C)\subseteq
L(\mathcal{A},C^{\prime})$ and $C\cong_{\mathcal{A}}C^{\prime}$ implies
$L(\mathcal{A},C)=L(\mathcal{A},C^{\prime})$.

######  Remark 3.7.

$C\supseteq C^{\prime}$ implies $C\leq_{\mathcal{A}}C^{\prime}$. Hence, for
any timed word $\rho$, if $\rho,i\models\mathcal{A},C$ then
$\rho,i\models\mathcal{A},C^{\prime}$. Intuitively, the additional states in
$C$ (which are not appearing in $C^{\prime}$) impose extra obligations in
addition to that imposed by states common in both $C$ and $C^{\prime}$ which
makes reaching the accepting configuration (hence accepting a timed word)
harder from $C$.

######  Proof 3.8 (Proof of Remark 8).

We show that $\supseteq$ is a simulation relation. That is,
$C\textquoteright\subseteq C$ (or $C\supseteq C\textquoteright$) implies
$C\leq_{\mathcal{A}}C\textquoteright$. We just need to prove that $\supseteq$
indeed satisfies condition 2 (condition 1 is trivially satisfied) of the
simulation relation. Notice that the set of accepting configurations is
downward closed. That is, for any accepting configuration $D$ any of its
subset $D\textquoteright$ is accepting (by definition of accepting
configuration). Hence, $\supseteq$ satisfies condition 2.1.

Wlog, let $C=\\{s_{1},\ldots s_{n}\\}$ and $C\textquoteright=\\{s_{1},\ldots
s_{m}\\}$ for some $m\leq n$. For any $(t,a)\in\mathbb{R}\times\Sigma$, by
definition, any $C\xrightarrow{(t,a)}D$ iff $D=D_{1}\cup D_{2}\ldots D_{n}$
where $D_{i}$ is some successor of $s_{i}$ on $(t,a)$. Similarly,
$C^{\prime}\xrightarrow{(t,a)}D^{\prime}iffD\textquoteright=D_{1}\cup
D_{2}\ldots D_{m}$ where $D_{i}$ is some successor of $s_{i}$ on $(t,a)$.
Hence, For any $(t,a)\in\mathbb{R}\times\Sigma$, for any
$C\xrightarrow{(t,a)}D$ there exists a
$C^{\prime}\xrightarrow{(t,a)}D^{\prime}$ such that $D\supseteq
D\textquoteright$ (for any state $s_{i}\in C\cap C\textquoteright$ , just
choose the same successor of $s_{i}$ which was used in $D$ to construct
$D\textquoteright$). Hence, for any successor $C$, we have a successor of
$C\textquoteright$ which is a subset of that of $C$. Hence, $\supseteq$
satisfies condition 2.2.

Intuitively, these extra states $s_{m+1}\ldots s_{n}$ will generate extra
states in the successor configurations, which will make reaching an accepting
configuration harder from $C$ (and its successors) as compared to
$C\textquoteright$ (and its successors),

######  Remark 3.9.

If $D^{\prime}\subseteq C$ and $D\leq_{\mathcal{A}}D^{\prime}$, then
$(C\setminus D^{\prime})\cup D\leq_{\mathcal{A}}C$. In other words, we can
replace the states in $D^{\prime}$ with that in $D$ in any configuration $C$,
and get a configuration that is simulated by $C$. Hence,
$L(\mathcal{A},(C\setminus D^{\prime})\cup D)\subseteq L(\mathcal{A},C)$.

######  Proof 3.10 (Proof of Remark 9).

Consider a relation $\mathcal{R}$ amongst configurations of $A$ such that
$E\leavevmode\nobreak\ {\mathcal{R}}\leavevmode\nobreak\ E^{\prime}$ iff
$E^{\prime}=E_{1}\cup E_{2}$ such that $E\leq_{\mathcal{A}}E_{1}$ and
$E\leq_{\mathcal{A}}E_{2}$. We first show that $\mathcal{R}$ is a simulation
relation. We need to show that $\mathcal{R}$ satisfies condition (2.2) as it
trivially satisfies condition (2.1). Let $E\leavevmode\nobreak\
\mathcal{R}\leavevmode\nobreak\ E^{\prime}$ and $E^{\prime}=E_{1}\cup E_{2}$
such that $E\leq_{\mathcal{A}}E_{1}$ and $E\leq_{\mathcal{A}}E_{2}$. Let
$E_{2}^{\prime}=E_{2}\setminus E_{1}$. Then
$E\leq_{\mathcal{A}}E_{2}\leq_{\mathcal{A}}E_{2}^{\prime}$ (by remark 3.7). By
definition of simulation preorder, for any $E\xrightarrow{(t,a)}F$ there
exists (1)$E_{1}\xrightarrow{(t,a)}F_{1}$ and
(2)$E_{2}^{\prime}\xrightarrow{(t,a)}F_{2}$ such that
$F\leq_{\mathcal{A}}F_{1}$ and $F\leq_{\mathcal{A}}F_{2}$. Let
$F^{\prime}=F_{1}\cup F_{2}$. By semantics ATA, (1) and (2) imply
$E^{\prime}\xrightarrow{(t,a)}F^{\prime}$. Moreover, by definition of
$\mathcal{R}$, $F\leavevmode\nobreak\ \mathcal{R}\leavevmode\nobreak\
F^{\prime}$ if $E\leavevmode\nobreak\ \mathcal{R}\leavevmode\nobreak\
E^{\prime}$. Hence, for any $E\leavevmode\nobreak\
\mathcal{R}\leavevmode\nobreak\ E^{\prime}$, and $E\xrightarrow{(t,a)}F$ there
exists $E^{\prime}\xrightarrow{((t,a)}F^{\prime}$ such that
$F\leavevmode\nobreak\ \mathcal{R}\leavevmode\nobreak\ F^{\prime}$. Hence,
$\mathcal{R}$ satisfies condition 2.2.

Given $D^{\prime}\leq_{\mathcal{A}}D$. Hence, by remark 3.7, $((C\setminus
D^{\prime})\cup D)\leq_{\mathcal{A}}(C\setminus D^{\prime})$ and $(C\setminus
D^{\prime})\cup D\leq_{\mathcal{A}}D\leq_{\mathcal{A}}D^{\prime}$. Hence,
$(C\setminus D^{\prime})\cup D\leavevmode\nobreak\
\mathcal{R}\leavevmode\nobreak\ ((C\setminus D^{\prime})\cup D^{\prime})$.
Hence, $((C\setminus D^{\prime})\cup D)\leq_{\mathcal{A}}C$.

Both the above remarks imply the following Proposition. We abuse the notation
by writing $\\{s\\}\leq_{\mathcal{A}}\\{s^{\prime}\\}$ as
$s\leq_{\mathcal{A}}s^{\prime}$.

######  Proposition 3.11.

If $s,s^{\prime}\in C$ and $s\leq_{\mathcal{A}}s^{\prime}$ then
$C\setminus\\{s^{\prime}\\}\cong_{\mathcal{A}}C$.

######  Proof 3.12.

Notice that
$(C\setminus\\{s^{\prime}\\})\cup\\{s\\}=C\setminus\\{s^{\prime}\\}$. Hence,
by Remark 3.9, $(C\setminus\\{s^{\prime}\\})\leq_{\mathcal{A}}C$. By Remark
3.7, $C\leq_{\mathcal{A}}C\setminus\\{s^{\prime}\\}$. Hence proved.

We use the above Proposition 3.11 and Lemma 3.16 (which holds for
${\text{VWATA}^{0,\infty}}$ and 1-${\text{ATA}^{0,\infty}}$) to bound the
cardinality of the configuration preserving simulation equivalence. This bound
on the cardinality of configurations will imply that we need to remember only
a bounded number of clock values to simulate these configurations. Hence, we
use this bound on the cardinality of the configurations to bound the number of
clock copies required while constructing the required timed automaton.

###  3.3 Bounding Cardinality of Configurations

####  3.3.1 Intuition

We now discuss the intuition for the decidability of
${\text{VWATA}^{0,\infty}}$. The main reason for the undecidability of ATA or
VWATA is due to the unboundedness of the configuration size. That is, the
cardinality of the configurations could depend on the length of the timed word
prefix read so far. Hence, we need to keep track of an unbounded number of
clocks. This happens, because we can reset a clock $x$ in one branch and not
reset $x$ in another branch while taking transitions. This is a result of
transitions containing clauses of the form $(X_{i}.q_{i}\wedge X_{j}.q_{j})$
where $X_{i}\neq X_{j}$ and $X_{i},X_{j}\subseteq X$. That is, we get two
states in the successive configuration each resetting a different set of
clocks. Hence, we need to remember multiple values for clock variables that
are reset in one branch and not in another. In case of
${\text{ATA}^{0,\infty}}$, we observe the following:

  * •

Observation 1 - Let $q\in\mathsf{Q^{\geq}}$. Due to the nature of constraints,
i.e. $x_{i}\in(l,\infty)$, if we have a pair of states
$(q,\nu_{1}),(q,\nu_{2})$ in a configuration $C$, such that
$\nu_{1}\leq\nu_{2}$ (i.e. $\forall x\in X.\nu_{1}(x)\leq\nu_{2}(x)$), then
any timing constraint that is satisfied by $\nu_{1}$ will also be satisfied by
$\nu_{2}$. Hence, any transition that can be taken by $(q,\nu_{1})$ can also
be taken by $(q,\nu_{2})$. Moreover, after taking the same transition (time
delay followed by event-based transition) both $(q,\nu_{1})$ and $(q,\nu_{2})$
get states of the form $(q^{\prime},\nu_{1}^{\prime})$ and
$(q^{\prime},\nu_{2}^{\prime})$, respectively, in their successor
configurations, such that $\nu_{1}^{\prime}\leq\nu_{2}^{\prime}$ if
$q^{\prime}\in\mathsf{Q^{\geq}}$ and
$\nu_{1}^{\prime}=\nu_{2}^{\prime}=\mathbf{0}$ if
$q^{\prime}\in\mathsf{Q^{\leq}}$. Thus,
$(q,\nu_{1})\leq_{\mathcal{A}}(q,\nu_{2})$. Hence, by Proposition 3.11, we can
delete $(q,\nu_{2})$ from $C$ preserving simulation equivalence (and hence the
language). A similar argument applies for $q\in\mathsf{Q^{\leq}}$.

  * •

Observation 2 - In 1-ATA, for any pair of valuations $\nu_{1},\nu_{2}$, either
$\nu_{1}\leq\nu_{2}$ or $\nu_{2}\leq\nu_{1}$. Hence, on applying the reduction
using Proposition 3.11 (and discussed in the previous bullet, i.e.,
Observation 1), we will always get a configuration, where each location
appears at most once. Hence, the cardinality of configurations is bounded by
the number of locations.

  * •

Observation 3 - But this is not necessarily the case for multiple clocks. This
is because there could be unboundedly many incomparable valuations. For
example, for 2-clocks $X=\\{x,y\\}$, consider the following family of
configurations parameterized by $m$,
$C_{m}=\\{(q,x=0.1+nk,y=0.9-nk)|n\in\\{0,\ldots,m-1\\}\\}$ and $k=0.8/m$.
$|C_{m}|=m$ and all the clock valuations are incomparable. Notice
$C_{8}=\\{{(q,x=0.1,y=0.9),(q,x=0.2,y=0.8)\ldots(q,x=0.9,y=0.1)}\\}$.
Hence, as the second main step we show that, if $\mathcal{A}$ is a
${\text{VWATA}^{0,\infty}}$, and if we conservatively keep on compressing the
configurations as discussed in Observation 1 (using Proposition 3.11), we will
have boundedly many incomparable clock valuations. To be precise, we will have
at most one copy of each location in the configuration. This is shown in Lemma
3.16 (the main technical Lemma).

####  3.3.2 Bounding Lemma

In this section, we will use the intuition in Observation 1 for constructing a
simulation equivalent transition system for a given
1-${\text{ATA}^{0,\infty}}$ and ${\text{VWATA}^{0,\infty}}$ whose states are
configurations of given ATA $\mathcal{A}$ with bounded cardinality. For the
1-${\text{ATA}^{0,\infty}}$, the intuition in Observation 2 guarantees the
case. For the multi-clock ${\text{VWATA}^{0,\infty}}$, the issues discussed in
Observation 3 must be resolved. This is resolved in Lemma 3.16, the main
contribution of this section.

In what follows, assume $\mathcal{A}$ to be an ${\text{ATA}^{0,\infty}}$. We
define relation $\preceq$ amongst states of $\mathcal{A}$. For
${\sim}\in\\{\leq,\geq\\}$, let $\preceq$ be defined between states such that
$s\preceq s^{\prime}$ iff $s=(q,\nu)$, $s^{\prime}=(q,\nu^{\prime})$, and if
$q\in\mathsf{Q^{\sim}}$ then $\nu^{\prime}\sim\nu$. By Observation 1 we have
Proposition 3.13. The formal proof is in Appendix B.3.

######  Proposition 3.13.

$s\preceq s^{\prime}$ implies $s\leq_{\mathcal{A}}s^{\prime}$.

Given any configuration $C$, we define $\mathsf{Red_{\preceq}}(C)$ as a
configuration $C^{\prime}$ obtained from $C$, by deleting all states
$s^{\prime}\in C^{\prime}$ if there exists a state $s\in C^{\prime}$, such
that $s\neq s^{\prime}$, and $s\preceq s^{\prime}$. Intuitively, we delete
some information from a configuration that is redundant in deciding whether a
timed behaviour from that state is accepted or not.

Let $C_{0}$ be the initial configuration of $\mathcal{A}$. Let
$TS(\mathcal{A})=(\mathcal{C},C_{0},(\mathbb{R}_{\geq
0}\times\Sigma),\rightarrow_{\mathcal{A}})$ be the transition system
corresponding to $\mathcal{A}$. We define $\mathsf{T}_{red}(\mathcal{A})$ as a
transition system
$\mathsf{T}_{red}(\mathcal{A})=(\mathcal{C},C^{\prime}_{0},(\mathbb{R}_{\geq
0}\times\Sigma),\rightarrow_{\mathcal{A},\mathsf{red}})$ such that
$C^{\prime}_{0}=\mathsf{Red_{\preceq}}(C_{0})$ and for any
$C,C^{\prime},D,D^{\prime}\in\mathcal{C}$, $a\in\Sigma$, and
$t\in\mathbb{R}_{\geq 0}$, $C\xrightarrow{(t,a)}_{\mathcal{A}}C^{\prime}$ iff
$D\xrightarrow{(t,a)}_{\mathcal{A},\mathsf{red}}D^{\prime}$,
$D=\mathsf{Red_{\preceq}}(C)$, and
$D^{\prime}=\mathsf{Red_{\preceq}}(C^{\prime})$. By Proposition 3.14,
$TS(\mathcal{A})$ is simulation equivalent to $\mathsf{T}_{red}(\mathcal{A})$.
The following Proposition is implied by Proposition 3.11 and 3.13.

######  Proposition 3.14.

$C\cong_{\mathcal{A}}\mathsf{Red_{\preceq}}(C)$. Hence, $TS(\mathcal{A})$ and
$\mathsf{T}_{red}(\mathcal{A})$ are simulation equivalent.

######  Remark 3.15.

Any run $R^{\prime}$ is a run of $\mathsf{T}_{red}(\mathcal{A})$ iff
$R^{\prime}=\mathsf{Img}(R)$ for some run $R$ of $\mathcal{A}$, where
$\mathsf{Img}(R)$ is defined as follows.
$R={C_{0}\xrightarrow{(t_{0},a_{0})}_{\mathcal{A}}C_{1}\xrightarrow{(t_{1},a_{1})}_{\mathcal{A}}C_{2}\ldots}$,
we define $\mathsf{Img}(R)$ as run
$R^{\prime}=C_{0}^{\prime\prime}\xrightarrow{(t_{0},a_{0})}\leavevmode\nobreak\
\leavevmode\nobreak\
C_{1}^{\prime\prime}\xrightarrow{(t_{1},a_{1})}\leavevmode\nobreak\
\leavevmode\nobreak\ C_{2}^{\prime\prime}\ldots$ where
$C_{0}^{\prime}=C_{0}^{\prime\prime}=\mathsf{Red_{\preceq}}(C_{0})$ and
$\forall i\geq
0.C^{\prime\prime}_{i}\xrightarrow{(t_{i},a_{i})}_{\mathcal{A}}C_{i}^{\prime}$
and $C_{i}^{\prime\prime}=\mathsf{Red_{\preceq}}C^{\prime}_{i}$.

######  Lemma 3.16.

Let $\mathcal{A}=(Q,\Sigma,\delta,q_{0},\mathsf{Q_{acc}},X,\mathcal{G})$ be
either an 1-${\text{ATA}^{0,\infty}}$ or ${\text{VWATA}^{0,\infty}}$ . Let $R$
be a run of $\mathcal{A}$, and
$R^{\prime}=\mathsf{Img}(R)=C_{0}^{\prime\prime}(t_{0},a_{0})C_{1}^{\prime\prime}(t_{1},a_{1})\ldots$,
then for all $i\geq 1$, $C_{i}^{\prime\prime}$ does not contain states
$(q,\nu)$ and $(q,\nu^{\prime})$ where $\nu\neq\nu^{\prime}$ for any $q\in Q$.
In other words, every location $q\in Q$ appears at most once in any
configuration $C_{i}^{\prime\prime}$ for any $i\geq 1$. Hence,
$|C_{i}^{\prime\prime}|\leq|Q|$.

######  Proof 3.17 (Proof (sketch)).

Notice that if $\mathcal{A}$ was 1-${\text{ATA}^{0,\infty}}$, the above
statement is straightforward as no two clock valuations are incomparable in
the case of 1-clock. We now show the same for $\mathcal{A}$ being a multi-
clock ${\text{VWATA}^{0,\infty}}$. We just present intuition behind the proof
idea. A formal proof is proved using DAG semantics of ATA and can be found in
Appendix C. We prove this by contradiction. Assumption 1 - Suppose $k$ is the
smallest number such that $C_{k}^{\prime\prime}$ contains two copies of some
location $q\in Q$. Hence, there exists $\nu$ and $\nu^{\prime}$ such that
$\nu^{\prime}$ is incomparable to $\nu$ and $(q,\nu),(q,\nu^{\prime})\in
C_{k}^{\prime\prime}$. Then, the following cases are possible:
Case 1 - Both $(q,\nu),(q,\nu^{\prime})$ appeared from the same location $p$
in $C^{\prime\prime}_{k-1}$. But, by condition (3) of VWATA, all the
transitions from location $p$ to location $q$ reset the same set of clocks.
Moreover, by assumption 1, location $p$ appears at most once in
$C^{\prime\prime}_{k-1}$. Let $(p,\nu_{p})\in C^{\prime\prime}_{k-1}$. Then
both the clock valuations $\nu$ and $\nu^{\prime}$ should be identical as they
result from the same state $(p,\nu_{p})$ resetting the same set of clocks.
Case 2 - $(q,\nu),(q,\nu^{\prime})$ appeared from distinct location
$(p,\nu_{k-1})$ and $(p^{\prime},\nu^{\prime}_{k-1})$ in
$C^{\prime\prime}_{k-1}$. By condition (3) of VWATA there is at most one
location $q^{\prime}\neq q$ from which there are transitions entering location
$q$. Moreover, all these transitions reset the same set of clocks. Hence, one
of $p$ and $p^{\prime}$ has to be $q$. Wlog $p=q$. It suffices to show that
whenever such a case occurs, the clock valuation of the state that results
from the self-loop (in this case $\nu$) is always greater than or equal to the
valuation from the other (in this case $\nu^{\prime}$) (Statement 1). Hence,
$\nu^{\prime}\leq\nu$ which leads to a contradiction. We just present the
intuition with an example. Let $\rho=(a_{1},\tau_{1}),(a_{2},\tau_{2})$.
Suppose, $(q_{0},\mathbf{0})$ is the initial location of the automaton as
drawn in Figure 3. Let $k=2$. Notice the run in the Figure,
$C_{1}=\\{(q_{0},\nu_{1}),(q_{1},\nu_{1}^{\prime})\\}$ where if $x\in
X^{\prime}$, $\nu_{1}^{\prime}(x)=0\leq\nu_{1}(x)=\tau_{1}$. Else,
$\nu_{1}(x)=\nu_{1}^{\prime}(x)=\tau_{1}$. Similarly,
$C_{2}=\\{(q_{0},\nu_{2}),(q_{1},\nu^{\prime}),(q_{1},\nu)\\}$, where
$(q_{1},\nu)$ results from the self loop and $(q_{1},\nu^{\prime})$ results
from the transition from $q_{0}$. Hence, if $x=X^{\prime}$,
$\nu(x)=0\leq\nu^{\prime}(x)=\tau_{2}-\tau_{1}$. Else,
$\nu_{1}(x)=\nu_{1}^{\prime}(x)=\tau_{2}$. In other words, while reaching both
$(q_{1},\nu)$ and $(q_{1},\nu^{\prime})$ from the initial configuration, the
same set of clock $X^{\prime}$ was reset. But, in the case of the former, they
were reset before the latter. Hence, $\nu$ and $\nu^{\prime}$ agree on all the
clock values not in $X^{\prime}$ and $\nu\geq\nu^{\prime}$ for all the clocks
in $X$. Applying this argument inductively we can prove Statement 1. We
believe it is more intuitive to prove the result using the DAG semantics of
ATA. Hence, the full proof can be found in the Appendix C, where we introduce
the semantics too.

Figure 3: The red and green transitions denote those without resets, and the
blue ones with resets. Notice the paths from $C_{0}$ to $C_{2}$. The Blue-
Green and Red-Blue path reset the same set of clocks $Y$. But the former
resets the clocks earlier (in the first step) as compared to the latter (in
the second step). Hence in the former, clocks in $Y$ get a chance to progress
between $C_{1}$ and $C_{2}$. Moreover, both the paths should agree on the
value of clocks not in $Y$ as they are not reset in both these paths. Hence,
$\nu^{\prime}\leq\nu$.

###  3.4 From ${\text{VWATA}^{0,\infty}}$ to Timed Automata

In this section, we propose an on-the-fly construction from
${\text{VWATA}^{0,\infty}}$ to Timed Automata. The termination relies on Lemma
3.16. The main idea is to bind the number of active clocks using Lemma 3.16.
Given a ${\text{VWATA}^{0,\infty}}$ or $1-{\text{ATA}^{0,\infty}}$,
$\mathcal{A}=(Q,\Sigma,\delta,q_{0},\mathsf{Q_{acc}},X,\mathcal{G},\mathsf{Q^{\geq}},\mathsf{Q^{\leq}})$
we get a timed automaton
$\mathcal{A}=(\mathcal{Q},\Sigma,\Delta,q^{\prime}_{0},\mathcal{Q}_{acc},X\times\\{0,\ldots,|Q|-1\\},\mathcal{G})$
and at every step we reduce the size of the location $q\in\mathcal{Q}$
preserving simulation equivalence. Let $V$ be set of all the functions of the
form $v:X\mapsto\\{0,\ldots,|Q|-1\\}$. Let $\mathcal{L}$ be a set of all the
functions from $Q$ to $V\cup\\{0\\}$. Let $\mathsf{Active}$ be a set of all
the functions from $X$ to a sequence (without duplicate) over
$\\{0,1\ldots|Q-1|\\}$. Then $\mathcal{Q}=\mathcal{L}\times\mathsf{Active}$.
Intuitively, we replace the bunch of conjunctive transitions $C$ into a single
transition, similar to the subset construction for converting Alternating
Finite Automata (AFA) to Non-Deterministic Finite Automata (NFA). But notice
that we can have clauses (or conjunctions) of the form $q\wedge
X^{\prime}.q^{\prime}$. Hence, simple subset construction won’t work as we
need to spawn multiple copies of clocks in $X^{\prime}$, wherein one of the
elements of the new location $\\{q,q^{\prime}\\}$ they are reset while in
another they are not. In general, there could be an unbounded number of such
clock copies required for a single clock, $x\in X$. But due to Lemma 3.16, if
we make sure to compress the states (and hence remove redundant clocks), we
need to keep at most $|Q|$ copies for each clock in $X$. In principle, we are
constructing an NTA $\mathbb{A}$ whose transition system $TS(\mathbb{A})$ is
simulation equivalent to the LTS $\mathsf{T}_{red}(\mathcal{A})$ (see Appendix
D Proposition D.1) and hence to input ${\text{VWATA}^{0,\infty}}$
$TS(\mathcal{A})$. Thus, by Proposition 3.5, $L(\mathcal{A})=L(\mathbb{A})$.
We present the idea via our running example.

Figure 4: Steps in the construction of $\mathbb{A}$ corresponding to our
running example. With the color coding in $q^{\prime}_{1},q^{\prime}_{2}$, it
is easy to see that $q^{\prime}_{2}$ is same as $q^{\prime}_{1}$ on removing
the circled entities in $q^{\prime}_{2}$. Same with $q^{\prime}_{4}$ and
$q^{\prime}_{6}$.

####  3.4.1 Construction on Running Example

Please refer to the ${\text{VWATA}^{0,\infty}}$ of our running example Figure
2. We now illustrate the construction on our running example. We start with
location $q_{0}$, with the $0^{th}$ copies of clock $x$ and $y$. Hence
$q^{\prime}_{0}=\\{(q_{0},(x,0)(y,0)),\mathsf{Active}(x)=[0],\mathsf{Active}(y)=[0]\\}$.
This corresponds to the configuration $C_{0}=\\{(q_{0},\mathbf{0}_{X})\\}$ of
$\mathcal{A}$. In the input automaton, the transitions from $q_{0}$ on $a$ is
defined by $\delta(q_{0},a)=q_{0}\wedge x.q_{1}$. Hence, we need to spawn a
new copy of clock $x$ as it is reset in one transition and not in another. We
associate this new copy of clock $x$ with the branch that resets $x$, i.e.,
this new clock $x$ is associated with location $q_{1}$. Hence, we have
$\Delta(q^{\prime}_{0},a)=(x,1).q^{\prime}_{1}$ where
$q^{\prime}_{1}=\\{(q_{0},(x,0),(y,0)),(q_{1},(x,1)(y,0)),\mathsf{Active}(x)=0\geq
1,\mathsf{Active}(y)=0\\}$. Intuitively, $q^{\prime}_{1}$ corresponds to the
configurations of the form
$C_{1}=\\{(q_{0},\nu^{1}_{0}),(q_{1},\nu^{1}_{1})\\}$ of $\mathcal{A}$, where
$\nu^{1}_{0}(x)=\text{value of }(x,0)$, $\nu^{1}_{1}(x)=\text{value of
}(x,1)$, and $\nu^{1}_{0}(y)=\nu^{1}_{1}(y)=\text{value of }(y,0)$. We
continue with this new location. Hence, we will consider the transitions from
both $q_{0}$ and $q_{1}$ on $a$. The component $((q_{0},(x,0),(y,0)))$ on $a$
again spawns a new copy of clock $x$ as it resets the clock in one while not
resetting on self-loop, hence, getting
$\\{(q_{0},(x,0),(y,0)),(q_{1},(x,2)(y,0))\\}$ (possibility 1 from $q_{0}$,
the only possibility). Notice that we spawned $(x,2)$ as $(x,1)$ is in use by
$q_{1}$ already. The component $(q_{1},(x,1)(y,0))$ will be computed using the
transition function of input automaton, i.e. $\delta(q_{1},a)=(y.q_{2}\wedge
x\leq 2)\vee q_{1}$. Here, we either stay at $q_{1}$ with the same set of
clock copies as before (possibility 1 from $q_{1}$), or we need a new copy of
$y$ while simultaneously checking for the clock copy of $x$ corresponding to
location $q_{1}$ (i.e. $(x,1)$) is $\leq 2$ (possibility 2 from $q_{1}$).
Combining the possibilities 1 from $q_{0}$ and $q_{1}$ we get,
$\scriptstyle{{\\{(q_{0},(x,0),(y,0),(q_{1},(x,2),(y,0))(q_{1},(x,1),y,0),\mathsf{Active}(x)=[0\geq
1\geq 2],\mathsf{Active}(y)=[0]\\}}}$. But $q\in\mathsf{Q^{\leq}}$. Hence, if
we can reach the accepting state from $(q_{1},(x,1),(y,0))$ then we can reach
the accepting state from $(q_{1},(x,2),(y,0)$ too, as $\text{value of
}(x,1)\geq\text{value of }(x,2)$ (this fact is also encoded in the
$\mathsf{Active}(x)$ sequence). Thus, $(q_{1},(x,2),(y,0))$ can be removed
from the new location without affecting simulation equivalence (and hence
language equivalence). This corresponds to the removal of redundant states in
the construction of the runs of $\mathsf{T}_{red}(\mathcal{A})$ from
$T(\mathcal{A})$. Hence, after deletion we get
$\scriptstyle{{q^{\prime}_{2}=\\{(q_{0},(x,0),(y,0),\cancel{(q_{1},(x,2),(y,0))},(q_{1},(x,1),y,0),\mathsf{Active}(x)=[0\geq
1\cancel{\geq 2}],\mathsf{Active}(y)=[0]\\}=q^{\prime}_{1}}}$.

Figure 5:  Final Automata after applying the reductions

Thus, combining result of the transition of $q_{0}$ on $a$ and possibility 1
from $q_{1}$ we get
$\scriptstyle{{q^{\prime}_{1}=\\{q_{0},(x,0),(y,0),(q_{1},(x,1),y,0),\mathsf{Active}(x)=0\geq
1,\mathsf{Active}(y)=0\\}}}$.
Combining results possibility 1 from $q_{0}$ and possibility 2 from $q_{1}$,
we get
$\scriptstyle{\\{q_{0},(x,0),(y,0),(q_{1},(x,2),(y,0)),}$
$\scriptstyle{(q_{2},(x,1),(y,1))\mathsf{Active}(x)=0\geq 2\geq
1,\mathsf{Active}(y)=0\geq 1.\\}=q^{\prime}_{3}}$ if $(x,1)\leq 2$. Note that
each location from $Q$ appears at most once in $q^{\prime}_{3}$. Hence, there
is no scope of reduction. Combining the above two combination of
possibilities,
$\Delta(q^{\prime}_{1},a)=q^{\prime}_{1}\vee(y,1).(q^{\prime}_{3}\wedge x\leq
2)$. Continuing this we get the resulting NTA $\mathbb{A}$ equivalent to the
input formula $\phi$. Notice that we are eliminating the conjunctive
transitions using subset like construction and keeping the disjunctions as it
is. Hence, after eliminating all the conjunctive transitions the reduced
automata contains only disjunctions amongst different locations in the output
formulae of the transitions giving an NTA. Refer to Figures 4, 5.

####  3.4.2 Worst Case Complexity

By construction in [2], the number of states in the region automata of
$\mathbb{A}=W\leq|\mathcal{Q}|\times(|X|\times|Q|)!\times 2\times(c_{max}+1)$
where $c_{max}$ is the max constant used in the guards in $\mathcal{G}$ and
$|\mathcal{Q}|=|Q|\times(|X|^{|Q|}+1)\times(|Q|!)^{|X|}$. Hence,
$W=O(2^{Poly(|A|)})$ implying that the emptiness could be checked in NPSPACE =
PSpace . Notice that the state containing the location $(L,\mathsf{Act})$ will
only have to store the region information of active clocks, which, in
practice, could be much less than the worst case. Hence, lazily spawning clock
copies may result in NTA with much less number of clocks than the worst case
(i.e. $|X|\times|Q|$).

##  4 Expressiveness of $\text{TPTL}^{0,\infty}$

We now compare the expressive power of 1-$\text{TPTL}^{0,\infty}$ with respect
to that of MITL.

###  4.1 Metric Temporal Logic(MTL)

MTL is a real-time extension of $\mathsf{LTL}$ where the $\mathsf{U}$ modality
is guarded with an interval. Syntax of MTL is defined as follows.
$\varphi::=a\leavevmode\nobreak\ |\top\leavevmode\nobreak\
|\varphi\wedge\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\neg\varphi\leavevmode\nobreak\ |\leavevmode\nobreak\
\varphi\mathsf{U}_{I}\varphi,$
where $a\in\Sigma$ and $I\in\mathcal{I}_{\mathsf{int}}$. For a timed word
$\rho=(\sigma_{1},\tau_{1})(\sigma_{2},\tau_{2})\ldots(\sigma_{n},\tau_{n})\in
T\Sigma^{*}$, a position $i\in dom(\rho)$, an MTL formula $\varphi$, the
satisfaction of $\varphi$ at a position $i$ of $\rho$, denoted
$\rho,i\models\varphi$, is defined as follows. We discuss only the semantics
of temporal modalities. Boolean operators mean as usual. $\rho,i\ \models\
\varphi_{1}\mathsf{U}_{I}\varphi_{2}\ \text{iff}\ \exists j>i.\rho,j\ \models\
\varphi_{2},\tau_{j}-\tau_{i}\in I,\ \text{and}\ \forall i<k<j.\rho,k\
\models\ \varphi_{1}$. As usual,
$\mathsf{F}_{I}(\phi)=\top\mathsf{U}_{I}\phi$,
$\mathsf{G}(\phi)=\neg\mathsf{F}_{I}\neg\phi$ ,
$\mathsf{Next}_{I}\phi=\bot\mathsf{U}_{I}\phi$. The language of an MTL formula
$\varphi$ is defined as $L(\varphi)=\\{\rho|\rho,1\models\varphi\\}$. The
subclass of MTL where the intervals $I$ in the until modalities are restricted
to be non-punctual is known as Metric Interval Temporal Logic (MITL) .
$\text{MITL}^{0,\infty}$ [1][3][13] is the subclass of MTL where intervals are
restricted in $\mathcal{I}_{\mathsf{int}}^{0,\infty}$. Satisfiability Checking
for MITL ($\text{MITL}^{0,\infty}$) is ExpSpace -complete (PSpace -complete)
[4] [1] [3]. MITL is strictly more expressive than $\text{MITL}^{0,\infty}$ in
pointwise semantics [12].

######  Remark 4.1.

Any MTL formula can be translated to an equivalent 1-TPTL (closed) formula
using the following equivalence recursively.
$\varphi_{1}\mathsf{U}_{I}\varphi_{2}\equiv
x.(\varphi_{1}\mathsf{U}\varphi_{2}\wedge x\in I)$.

###  4.2 Expressiveness of $\text{TPTL}^{0,\infty}$

######  Theorem 4.2.

1-$\text{TPTL}^{0,\infty}$ is strictly more expressive than MITL.

######  Proof 4.3.

Both MITL and 1-$\text{TPTL}^{0,\infty}$ are closed under all boolean
operations. Hence, we just need to show that any formula of the form
$\varphi^{\prime}\mathsf{U}_{I}\varphi$ is expressible in
1-$\text{TPTL}^{0,\infty}$. Notice that, any MITL formula
$\varphi^{\prime}\mathsf{U}_{[l,u)}\varphi\equiv[\mathsf{G}_{[0,l)}\\{\varphi^{\prime}\wedge(\varphi^{\prime}\mathsf{U}\varphi)\\}]\wedge[\mathsf{F}_{[l,l+1)}\varphi\vee\mathsf{F}_{[l+1,l+2)}\varphi\ldots\mathsf{F}_{[u-1,u)}\varphi]$.
(similar reduction applies for other kinds of intervals).
$\mathsf{G}_{[0,l)}(\varphi^{\prime}\wedge(\varphi^{\prime}\mathsf{U}\varphi))$
is already in $\text{MITL}^{0,\infty}$ (and hence in
1-$\text{TPTL}^{0,\infty}$ by remark 4.1). Hence, it suffices to encode
modalities of the form $\mathsf{F}_{[l,l+1)}$ using 1-$\text{TPTL}^{0,\infty}$
formula. Let $\mathbf{\rho}=(a_{1},\tau_{1}),(a_{2},\tau_{2})\ldots$ be any
timed word. Let $i\in dom(\mathbf{\rho})$ be any point.
$\mathbf{\rho},i\models\mathsf{F}_{[l,l+1)}(\varphi)$ iff there exists a point
$i^{\prime}>i$ such that $\tau_{i^{\prime}}-\tau_{i}\in[l,l+1)$ and
$\mathbf{\rho},i^{\prime}\models\varphi$. $\mathbf{\rho}$ has a point
$i^{\prime}$ within $[l,l+1)$ interval from $i$ where $\varphi$ holds iff
there exist earliest such point $j$ ($j\leq i^{\prime}$) within $[l,l+1)$ from
$i$ where $\varphi$ holds iff there is a point $j^{\prime}>i$ such that
$\tau_{j^{\prime}}-\tau_{i}\geq l$ (i.e.
$\rho,i\models\phi_{0}=\mathsf{F}_{[l,\infty)}\varphi$), and let $j$ be the
first point such that $\tau_{j}-\tau_{i}\geq l$, and
$\mathbf{\rho},j\models\varphi$. Such a point exists due to $\phi_{0}$. Then:

  * •

Case 1: Either there is no point strictly between $i$ and $j$ where $\varphi$
holds. Then occurrence of $j$ within $l+1$ can be expressed using formula,
$\phi_{1}=\neg\mathsf{F}_{[0,l)}\varphi\wedge\mathsf{F}_{[0,l+1)}\varphi$.

  * •

Case 2: Or there exists a point $k$ such that $\tau_{j}-\tau_{k}<1$,
$\tau_{k}-\tau_{i}\in[l-1,l)$, and $\mathbf{\rho},k\models\varphi$.
Equivalently, $i$ satisfies
$\phi_{2}=\mathsf{G}_{[l-1,l)}(\mathsf{F}_{[0,1]}(\varphi))$,

  * •

Case 3: Or there exists a point $k$ with $i<k<j$ such that
$\tau_{j}-\tau_{k}\geq 1$, $\mathbf{\rho},k\models\varphi$, and $\forall
k<k^{\prime}<j.\rho,k^{\prime}\not\models\varphi$.
(1) Such a point $k$ satisfies
$\phi_{\mathsf{approach}}=\varphi\wedge\mathsf{G}_{[0,1)}(\neg\varphi)$.
Indeed a key property is that $k$, the last point in $[0,l)$ satisfying
$\phi$, satisfies $\phi_{\mathsf{approach}}$. By the definition of $k$, i.e.,
there are no occurrences of $\varphi$ after $k$ in $[0,l)$.
(2) Notice that any two point $k_{1}$ and $k_{2}$ satisfying
$\phi_{\mathsf{approach}}$ are at least a unit time apart. Hence, there could
be at most $l$ points satisfying $\phi_{\mathsf{approach}}$ within $[0,l)$.
Then, the following 1-$\text{TPTL}^{0,\infty}$ formula
$\mathsf{Count}\phi_{\mathsf{approach}}(n)$ with parameter $n$ states that
there are exactly $n$ points, $1\leq n\leq l$ within $[0,l)$ of point $i$
where $\phi_{\mathsf{approach}}$ holds. Here,
$\mathsf{Count}\phi_{\mathsf{approach}}(n)\leavevmode\nobreak\
=\leavevmode\nobreak\ \phi_{\geq n}\wedge\neg\phi_{\geq n+1}$, where
$\phi_{\geq
n}=x.((\neg\phi_{\mathsf{approach}})\mathsf{U}(\phi_{\mathsf{approach}}\wedge$
$((\neg\phi_{\mathsf{approach}})\mathsf{U}(\phi_{\mathsf{approach}}\wedge\underbrace{\ldots}_{n-3}\wedge((\neg\phi_{\mathsf{approach}})\mathsf{U}(\phi_{\mathsf{approach}}\wedge
x<l)\ldots)))$.
Observe that for a given timed word and interval $[0,l]$ from $i$, there is a
unique $n$ satisfying this formula
$\mathsf{Count}\phi_{\mathsf{approach}}(n)$.
(3) Using this $n$, the formula
$\gamma(n,\varphi)=x.(\neg\phi_{\mathsf{approach}}\mathsf{U}(\phi_{\mathsf{approach}}\wedge\neg\phi_{\mathsf{approach}}\mathsf{U}(\phi_{\mathsf{approach}}\wedge\underbrace{\ldots}_{n-3}\wedge((\neg\phi_{\mathsf{approach}})\mathsf{U}(\phi_{\mathsf{approach}}\wedge\mathsf{G}(x\leq
l\lor\neg\varphi)\wedge\mathsf{F}(\varphi\wedge x<l+1))\ldots))$ holds if
after $n$ occurrences of $\phi_{\mathsf{approach}}$ (which gives point $k$),
the next occurrence of $\varphi$ occurs before time $l+1$.
Hence, case 3 is characterized by the formula
$\phi_{3}=\bigvee\limits_{n=1}^{l}\mathsf{Count}\phi_{\mathsf{approach}}(n)\wedge\gamma(n,\varphi)$.

Hence, the required formula
$\psi=\phi_{0}\wedge(\phi_{1}\vee\phi_{2}\vee\phi_{3})$. For strict
containment of MITL, consider the formula
$\beta=x.\mathsf{F}(b\wedge\mathsf{F}(b\wedge x\leq 1))$. This specifies,
there exist at least two points within the next unit interval where $b$ holds.
[15] [28] [23] show that this formula is not expressible in MTL (and thus also
in the subclass MITL).

##  5 Discussion and Conclusion

Ferrère [8] proposed an extension of LTL with Metric Interval Regular
Expressions called Metric Interval Dynamic Logic (MIDL) and showed it to be
more expressive than EMITL of [35]. We claim that our proof of PSpace
completeness for 1-${\text{ATA}^{0,\infty}}$ emptiness implies the same for
MIDL0,∞ satisfiability strictly generalizing the results and techniques of
[16] which proved the same for $\text{EMITL}_{0,\infty}$. This resolves one of
the ‘future directions’ of [16]. Authors in [18] generalized the notion of
non-punctuality to non-adjacency for 1-TPTL. We remark that unfortunately,
this notion doesn’t help in making 2-TPTL decidable. Notice that
$\varphi=\mathsf{G}x.\\{\neg\phi\vee\mathsf{F}y.(\top\wedge
x\in[1,2]\wedge\mathsf{F}(\phi_{1}\wedge x\in[1,2]\wedge
y\in[1,2]))\\}\equiv\mathsf{G}[\phi\rightarrow\mathsf{F}_{[1,1]}(\mathsf{F}_{[1,1]}\phi_{1})]$.
Because, for any point $i$ where $\varphi$ holds there is a point $j$ in the
future such that $\tau_{j}-\tau_{i}\in[1,2]$, and from that point $j$ there is
a point $k$ in the future where $\phi_{2}$ holds such that
$\tau_{k}-\tau_{j}\in[1,2]$ and $\tau_{k}-\tau_{i}\in[1,2]$. Solving the
inequalities we get, $\tau_{j}-\tau_{i}=1$ and $\tau_{k}-\tau_{i}=2$. Hence,
$\varphi$ can express some restricted form of punctual timing properties which
leads to the undecidability of satisfiability using encoding similar to [25].
$\text{MITL}^{0,\infty}$ was extended with Counting (TLC) and Pnueli (TLP)
modalities by [15] to increase the expressiveness, meanwhile maintaining the
decidability in EXPSPACE and PSPACE, respectively. TLP and TLC have the same
expressive power. This is because expressing arbitrary non-punctual metric
interval constraints using unilateral intervals is a non-trivial phenomenon in
pointwise semantics (see [16]). While these logics were strictly more
expressive than MITL in continuous semantics in pointwise they are
incomparable. Moreover, TLP and TLC properties are trivially expressible in
$\text{TPTL}^{0,\infty}$ (see construction in Appendix K.1 in [22]), making
our logic strictly more expressive than these. As one of our future work, we
would like to show that TLCI and TLPI (extensions of TLP and TLC using
arbitrary non-punctual intervals) which are decidable in EXPSACE are
expressible in $\text{TPTL}^{0,\infty}$. Finally, we leave open (i)the
extension of this work with Past modalities, (ii)FOL-like characterizations of
$\text{TPTL}^{0,\infty}$, and (iii) whether adding multiple clocks in
$\text{TPTL}^{0,\infty}$ improves expressiveness.

## References

  * [1] R. Alur, T. Feder, and T. Henzinger.  The benefits of relaxing punctuality.  J.ACM, 43(1):116–146, 1996.
  * [2] Rajeev Alur and David L. Dill.  A theory of timed automata.  Theor. Comput. Sci., 126(2):183–235, 1994.
  * [3] Rajeev Alur, Tomás Feder, and Thomas A. Henzinger.  The benefits of relaxing punctuality.  In Luigi Logrippo, editor, Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 19-21, 1991, pages 139–152. ACM, 1991.
  * [4] Rajeev Alur and Thomas A. Henzinger.  Back to the future: Towards a theory of timed regular languages.  In 33rd Annual Symposium on Foundations of Computer Science, Pittsburgh, Pennsylvania, USA, 24-27 October 1992, pages 177–186. IEEE Computer Society, 1992.
  * [5] Rajeev Alur and Thomas A. Henzinger.  Real-time logics: Complexity and expressiveness.  Inf. Comput., 104(1):35–77, 1993.
  * [6] Rajeev Alur and Thomas A. Henzinger.  A really temporal logic.  J. ACM, 41(1):181–203, January 1994.
  * [7] Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey.  On the expressiveness of tptl and mtl.  In Sundar Sarukkai and Sandeep Sen, editors, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, pages 432–443, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.
  * [8] Thomas Ferrère.  The compound interest in relaxing punctuality.  In Klaus Havelund, Jan Peleska, Bill Roscoe, and Erik P. de Vink, editors, Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings, volume 10951 of Lecture Notes in Computer Science, pages 147–164. Springer, 2018.
  * [9] Paul Gastin and Denis Oddoux.  LTL with past and two-way very-weak alternating automata.  In Branislav Rovan and Peter Vojtás, editors, Mathematical Foundations of Computer Science 2003, 28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003, Proceedings, volume 2747 of Lecture Notes in Computer Science, pages 439–448. Springer, 2003.
  * [10] Christoph Haase, Joël Ouaknine, and James Worrell.  On process-algebraic extensions of metric temporal logic.  In A. W. Roscoe, Clifford B. Jones, and Kenneth R. Wood, editors, Reflections on the Work of C. A. R. Hoare, pages 283–300. Springer, 2010\.
  * [11] Moritz Hammer, Alexander Knapp, and Stephan Merz.  Truly on-the-fly ltl model checking.  In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 191–205, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.
  * [12] Thomas A. Henzinger.  It’s about time: Real-time logics reviewed.  In Davide Sangiorgi and Robert de Simone, editors, CONCUR’98 Concurrency Theory, pages 439–454, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.
  * [13] Thomas A. Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens.  The regular real-time languages.  In Kim Guldstrand Larsen, Sven Skyum, and Glynn Winskel, editors, Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, volume 1443 of Lecture Notes in Computer Science, pages 580–591. Springer, 1998.
  * [14] Y. Hirshfeld and A. Rabinovich.  An expressive temporal logic for real time.  In MFCS, pages 492–504, 2006.
  * [15] Yoram Hirshfeld and Alexander Rabinovich.  Expressiveness of metric modalities for continuous time.  In Dima Grigoriev, John Harrison, and Edward A. Hirsch, editors, Computer Science – Theory and Applications, pages 211–220, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.
  * [16] Hsi-Ming Ho.  Revisiting timed logics with automata modalities.  In Necmiye Ozay and Pavithra Prabhakar, editors, Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, pages 67–76. ACM, 2019.
  * [17] S. N. Krishna K. Madnani and P. K. Pandya.  On unary fragments of mtl over timed words.  In ICTAC, pages 333–350, 2014.
  * [18] Shankara Narayanan Krishna, Khushraj Madnani, Manuel Mazo Jr., and Paritosh K. Pandya.  Generalizing non-punctuality for timed temporal logic with freeze quantifiers.  In Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan, editors, Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 182–199. Springer, 2021.
  * [19] Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya.  Logics meet 1-clock alternating timed automata.  In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 39:1–39:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
  * [20] Slawomir Lasota and Igor Walukiewicz.  Alternating timed automata.  ACM Trans. Comput. Log., 9(2):10:1–10:27, 2008.
  * [21] Christof Loding and Wolfgang Thomas.  Alternating automata and logics over infinite words.  In Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, and Takayasu Ito, editors, Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics, pages 521–535, Berlin, Heidelberg, 2000\. Springer Berlin Heidelberg.
  * [22] Khushraj Madnani, Shankara Narayanan Krishna, and Paritosh K. Pandya.  Metric temporal logic with counting.  CoRR, abs/1512.09032, 2015.
  * [23] Khushraj Nanik Madnani.  On Decidable Extensions of Metric Temporal Logic.  PhD thesis, Indian Institute of Technology Bombay, Mumbai, India, 2019\.
  * [24] J. Ouaknine and J. Worrell.  On the decidability of metric temporal logic.  In LICS, pages 188–197, 2005.
  * [25] J. Ouaknine and J. Worrell.  Safety metric temporal logic is fully decidable.  In TACAS, pages 411–425, 2006.
  * [26] Paritosh K. Pandya and Simoni S. Shah.  On expressive powers of timed logics: Comparing boundedness, non-punctuality, and deterministic freezing.  In Joost-Pieter Katoen and Barbara König, editors, CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 60–75. Springer, 2011.
  * [27] Paritosh K. Pandya and Simoni S. Shah.  The unary fragments of metric interval temporal logic: Bounded versus lower bound constraints.  In Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012\. Proceedings, pages 77–91, 2012.
  * [28] A. Rabinovich.  Complexity of metric temporal logic with counting and pnueli modalities.  In FORMATS, pages 93–108, 2008.
  * [29] Alexander Rabinovich.  Complexity of metric temporal logics with counting and the pnueli modalities.  Theor. Comput. Sci., 411(22-24):2331–2342, 2010.
  * [30] Jean Francois Raskin.  Logics, Automata and Classical Theories for Deciding Real Time.  PhD thesis, Universite de Namur, 1999.
  * [31] Gareth Scott Rohde.  Alternating Automata and the Temporal Logic of Ordinals.  PhD thesis, USA, 1997.  AAI9812757.
  * [32] Jan Strejček.  Deeper connections between ltl and alternating automata by radek pelánek jan strejček.  2004\.
  * [33] Heikki Tauriainen.  Automata and linear temporal logic : translations with transition-based acceptance.  2006\.
  * [34] Moshe Vardi.  An automata-theoretic approach to linear temporal logic.  08 1996.
  * [35] Thomas Wilke.  Specifying timed state sequences in powerful decidable logics and timed automata.  In Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Lübeck, Germany, September 19-23, Proceedings, pages 694–715, 1994.

##  Appendix A Reduction from TPTL to VWATA

###  A.1 Pre-processing

We call a formula $\phi$ as temporal formula iff the topmost operator is a
temporal modality. Similarly, we call a subformula $\phi^{\prime}$ of $\phi$
as a temporal subformula.

Pushed Formulae. Given any TPTL formula $\phi$, we first distribute all the
freeze quantifiers, such that, only a single temporal formula appears within
the scope of a freeze quantifier. This can be done using the identity
recursively: $x.(\phi\wedge\phi^{\prime})=x.\phi\wedge x.\phi^{\prime}$,
$y.(\phi\vee\phi^{\prime})=y.\phi\vee y.\phi^{\prime},x.(Prp)=Prp,x.(x\in
I)=\top$ if $0\in I$, else $\bot$, where $Prp$ is a propositional formula over
$\Sigma$ and clock constraints not containing the variable $x$. We call such a
formula where quantifiers are pushed inside as a _pushed formula_. For
example, $\phi=x.(a\mathsf{U}y.(b\wedge y\in(2,3)\vee x\in(1,2))\wedge a\wedge
x\in[0,1))=x.(a\mathsf{U}y.(b\wedge y\in(2,3)\vee x\in(1,2)))\wedge
a\wedge\top=x.(a\mathsf{U}(b\wedge\bot\vee x\in(1,2)))\wedge
a\wedge\top=x.(a\mathsf{U}(x\in(1,2)))\wedge a\wedge\top$.

Strictly Closed Formulae. Similarly, given any closed formula $\phi$,
$X.(\phi)$ is equivalent to $\phi$, by semantics of TPTL for any $X$. Given
any formula $\phi$ using clocks in $|X|$, change every closed subformula
$\phi^{\prime}$ of $\phi$ to $X.\phi^{\prime}$. $X.\phi^{\prime}$ is called a
_strictly closed_ formula. For example, $\phi=x.y.(a\wedge
x.\mathsf{F}(a\wedge x\in(0,1)))$. Notice that subformula
$x.\mathsf{F}(a\wedge x\in(0,1))$ is closed. Hence, changing it to
$x.y.\mathsf{F}(a\wedge x\in(0,1))$ would not affect the language of the
formula, $\phi$. Hence, the new formula we get is $x.y.(a\wedge
x.y.\mathsf{F}(a\wedge x\in(0,1)))$. We can now assume that the given formula
$\varphi$ for which we want to construct VWATA is a pushed, and strictly
closed formula.

Let $A\in 2^{\Sigma}$ and $\phi$ be any pushed strictly closed formula. We
first define $\mathsf{frm}(\phi,A)$ inductively as follows.
$\mathsf{frm}(\phi_{1}\wedge\phi_{2},A)=\mathsf{frm}(\phi_{1})\wedge(\phi_{2})$,
$\mathsf{frm}(\phi_{1}\vee\phi_{2},A)=\mathsf{frm}(\phi_{1})\vee(\phi_{2})$,
$\mathsf{frm}(X.\phi_{1},A)=X.\mathsf{frm}(\phi_{1},a)$, $\mathsf{frm}(a,x\in
I)=x\in I$, $\mathsf{frm}(a,\phi)=\phi)$ if $\phi$ is a temporal formula,
$\mathsf{frm}(a,A)=\top$ if $a\in A$, else $\mathsf{frm}(a,A)=\bot$.

Let $\mathsf{cl}(\varphi)$ contain all the temporal subformulae of $\varphi$.
Given any TPTL formula we now define the ATA
$\mathcal{A}_{\varphi}=(Q,2^{\Sigma},\delta,q_{0},\mathsf{Q_{acc}},X,\mathcal{G})$,
where $Q=\mathsf{cl}(\varphi)\cup\varphi^{0}$ (we call $\varphi^{0}$ the
initial copy of the given formula $\varphi$), $q_{0}=\varphi^{0}$,
$\mathsf{Q_{acc}}$ all the formulae of the form $\mathsf{G}(...)$, i.e.
formulae whose topmost operator is a $\mathsf{G}$ operator, $X$ is set of all
the clocks appearing in $\varphi$, $\mathcal{G}$ is the set of guards
appearing in $\varphi$. We define $\delta$ as follows: for any $A\in
2^{\Sigma}$, $\delta(\varphi^{0},A))=\varphi$,
$\delta(\phi_{1}\mathsf{U}\phi_{2})=\mathsf{frm}(\phi_{2},A)\vee(\mathsf{frm}(\phi_{1},A)\wedge\phi_{1}\mathsf{U}\phi_{2})$,
$\delta(\mathsf{G}(\phi),A)=\mathsf{frm}(\phi,A)\wedge\mathsf{G}(\phi)$. The
equivalence is due to [24][10]. The proof goes through mutatis mutandis for
this case too.

We have the following points.

  * •

The constructed $\mathcal{A}_{\varphi}$ is indeed an ATA satisfying condition
(1) and (2) of the VWATA. We call this VWATA(1-2).

  * •

As the given $\varphi$ is pushed and strictly closed, every closed subformula
$X^{\prime}.\psi$ would be such that $\psi\in\mathsf{cl}(\varphi)$ and
$X^{\prime}=X$. Hence, all the transitions entering the location corresponding
to $\psi$ in $\mathcal{A}_{\varphi}$ are strong reset transitions. This
condition will make sure that if $\varphi\in\text{TPTL}^{0,\infty}$ then
$\mathcal{A}_{\varphi}$ is indeed ${\text{ATA}^{0,\infty}}$.

  * •

The number of transitions entering a subformula $\psi$ of $\varphi$ is exactly
the number of times (say $i$) subformula $\psi$ occurs in $\varphi$. Notice
that, due to the structure of the automaton, $i$ is also the number of paths
from initial state $\varphi^{0}$ to $\psi$ in $\mathcal{A}_{\varphi}$. Hence,
we unfold the automaton, by making $i_{q}$ copies for every location $q$ where
$i_{q}$ is the number of transitions entering $q$. This unfolding is guided by
the tree representation of the given $\varphi$. Hence, the final automaton
will mimic the structure of the tree representation of the given formula
$\varphi$. After this transformation, we make sure that between any two states
there is a unique path (modulo self-loops). This results in the equivalent
automaton $\mathcal{A}$ which is a VWATA (i.e. it satisfies all the conditions
(1-3) of VWATA mentioned in section 2.1.1). Notice that the measure of the
size that we consider in this paper is proportional to the tree representation
and not the DAG. This gap in succinctness is visible while unfolding the
automaton to satisfy condition 3.

  * •

Hence if the given formula $\varphi$ is a $\text{TPTL}^{0,\infty}$ formula,
then $\mathcal{A}$ is ${\text{VWATA}^{0,\infty}}$ as per our definition.

##  Appendix B Proofs in section 3.2

###  B.1 Proof of Remark 3.7

Statement $C\supseteq C^{\prime}$ implies $C\leq_{\mathcal{A}}C^{\prime}$.
Hence, for any timed word $\rho$, if $\rho,i\models\mathcal{A},C$ then
$\rho,i\models\mathcal{A},C^{\prime}$.

######  Proof B.1.

We show that $\supseteq$ is a simulation relation. That is,
$C\textquoteright\subseteq C$ (or $C\supseteq C\textquoteright$) implies
$C\leq_{\mathcal{A}}C\textquoteright$. We just need to prove that $\supseteq$
indeed satisfies condition 2 (condition 1 is trivially satisfied) of the
simulation relation. Notice that the set of accepting configurations is
downward closed. That is, for any accepting configuration $D$, all of its
subset $D\textquoteright$ is accepting (by definition of accepting
configuration). Hence, $\supseteq$ satisfies condition 2.1.

Wlog, let $C=\\{s_{1},\ldots s_{n}\\}$ and $C\textquoteright=\\{s_{1},\ldots
s_{m}\\}$ for some $m\leq n$. For any $(t,a)\in\mathbb{R}\times\Sigma$, by
definition, any $C\xrightarrow{(t,a)}D$ iff $D=D_{1}\cup D_{2}\ldots D_{n}$
where $D_{i}$ is some successor of $s_{i}$ on $(t,a)$. Similarly,
$C^{\prime}\xrightarrow{(t,a)}D^{\prime}iffD\textquoteright=D_{1}\cup
D_{2}\ldots D_{m}$ where $D_{i}$ is some successor of $s_{i}$ on $(t,a)$.
Hence, For any $(t,a)\in\mathbb{R}\times\Sigma$, for any
$C\xrightarrow{(t,a)}D$ there exists a
$C^{\prime}\xrightarrow{(t,a)}D^{\prime}$ such that $D\supseteq
D\textquoteright$ (for any state $s_{i}\in C\cap C\textquoteright$ , just
choose the same successor of $s_{i}$ which was used in $D$ to construct
$D\textquoteright$). Hence, for any successor $C$, we have a successor of
$C\textquoteright$ which is a subset of that of $C$. Hence, $\supseteq$
satisfies condition 2.2.

Intuitively, these extra states $s_{m+1}\ldots s_{n}$ will generate extra
states in the successor configurations, which will make reaching an accepting
configuration harder from $C$ (and its successors) as compared to
$C\textquoteright$ (and its successors),

###  B.2 Proof of Remark 3.9

Statement If $D^{\prime}\subseteq C$ and $D\leq_{\mathcal{A}}D^{\prime}$, then
$(C\setminus D^{\prime})\cup D\leq_{\mathcal{A}}C$. In other words, we can
replace the states in $D^{\prime}$ with that in $D$ in any configuration $C$,
and get a configuration that is simulated by $C$. Hence,
$L(\mathcal{A},(C\setminus D^{\prime})\cup D)\subseteq L(\mathcal{A},C)$.

######  Proof B.2.

Consider a relation $\mathcal{R}$ amongst configurations of $A$ such that
$E\leavevmode\nobreak\ {\mathcal{R}}\leavevmode\nobreak\ E^{\prime}$ iff
$E^{\prime}=E_{1}\cup E_{2}$ such that $E\leq_{\mathcal{A}}E_{1}$ and
$E\leq_{\mathcal{A}}E_{2}$. We first show that $\mathcal{R}$ is a simulation
relation. We need to show that $\mathcal{R}$ satisfies condition (2.2) as it
trivially satisfies condition (2.1). Let $E\leavevmode\nobreak\
\mathcal{R}\leavevmode\nobreak\ E^{\prime}$ and $E^{\prime}=E_{1}\cup E_{2}$
such that $E\leq_{\mathcal{A}}E_{1}$ and $E\leq_{\mathcal{A}}E_{2}$. Let
$E_{2}^{\prime}=E_{2}\setminus E_{1}$. Then
$E\leq_{\mathcal{A}}E_{2}\leq_{\mathcal{A}}E_{2}^{\prime}$ (by remark 3.7). By
definition of simulation preorder, for any $E\xrightarrow{(t,a)}F$ there
exists (1)$E_{1}\xrightarrow{(t,a)}F_{1}$ and
(2)$E_{2}^{\prime}\xrightarrow{(t,a)}F_{2}$ such that
$F\leq_{\mathcal{A}}F_{1}$ and $F\leq_{\mathcal{A}}F_{2}$. Let
$F^{\prime}=F_{1}\cup F_{2}$. By semantics ATA, (1) and (2) imply
$E^{\prime}\xrightarrow{(t,a)}F^{\prime}$. Moreover, by definition of
$\mathcal{R}$, $F\leavevmode\nobreak\ \mathcal{R}\leavevmode\nobreak\
F^{\prime}$ if $E\leavevmode\nobreak\ \mathcal{R}\leavevmode\nobreak\
E^{\prime}$. Hence, for any $E\leavevmode\nobreak\
\mathcal{R}\leavevmode\nobreak\ E^{\prime}$, and $E\xrightarrow{(t,a)}F$ there
exists $E^{\prime}\xrightarrow{((t,a)}F^{\prime}$ such that
$F\leavevmode\nobreak\ \mathcal{R}\leavevmode\nobreak\ F^{\prime}$. Hence,
$\mathcal{R}$ satisfies condition 2.2.

Given $D^{\prime}\leq_{\mathcal{A}}D$. Hence, by remark 3.7, $((C\setminus
D^{\prime})\cup D)\leq_{\mathcal{A}}(C\setminus D^{\prime})$ and $(C\setminus
D^{\prime})\cup D\leq_{\mathcal{A}}D\leq_{\mathcal{A}}D^{\prime}$. Hence,
$(C\setminus D^{\prime})\cup D\leavevmode\nobreak\
\mathcal{R}\leavevmode\nobreak\ ((C\setminus D^{\prime})\cup D^{\prime})$.
Hence, $((C\setminus D^{\prime})\cup D)\leq_{\mathcal{A}}C$.

###  B.3 Proof of Proposition 3.13

Statement \- $s\preceq s^{\prime}$ implies $s\leq_{\mathcal{A}}s^{\prime}$.

######  Proof B.3.

We extend the relation $\preceq$ between configurations of $\mathcal{A}$ as
follows. We say that $C\preceq C^{\prime}$ iff $\forall(q,\nu^{\prime})\in
C^{\prime}\exists(q,\nu)\in C$ such that if $q\in\mathsf{Q^{\sim}}$ then
$\nu^{\prime}\sim\nu$. Let $C\preceq C^{\prime}$. Let $f:C^{\prime}\mapsto
2^{C}\setminus\emptyset$, such that for any $(q,\nu^{\prime})\in C^{\prime}$
and $q\in\mathsf{Q^{\sim}}$, $f((q,\nu^{\prime}))=\\{(q,\nu)|(q,\nu)\in
C\wedge\nu^{\prime}\sim\nu\\}$. Let $s^{\prime}=(q,\nu^{\prime})$ be any state
in $C^{\prime}$ and $s=(q,\nu)$ be any state in $f((q,\nu^{\prime}))$.

To prove the above statement, it suffices to show that $\preceq$ is a
simulation relation.

Key Observation: The transition formula for finding the successor of
$s^{\prime}$ and $s$ on any $(t,a)\in\mathbb{R}_{\geq 0}\times\Sigma$ is the
same, i.e., $\delta(q,a)$. By semantics of ${\text{ATA}^{0,\infty}}$, all the
timing constraints appearing in $\delta(q,a)$ that are satisfied by valuation
$\nu+t$ will also be satisfied by $\nu^{\prime}+t$. Hence, every non-
deterministic choice that can be taken from $s$ can be taken from $s^{\prime}$
on $t,a$. More precisely, for every
$D=\\{(q_{1},\nu_{1}),(q_{2},\nu_{2}),\ldots,(q_{j},\nu_{j})\\}\in\mathsf{Succ}_{\delta}^{st}(s,t,a)$
there exists
$D^{\prime}=\\{(q_{1},\nu^{\prime}_{1}),(q_{2},\nu^{\prime}_{2}),\ldots,(q_{j},\nu^{\prime}_{j})\\}\in\mathsf{Succ}_{\delta}^{st}(s^{\prime},t,a)$
such that for $1\leq i\leq j$, (1) $\nu_{i}$ and $\nu^{\prime}_{i}$ are
constructed from $\nu+t$ and $\nu^{\prime}+t$ by resetting the same set of
clock variables, $X_{i}\subseteq X$. Hence, $\nu^{\prime}_{i}\sim\nu_{i}$. (2)
If $q\in\mathsf{Q^{\sim}}$ then either $q_{i}\in\mathsf{Q^{\sim}}$ or
$\nu^{\prime}_{i}=\nu_{i}=0$ (by definition of ${\text{ATA}^{0,\infty}}$,
every transition from a location in $\mathsf{Q^{\sim}}$ to a location not in
$\mathsf{Q^{\sim}}$ should be a strong reset transition). Hence, if
$q_{i}\notin\mathsf{Q^{\sim}}$ then $\nu\sim\nu^{\prime}=0$, trivially. Hence,
$D\preceq D^{\prime}$. In other words, $\forall
D\in\mathsf{Succ}_{\delta}^{st}(s,t,a)\exists
D^{\prime}\in\mathsf{Succ}_{\delta}^{st}(f^{-1}(s),t,a).D\preceq D^{\prime}$
(Id 1).

Let $C_{min}\subseteq C$ such that (1) $\forall s^{\prime}\in
C^{\prime}\exists s\in C_{min}.s\in f(s^{\prime})$ and (2) $\forall s\in
C_{min}\exists s^{\prime}\in C^{\prime}.s\in f(s^{\prime})$ . Notice that such
a subset should exist.

By remark 3.7, $C\leq_{\mathcal{A}}C_{min}$. Hence, it suffices to show that
$C_{min}\leq_{\mathcal{A}}C^{\prime}$, i.e., Condition (2.1)(2.2) for
simulation relation holds. (Condition 2.1) If $C_{min}$ is an accepting state
then $C^{\prime}$ is an accepting state. This is because, if $C_{min}$ is an
accepting state then it only contains accepting locations. As all locations in
$C^{\prime}$ also appear in $C_{min}$ (and vicec-versa, all the locations in
$C^{\prime}$ are accepting iff $C_{min}$ is accepting. (Condition 2) For any
$t,a\in\mathbb{R}_{\geq 0}\times\Sigma$, for any
$D\in\mathsf{Succ}_{\delta}(C_{min},t,a)$ there exists
$D^{\prime}\in\mathsf{Succ}_{\delta}(C^{\prime},t,a)$ such that
$D\leq_{\mathcal{A}}D^{\prime}$. This is shown as follows. Let
$C_{min}=\\{s_{1},\ldots s_{n}\\}$ and
$C^{\prime}=\\{s^{\prime}_{1},\ldots,s^{\prime}_{m}\\}$. (Condition 2.2) is
equivalent to (Condition 3) For any $t,a\in\mathbb{R}_{\geq 0}\times\Sigma$,
$\forall D_{1}\in\mathsf{Succ}_{\delta}(s_{1},t,a).\forall
D_{2}\in\mathsf{Succ}_{\delta}(s_{2},t,a).\ldots.\forall
D_{n}\in\mathsf{Succ}_{\delta}(s_{n},t,a).\exists
D^{\prime}_{1}\in\mathsf{Succ}_{\delta}(s^{\prime}_{1},t,a).\exists
D^{\prime}_{2}\in\mathsf{Succ}_{\delta}(s^{\prime}_{2},t,a).\ldots.\exists
D^{\prime}_{m}\in\mathsf{Succ}_{\delta}(s^{\prime}_{m},t,a).$ such that
$D_{1}\cup D_{2}\cup\ldots\cup D_{n}\preceq D^{\prime}_{1}\cup
D^{\prime}_{2}\cup\ldots\cup D^{\prime}_{m}$. Condition 3 is implied by
rearranging, $\forall D_{1}\in\mathsf{Succ}_{\delta}(s_{1},t,a).\exists
D^{\prime\prime}_{1}\in\mathsf{Succ}_{\delta}(f^{-1}(s_{1}),t,a).D_{1}\preceq
D_{1}^{\prime\prime}\wedge\forall
D_{2}\in\mathsf{Succ}_{\delta}(s_{2},t,a).\exists
D^{\prime\prime}_{2}\in\mathsf{Succ}_{\delta}(f^{-1}(s_{2}),t,a).D_{2}\preceq
D_{2}^{\prime\prime}\wedge\ldots\wedge\forall
D_{n}\in\mathsf{Succ}_{\delta}(s_{n},t,a).\exists
D^{\prime\prime}_{n}\in\mathsf{Succ}_{\delta}(f^{-1}(s_{n}),t,a).D_{n}\preceq
D_{n}^{\prime\prime}$ which is in turn is implied by (Id 1). Hence, proved.

##  Appendix C Proof of Lemma 3.16

###  C.1 ATA Semantics as Directed Acyclic Graph

Equivalent to the Transition Systems based semantics of ATA described in
section 2.1.1, we can also represent runs of ATA $\mathcal{A}$ starting from a
state $s$ as a Directed Acyclic Graph (DAG) such that each node $m$ of a DAG
is labeled with a state $s_{m}\in S$. All the transitions from nodes at depth
$n$ to the nodes at depth $n+1$ are labeled with the same symbol
$(t_{n+1},a_{n+1})$. The root node is labeled as $s$. Two children sharing the
same parent will have different labels. $M=\\{m_{1},\ldots m_{k}\\}$ is the
set of children of node $m$ iff $C_{m}=\\{s_{1},\ldots s_{k}\\}$ is a
successor of $s_{m}$ on time delay $t$ and action $a$, and for all $1\leq
i\leq k$, $m_{i}$ is labelled as $s_{i}$. The set of labels appearing at depth
$n$ is the configuration that is reached at step $n$ by transition system
$T(\mathcal{A},\\{s\\})$. See the different colored paths in figure 3. Those
paths and individual states generates a DAG (a tree in this case). This tree
is equivalent to the run presented there.

###  C.2 Relation between DAGs of $\mathsf{Img}(R)$

If $R$ is represented as a run DAG, then $\mathsf{Img}(R)$, is defined
similarly. To be precise, $\mathsf{Img}(R)$ is a subDAG of $R$ constructed as
follows. At any level $i$ of tree $R$, if there is a node $s^{\prime}$ such
that there exists yet another node $s\neq s^{\prime}$ and $s\preceq
s^{\prime}$ then we delete the subDAG rooted at $s^{\prime}$. See an example
in figure 6. We now prove the main lemma which will be used to show that our
construction from ${\text{VWATA}^{0,\infty}}$ to Timed Automata terminates.
Moreover, the Timed Automata has at most exponentially many locations and
polynomially many clocks.

Figure 6: Tree corresponding to run $R$ on
$\mathbf{\rho}=(a,0)(a,1)(a,1.5)(b,1.5)$ for the ${\text{VWATA}^{0,\infty}}$
in Fig 2. Remove the highlighted subDAG to get the run DAG for
$\mathsf{Img}(R)$

####  C.2.1 Type Sequences of Paths in Run DAG

Let node $m$ ($m^{\prime}$) at level $n$ ($n^{\prime}$) be labelled $(q,\nu)$
($(q^{\prime},\nu^{\prime})$) of a run DAG of $\mathcal{A}$. An annotated path
between node $n$ and $n^{\prime}$ can be expressed using a sequence of states
visited along the path and the set of clock resets along the path as follows:
$P=(q,\nu)[X_{1},(q_{1},\nu_{1})][X_{2},(q_{2},\nu_{2})]\ldots[X_{m-m^{\prime}},(q^{\prime},\nu^{\prime})]$
where $X_{1},\ldots,X_{m-m^{\prime}}\subseteq X$. We associate a type defined
by sequence over $H=(2^{X}\times Q)\cup Q^{*}\cup Q$ to the annotated paths of
a run tree of ${\text{VWATA}^{0,\infty}}$, $\mathcal{A}$, where
$Q^{*}=\\{q^{*}|q\in Q\\}$. We define $\mathsf{Type}(P)$ as a sequence
obtained from $P$ as follows: (1) Drop the clock valuations in the sequence,
(2) Replace every substring
$[X_{i-1},q_{i-1}][X_{i},q_{i}][X_{i+1},q_{i+1}]\ldots[X_{i+j+1},q_{i+j+1}]$
with $[X_{i-1},q_{i-1}][X_{i},q_{i}]q_{i}^{*}[X_{i+j+1},q_{i+j+1}]$ iff
$q_{i-1}\neq q_{i}$ or $X_{i}\neq\emptyset$, and $q_{i+j+1}\neq q_{i}$ or
$X_{i+j+1}\neq\emptyset$, and $X_{i+1}=X_{i+2}=\ldots=X_{i+j}=\emptyset$ and
$q_{i}=q_{i+1}=q_{i+2}=\ldots=q_{i+j}$ Notice that if $\mathcal{A}$ is a VWATA
and $q_{i}=q_{i+1}$ then $X_{i+1}$ should necessarily be an empty set as self-
loops are reset free. For example, consider path
$P=(q,\nu)[X_{1},(q_{1},\nu_{1})][\emptyset,(q_{1},\nu_{1})][\emptyset,(q_{1},\nu_{1})][X_{2},(q_{2},\nu_{2})][X_{3},(q_{3},\nu)]$.
$\mathsf{Type}(P)=q.[X_{1},(q_{1},\nu_{1})].q_{1}^{*}.[X_{2},(q_{2},\nu_{2})].q_{2}^{*}.[X_{3},(q_{3},\nu)].q_{3}^{*}$.

This sequence $\mathsf{Type}(P)$ is called the type of path. Notice that
$\mathsf{Type}(P)$ is a sequence over $H$. Moreover, as $\mathcal{A}$ is a
VWATA, $|\mathsf{Type}(P)|$ is bounded by $|Q|$.

######  Remark C.1.

For any VWATA, the path type between two nodes labeled $(q,\nu)$ and
$(q^{\prime},\nu^{\prime})$ is only dependant on $q$ and $q^{\prime}$. In
other words, no matter which run tree we pick and which pair of nodes in that
run tree we pick, the type of path between those nodes will only depend on the
location appearing in those nodes. This is because the structure of the
automaton VWATA is a Tree-like structure.

###  C.3 Proof

Statament \- Let
$\mathcal{A}=(Q,\Sigma,\delta,q_{0},\mathsf{Q_{acc}},X,\mathcal{G})$ be either
an 1-${\text{ATA}^{0,\infty}}$ or ${\text{VWATA}^{0,\infty}}$ . Let Run $R$ of
$\mathcal{A}$, and
$R^{\prime}=\mathsf{Img}(R)=C_{0}^{\prime\prime}(t_{0},a_{0})C_{1}^{\prime\prime}(t_{1},a_{1})\ldots$,
then for all $i\geq 1$, $C_{i}^{\prime\prime}$ does not contain states
$(q,\nu)$ and $(q,\nu^{\prime})$ where $\nu\neq\nu^{\prime}$ for any $q\in Q$.
In other words, if every location $q\in Q$ appears at most once in any
configuration $C_{i}^{\prime\prime}$ for any $i\geq 1$. Hence,
$|C_{i}^{\prime\prime}|\leq|Q|$.

######  Proof C.2.

Notice that if $\mathcal{A}$ was 1-${\text{ATA}^{0,\infty}}$, the above
statement is straightforward as no two clock valuations are incomparable in
the case of 1-clock. We now show the same for $\mathcal{A}$ being a multi-
clock ${\text{VWATA}^{0,\infty}}$.

The following statement is equivalent to the statement of the lemma. Let $R$
be any run represented as a run DAG, then $\mathsf{Img}(R)$ is such that at
every level $m$, at most one node is labeled with any location $q$.

We now show the following. In the tree corresponding to $\mathsf{Img}(R)$,
there is exactly one path $P$ of length $n$ of a particular type (Statement
1). Hence, if there are two paths, $P$ and $P^{\prime}$ reaching at location
$q$ at step $n$, then $\mathsf{Type}(P)\neq\mathsf{Type}(P^{\prime})$. But by
remark C.1 path from a state in location $q^{\prime}$ to location $q$ is of a
unique type. Hence, Statement 1 along with remark C.1 implies the result.

For paths of length 1, statement 1 trivially holds. Suppose it holds for all
the paths of length $\leq n-1$ for some $n$. We now prove the induction step
by contradiction. Suppose there are two different paths of the same type
$P=(p_{1},\nu_{1})[Y_{2},(p_{2},\nu_{2})]\ldots[Y_{n},(p_{n},\nu_{n})]$ and
$P^{\prime}=(p^{\prime}_{1},\nu^{\prime}_{1})[Y^{\prime}_{2},(p^{\prime}_{2},\nu^{\prime}_{2})]\ldots[Y^{\prime}_{n},(p^{\prime}_{n},\nu^{\prime}_{n})]$
ending up at states $s=(p_{n},\nu_{n})=(q,\nu_{n})$ and
$s^{\prime}=(p^{\prime}_{n},\nu_{n}^{\prime})=(q,\nu_{n}^{\prime})$,
respectively, at step $n$ such that $s\not\preceq s^{\prime}$. Hence,
$\nu_{n}$ and $\nu_{n}^{\prime}$ are incomparable. Let
$\mathsf{Type}(P)=\mathsf{Type}(P^{\prime})=q_{0}.q_{0}^{*}.[X_{1},q_{1}].q_{1}^{*}.\ldots.q_{j-1}^{*}.[X_{j},q_{j}].q_{j}^{*}$.
Let $1<m_{1}\leq m_{2}\leq\ldots\leq m_{j}$ be the points where $P$ takes a
non-self-loop transition. That is, $P$ takes a transition from location
$q_{i-1}$ to $q_{i}$ at point $m_{i}$. Similarly, $1<m^{\prime}_{1}\leq
m^{\prime}_{2}\leq\ldots\leq m^{\prime}_{k}$ be the points such that
$P^{\prime}$, for any $i\leq k$, takes a transition from location $q_{i-1}$ to
$q_{i}$ at point $m^{\prime}_{i}$. Without loss of generality, we assume
$m_{k}^{\prime}\leq m_{k}$. Please refer figures 7, 8, 9. Following are the
possibilities.

  * •

Case 1: $m_{k}<n$. This implies, $p_{n-1}=p^{\prime}_{n-1}=p_{n}$.Transition
from $p_{n-1}$ to $p_{n}$ is a non-reset transition. By condition (2) of
VWATA, every self-loop transition is a non-reset transition. Hence, if
$p_{n-1}=p^{\prime}_{n-1}$, then the transition from $p^{\prime}_{n-1}$ to
$p^{\prime}_{n}$ is a non-reset transition too. Hence,
$\nu^{\prime}_{n}-\nu_{n}=\nu^{\prime}_{n-1}-\nu_{n-1}$. This would imply,
$\nu_{n-1}$ and $\nu_{n-1}^{\prime}$ are incomparable. But paths $P[1..n-1]$
and $P^{\prime}[1.n-1]$ are of the same type and of length strictly less than
$n$. This violates the induction hypothesis.

  * •

Case 2: $m^{\prime}_{k}=m_{k}=n$. $p_{n-1}=p^{\prime}_{n-1}\neq p_{n}$. By
condition (3), all the transitions from any location $q^{\prime}$ to
$q^{\prime\prime}$ reset the same set of clocks. Hence, the same set of clocks
$Y\subseteq X$ will reset while transitioning at step $n$ in both paths. This
would again imply, $\nu_{n-1}$ and $\nu_{n-1}^{\prime}$ are incomparable
leading to a contradiction of the induction hypothesis.

  * •

Case 3: $m_{k}^{\prime}<m_{k}$ and $m_{k}=n$. We encourage readers to refer to
figure 9. Suppose $m^{\prime}_{k}>m_{k-1}$. This implies that both $P$ and
$P^{\prime}$ are at location $q_{k-1}$ at point $w=m^{\prime}_{k}-1$. There
are two sub-possibilities, (1)$\nu_{w}$, $\nu^{\prime}_{w}$ are incomparable.
This implies that $P[1..w]\neq P^{\prime}[1..w]$ but
$\mathsf{Type}(P[1..w])=\mathsf{Type}(P^{\prime}[1..w])$, which contradicts
the induction hypothesis. In other words, as both $P$ and $P^{\prime}$ are
paths in $\mathsf{Img}(R)$, $\nu_{w}$ and $\nu^{\prime}_{w}$ should be either
equal or incomparable. Otherwise, we should have deleted one of the subtree
corresponding to the simulated state from the run tree, discontinuing either
$P$ or $P^{\prime}$. But, $\nu_{w}$ and $\nu^{\prime}_{w}$ being incomparable
violates the induction hypothesis. (2)$\nu_{w}=\nu^{\prime}_{w}$. This implies
that $P[1..w]=P^{\prime}[1..w]$. In this case, both $P[w..n]$ and
$P^{\prime}[w..n]$ are distinct paths of the same type and length of the
subtree rooted at node labelled with state $(q_{k-1},\nu_{w})$ (subgraph of
the original tree). As $n-w<n$, this contradicts the induction hypothesis.
Hence, both sub-possibilities lead to a contradiction. Thus the only
possibility is that $m^{\prime}_{k}\leq m_{k-1}$. Applying the similar
argument, (and let $m_{0}=0$) inductively for all $1\leq i<k$, we have,
$m^{\prime}_{i+1}<m_{i}$. Hence, for any clock $x\in X_{1}\cup X_{2}\cup\ldots
X_{k}$, $\nu_{n}(x)\leq\nu^{\prime}_{n}(x)$ as in $P^{\prime}$ all these
clocks are reset before their corresponding reset in $P$. Moreover, for all
the other clocks not in $X_{1}\cup\ldots X_{k}$, the values in $P$ and
$P^{\prime}$ remain the same. Hence, $\nu_{n}\leq\nu^{\prime}_{n}$. This
contradicts the assumption that $\nu_{n}$ and $\nu^{\prime}_{n}$ are
incomparable. Hence proved.

Figure 7: Figure Corresponding to Case 1 in lemma 3.16

Figure 8: Figure Corresponding to Case 2 in lemma 3.16 Figure 9: Figure
Corresponding to Case 3 in lemma 3.16. Note that the point marked above
contradicts the Induction Hypothesis. Hence,$m^{\prime}_{k}<m_{k-1}$.
Recursively arguing about $m^{\prime}_{k-2}\ldots m^{\prime}_{1}$ we get the
$\nu^{\prime}\geq\nu$.

Notice that the argument presented in Case 3 proves a stronger Lemma 3.16.

######  Lemma C.3.

Given any pair of paths
$P=(q_{0},\nu_{1})[Y_{2},(p_{2},\nu_{2})]\ldots[Y_{n},(p_{n},\nu_{n})][Y,q]$
and
$P^{\prime}=(q_{0},\nu_{1})[Y^{\prime}_{2},(p^{\prime}_{2},\nu^{\prime}_{2})]\ldots[Y^{\prime}_{n},(p^{\prime}_{n},\nu^{\prime}_{n})][Y^{\prime},q]$
of same length of run tree of $\mathsf{T}_{red}(\mathcal{A})$ such that
$p^{\prime}_{n}\neq q$ and $p_{n}=q$, then $\nu^{\prime}_{n}\geq\nu_{n}$.

Intuitively, if from a configuration without where every location appears
atmost once, if we fire a transition, leading to 2 states at same location
$(q,\nu)$ and $(q,\nu^{\prime})$, then by VWATA one of them has to be a result
of self-loop transition (say $(q,\nu^{\prime})$), in which case, the clock
valuation of the state resulting from self-loop transition $\nu^{\prime}$ is
always greater than or equal to the other valuation $\nu$.

##  Appendix D Formal Construction from ${\text{VWATA}^{0,\infty}}$ to NTA

####  D.0.1 Formal Construction

Given a ${\text{VWATA}^{0,\infty}}$ or $1-{\text{ATA}^{0,\infty}}$,
$\mathcal{A}=(Q,\Sigma,\delta,q_{0},\mathsf{Q_{acc}},X,\mathcal{G},\mathsf{Q^{\geq}},\mathsf{Q^{\leq}})$
we get a timed automaton
$\mathbb{A}=(\mathcal{Q},\Sigma,\Delta,q^{\prime}_{0},\mathcal{Q}_{acc},X\times\\{0,\ldots,|Q|-1\\},\mathcal{G})$
and at every step we reduce the size of the location $q\in\mathcal{Q}$
preserving simulation equivalence. Let $V$ be set of all the functions of the
form $v:X\mapsto\\{0,\ldots,|Q|-1\\}$. Let $\mathcal{L}$ be a set of all the
functions from $Q$ to $V\cup\\{0\\}$. Let $\mathsf{Active}$ be a set of all
the functions from $X$ to a sequence (without duplicate) over
$\\{0,1\ldots|Q-1|\\}$. Then $\mathcal{Q}=\mathcal{L}\times\mathsf{Active}$.

We now give some intuition before formal construction. The intuition behind
the tuples of $\mathbb{A}$: Our construction technique is inspired by subset
construction to eliminate conjunctive transitions in AFA, We introduce at most
$|Q|$ copies of every clock $x$ of $A$. This is required as there are
conjunctive transitions where a clock variable $x$ is reset in one of these
transitions while not in another. Hence, there are multiple possible
values/copies of variable $x$ that are generated due to these conjunctive
transitions. By lemma 3.16, the number of clocks that we require at any point
of time is bounded by $|Q|$. Hence, the bound $|Q|$ on copies for $X$.

A location of $\mathbb{A}$ is of the form $q^{\prime}=(L,\mathsf{Act})$.
Intuitively $L(q)=0$ means that $q^{\prime}$ doesn’t contain the location $q$
of $\mathcal{A}$. While, $L(q)=v$, means $q^{\prime}$ contains the location
$q$ of $\mathcal{A}$ and the copy of any clock $x\in X$ that is required for
computing the successors of $q^{\prime}$ due to $q$ is given by $(x,v(x))$.
Finally, $\mathsf{Act}$ stores all the active copies of $X$. In other words,
for any $x\in X$, if $\mathsf{Act}(x)=[1,3,5]$, then it means that clock
copies $1,3,5$ are the clock copies that will be required to compute the
successor of from location $q^{\prime}$. Hence, $L(q)(x)\in\\{1,3,5\\}$ for
any $q\in Q$ such that $L(q)\neq 0$. And, last reset of $(x,1)$ was before
last reset of $(x,3)$ which was before last reset of $(x,5)$. Hence, the value
of $(x,1)\geq(x,3)\geq(x,5)$.

Initial location is $(L_{0},\mathsf{Act}_{0})$, such that $L_{0}(q_{0})(x)=0$
for all $x\in X$ and $L_{0}(q)=0$ and for all $q\in Q$, $q\neq q_{0}$.
Moreover, $\mathsf{Act}(x)=[0]$ for all $x\in X$.

We refer the readers to our running example discussed prior to the
construction in the main paper section 3.4.1. Consider the
${\text{VWATA}^{0,\infty}}$, from our running example, figure 2. We show the
construction of $\Delta$ for any arbitrary location $q\in\mathcal{Q}$ using
the transition function $\delta$. This construction can then be used starting
from the initial location $q_{0}^{\prime}$ until all the reachable states are
explored. Hence, the size of the timed automaton that we get might be much
less than the worst case.

Formal Reduction: Let $q^{\prime}=(L,\mathsf{Act})$ be any location in
$\mathcal{Q}$. And let $Q^{\prime}=\\{q_{1},\ldots,q_{n}\\}=\\{q|q\in Q\wedge
L(q)\neq 0\\}$. Without loss of generality, we assume that the output formula
of the transition function $\delta$ is given in Disjunctive Normal Form (DNF)
222Notice that conversion to DNF will only incur a blow up in the size of the
formula, but not in the size of the locations of the input ATA. Hence, it
wouldn’t affect the worst-case size in the output NTA.. Hence, for any
$q_{i}\in Q^{\prime}$, $\delta(q_{i},a)=\bigvee\mathbb{C}_{i}$ where
$\mathbb{C}_{i}$ is a set of clauses (i.e. conjunction of transitions). Choose
clauses $C_{1}\in\mathbb{C}_{1},C_{2}\in\mathbb{C}_{2},\ldots
C_{n}\in\mathbb{C}_{n}$ and construct a clause (conjunction of transition)
$C=C_{1}\wedge C_{2}\ldots\wedge C_{m}$. Let $\mathbb{C}$ be set of all such
clauses. We now show the successor of $q^{\prime}$ due to a clause
$C\in\mathbb{C}$ (recall $C=C_{1}\wedge C_{2}\ldots C_{n}$). By conditions 2
and 3 of VWATA definition, every $q\in Q$ appears in at most two of the
clauses $C_{i_{q}}$ and $C_{j_{q}}$ and at most once in each as all the
transitions from $i_{q}$ to $q$ reset same set of clocks (for some
$i_{q},j_{q}\in\\{1,2,\ldots,n\\}$). Moreover, either $q_{i_{q}}=q$ or
$q_{j_{q}}=q$. Hence, every location $q\in Q$ appears at most twice in $C$.
Let $\mathsf{Appear}(q,C)\subseteq\\{C_{1},C_{2},\ldots,C_{n}\\}$ output set
of clauses where $q$ appears. Similarly, for any guard $g\in\mathcal{G}$, let
$\mathsf{Appear}_{G}(g,C)\subseteq\\{C_{1},C_{2},\ldots,C_{n}\\}$ output set
of clauses where guard $g$ appears. Let $C=X_{1}.Q_{1}\wedge X_{2}.Q_{2}\ldots
X_{m}.Q_{m}\wedge g_{1}\wedge g_{2}\wedge\ldots\wedge\wedge g_{n}$
($Q_{1},Q_{2},\ldots,Q_{m}\subseteq Q$). Notice that any $q$ will appear at
most once within the scope of a clock reset (by condition 2-3 of
$\text{VWATA})$. Notice that $X_{1},\ldots X_{m}\subseteq X$. We abuse the
notation by assuming that these sets could be empty too. Hence,
$\emptyset.Q_{1}$ means $\bigwedge Q_{1}$ Let $\mathsf{Reset}(q,C)=X_{i}$ if
$q\in Q_{i}$. For any $x\in X$, let $J_{x}=\\{j|1\leq j\leq m\wedge x\in
X_{j}\\}$. That is, $J_{x}$ indicates the index of transitions that resets
clock $x$. Let $J^{\prime}_{x}=\\{i|1\leq i\leq n\wedge x$ is reset in all
transitions in $C_{i}\\}$. Let $J^{\prime\prime}_{x}(i)=\\{k|1\leq k\leq
n\wedge L(q_{k})(x)=L(q_{i})(x)\\}$ indicates indices of the locations in
$\\{q_{1},\ldots q_{n}\\}$ which refer the the same copy of clock $x$ as
$q_{i}$. We now give the step-by-step construction of a transition from
$q^{\prime}$ due to clause $C$.

  1. 1.

$Y_{C}\leftarrow\emptyset$ (stores the set of clock copies to be reset).
$(L_{C},\mathsf{Act}_{C})$ is the location that is a successor of location
$(L,\mathsf{Act})$ constructed from clause $C$.

  2. 2.

For all $q\in Q$ do:

    1. (a)

If $q$ doesn’t appear in $C$, then $L^{\prime}(q)=0$.

    2. (b)

If $\mathsf{Appear}(q,C)=\\{C_{i_{q}}\\}$ and $\mathsf{Reset}(q,C)=\emptyset$
then

      1. i.

For all $x\in X$: $L_{C}(q)(x)\leftarrow L(q_{i_{q}})(x)$ (/*assign the same
clock copies as the parent $q_{i_{q}}$ to the state $q$*/) .

    3. (c)

If $\mathsf{Appear}(q,C)=\\{C_{i_{q}}\\}$ and
$\mathsf{Reset}(q,C)=X_{q}\neq\emptyset$ then for all $x\in X_{q}$:

      1. i.

If $J_{x}=\\{1,2,\ldots,m\\}$ (/* In this case, we need to maintain only one
copy of clock $x$ (the $0^{th}$ copy) as all the transitions simultaneously
reset their corresponding copies of $x$ to 0.*/) $L_{C}(q)(x)\leftarrow 0$,
$\mathsf{Act}_{C}(x)\leftarrow[0],Y_{c}\leftarrow Y_{c}\cup(x,0)$.

      2. ii.

Else if $J_{x}\subseteq\\{1,2,\ldots,m\\}$ and
$J^{\prime\prime}_{x}(i_{q})\subseteq J^{\prime}_{x}$ (/* In this case, all
the transitions exiting from the location $q_{k}\in Q^{\prime}$ referring to
the same copy of clock $x$ as $q_{i_{q}}$ reset the clock $x$. Hence, we need
not create a new copy of $x$. We just reset the copy of $x$ referred by
location $q_{i_{q}}$ */). Let $w=L(q_{i_{q}})(x)$. Then,
$L_{C}(q)(x)\leftarrow w$, $Y_{c}\leftarrow Y_{c}\cup(x,w)$.

      3. iii.

Else (/* In this case, the copy of $x$ referred by $q_{i_{q}}$ is reset by
some transitions and not reset by others. Hence, we need to create a new copy
of $x$ and reset that copy of $x$ */). Let $w_{x}$ be the smallest number not
appearing in $\mathsf{Act}(x)$. $L_{C}(q)(x)\leftarrow w_{x}$,
$\mathsf{Act}_{C}(x)\leftarrow\mathsf{Act}(x).w_{x}$, $Y_{c}\leftarrow
Y_{c}\cup(x,w_{x})$ where . is concatenation operator.

    4. (d)

If $\mathsf{Appear}(q,C)=\\{C_{i_{q}},C_{j_{q}}\\}$: (Without loss of
generality, assume $q_{j_{q}}=q$ and $q_{i_{q}}=q^{\prime\prime}\neq q$). (/*
Then by lemma C.3 the value of the clock copies associated with $q$ generated
from $q^{\prime\prime}$ will be less than or equal to corresponding values of
the clock copies associated with $q$ generated from self-loop. Hence, if
$q\in\mathsf{Q^{\leq}}$ then, if the location $q$ generated from self-loop
reaches the accepting state then the $q$ generated from $q^{\prime\prime}$
will also reach the accepting state (vice-versa holds in case of
$q\in\mathsf{Q^{\geq}}$)*/). If $q\in\mathsf{Q^{\leq}}$: For all $x\in X$ do:
$L_{C}(q)(x)\leftarrow L(q)(x)$. If $q\in\mathsf{Q^{\geq}}$: Do Steps 2(b-c)
and continue.

  3. 3.

Let $G_{C}\leftarrow\emptyset$ (stores the guards corresponding to the clause
$C$). For all $g\in\mathcal{G}$ do:

    1. (a)

For all $C_{i}\in\mathsf{Appear}_{G}(g,C)$ do: $G_{c}=G_{c}\cup g^{i}$, where
$g^{i}=(x,L(q_{i})(x))\in I$ iff $g=x\in I$.

  4. 4.

return $Y_{C},L_{C},\mathsf{Act}_{C},G_{C}$. (/* There is a transition from
$q^{\prime}$ on resetting clocks $Y_{C}$, asserting guards $G_{C}$, to a
location $(L_{C},\mathsf{Act}_{C})$*/).

Hence,
$\Delta(q^{\prime},a)=\bigvee\limits_{C\in\mathbb{C}}(Y_{C}.(L_{C},\mathsf{Act}_{C})\wedge\bigwedge
G_{C})$. Similar reduction works for 1-${\text{ATA}^{0,\infty}}$.

The correctness of the above algorithm depends on the following proposition.

######  Proposition D.1.

$\mathbb{A}$ to $\mathsf{T}_{red}(A)$ are simulation equivalent. Hence,
$L(A)=L(\mathbb{A})$.

To prove the D.1, consider the relation $R$ between states of $\mathbb{A}$ and
$\mathsf{T}_{red}(A)$ as follows. $((L,\mathsf{Act}),\nu),C)\in R$ iff;
$(q,\nu^{\prime})\in C$ iff $L(q)\neq 0$ and for all $x\in X$,
$\nu(x,{L(q)(x)})=\nu^{\prime}(x)$. Notice $R$ and $R^{-1}$ are simulation
relations from states of $\mathbb{A}$ to that of $\mathsf{T}_{red}(A)$ and
vice-versa, respectively, by inspection of construction.

####  D.0.2 Worst Case Complexity:

Notice that the number of bits required to store a state of region automata is
the sum of (1) $B_{l}$ = Number of bits required to store any location
$(L,\mathsf{Act})$, and (2) $B$ = Number of bits required to store the region
information. Bits required to store $L=|Q|\times\log(|Q|)\times log(|X|)+1$
and that required to store
$\mathsf{Act}=|X|\times\log(e\times|Q|!)\leq|X|\times(|Q|\log|Q|+1)$ ($e$ is
the natural Euler’s Number). Hence, $B_{l}=O(|X|\times\log(|Q|)\times|Q|)$.
Moreover, $B=log(|Q|\times|X|)!\times\log(2\times c_{max}+1)$ where $c_{max}$
is the maximum constant used in the timing constraints in $\mathcal{G}$.
Hence, to store a state of region automata, we only need bytes polynomial in
the number of locations and clocks of $A$, proving membership of emptiness for
1-${\text{ATA}^{0,\infty}}$ and ${\text{VWATA}^{0,\infty}}$ in PSPACE. Notice
that the state containing the location $(L,\mathsf{Act})$ will only have to
store the region information clocks in $\mathsf{Act}$, i.e. active clocks,
which, in practice, could be significantly less than the worst case. Hence,
lazily spawning clock copies may result in NTA with much less number of clocks
than the worst case (i.e. $|X|\times|Q|$).