Revisiting Timed Logics with Automata Modalities
Hsi-Ming Ho





0000-0003-0387-4857

  University of Cambridge
  United Kingdom

hsi-ming.ho@cl.cam.ac.uk






It is well known that (timed) ω-regular properties such as `p holds at every even position'
	and `p occurs at least three times within the next 10 time units'
	cannot be expressed in Metric Interval Temporal Logic ()
	and Event Clock Logic ().
	A standard remedy to this deficiency is to extend these
	with modalities defined in terms of automata. 

	In this paper, we show that the logics _0, ∞  
	(adding non-deterministic finite automata modalities
	into the fragment of  with only lower- and upper-bound constraints)
	and  (adding automata modalities into )
	are already as expressive as
	 (full  with automata modalities).
	In particular, the satisfiability and model-checking problems for
	_0, ∞ and 
	are PSPACE-complete, whereas the same problems for 
	are EXPSPACE-complete.
	We also provide a simple translation from _0, ∞
	to diagonal-free timed automata, which
	enables practical satisfiability and model checking based on off-the-shelf tools. 








<ccs2012>
<concept>
<concept_id>10003752.10003753.10003765</concept_id>
<concept_desc>Theory of computation Timed and hybrid models</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10003790.10002990</concept_id>
<concept_desc>Theory of computation Logic and verification</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10003790.10011192</concept_id>
<concept_desc>Theory of computation Verification by model checking</concept_desc>
<concept_significance>500</concept_significance>
</concept>
</ccs2012>


[500]Theory of computation Timed and hybrid models
[500]Theory of computation Logic and verification
[500]Theory of computation Verification by model checking




Revisiting Timed Logics with Automata Modalities
    Hsi-Ming Ho
    December 30, 2023
================================================





§ INTRODUCTION
 




















  
Timed logics In the context of real-time systems verification, it is natural and desirable to add timing constraints to
Linear Temporal Logic () <cit.>
to enable reasoning about timing behaviours of such systems.
For instance, one may write ϕ_1 _I ϕ_2 to assert
that ϕ_1 holds until a `witness' point where ϕ_2 holds,
and the time difference between now and that point lies within the
constraining interval I.
The resulting logic, Metric Temporal Logic () <cit.>,
can be seen as a fragment of Monadic First-Order Logic of Order and Metric () <cit.>, the timed counterpart of the classical Monadic First-Order Logic of Order ().
There are, nonetheless, some loose ends in this analogy. For instance, while  is as expressive as  <cit.>, it is noted early on 
that certain `non-local' timing properties in , albeit being very simple,
cannot be expressed in timed temporal logics like  <cit.>. 
As a concrete example, the property `every p-event is followed by a q-event and, later, an r-event within the next 10 time units', written as the   formula

    ∀ x   (p(x) ⇒∃ y  (q(y) ∃ z  (r(z)  x ≤ y ≤ z ≤ x + 10)))

is not expressible in —indeed, no `finitary' extension of  can be expressively complete
for  <cit.>.[(<ref>) can, however, be expressed in  if the  continuous semantics of the logic is adopted
or past modalities are allowed; see <cit.> for details.]
A more serious practical concern 
is that the satisfiability problem for  is undecidable <cit.>. For this reason, research efforts have been 
focused on fragments of  with decidable satisfiability, most notably
Metric Interval Temporal Logic (), the fragment of  in which
`punctual' constraining intervals are not allowed <cit.>.
In particular,  formulae can be effectively translated into timed automata (s) <cit.>,
giving practical EXPSPACE decision procedures for its satisfiability and model-checking problems <cit.>. 



  
Automata modalities
It is well known that properties that are necessarily second order (e.g., `p holds at all even positions') cannot be expressed in  or .
Fortunately, it is possible to add automata modalities into
 
at no additional computational cost <cit.>.
In timed settings, the logic obtained from  by adding
time-constrained automata modalities defined by non-deterministic finite automata (s)
is called Extended Metric Interval Temporal Logic () <cit.>.
From a theoretical point of view,  is a fully decidable
formalism (i.e. constructively closed under all Boolean operations and with decidable satisfiability <cit.>)
whose class of timed languages strictly contains
that of  and Büchi automata.[A very recent paper of Krishna, Madnani, and Pandya <cit.> showed
that this class admits some alternative characterisations (namely, a syntactic fragment of s and
a timed monadic second-order logic).]
In practice, it can be argued that automata modalities are natural, easy-to-use
extensions of the usual  modalities. 







 






They also allow  properties like (<ref>), which often
emerge in application domains like healthcare and automotive engineering,
to be written as specifications.
[<cit.>]
Discrimination algorithms are implemented in implantable cardioverter defibrillators (ICDs)
to detect potentially dangerous heartbeat patterns. As a simple example, one may want to check
whether the number of heartbeats in one minute is between 120 and 150. This can be expressed
as the  <cit.> formula _[0, 59]^≥ 120 p ∧_[0, 59]^≤ 150 p
where p denotes a peak in the cardiac signal. The counting modalities
^∼ k_I (where 0 ∈ I, which is the case here),
as well as (<ref>), be expressed straightforwardly in terms of automata.

[adapted from <cit.>]
In autonomous driving, one may want to specify that 
a car overtaking another from the left must be done in 10 seconds.
Suppose the lane on the left is empty and the events are sampled sufficiently frequently (say 5ms), this can be expressed as 
the  formula _[0, 10] (, …)
(see  <ref> and  <ref>)
where  is the time to collision, 
 is the longitudinal distance between the two vehicles, and 
,  are the actions for merging to the left/right lane—these are taken immediately after 
and , respectively.




 












Compared with  and , however, translating  
into s is considerably more challenging.
The original translation by Wilke <cit.>
is non-elementary and thus not suitable for practical purposes.




Krishna, Madnani, and Pandya <cit.>
showed that any  formula can be encoded into an  formula of doubly exponential size (which can then be translated into a ),
but this does not match the EXPSPACE lower bound inherited from .
More recently, Ferrère <cit.> proposed an asymptotically optimal construction from  (Metric Interval Dynamic Logic,
which is strictly more expressive and subsumes ) formulae
to s, but it is very complicated and relies heavily on the use of diagonal constraints (i.e. comparison between clocks) which are, in general, not preferred in practice <cit.> and not well-supported by existing model checkers.[It is possible to obtain a diagonal-free  from an  formula
by first applying the construction in <cit.> and then removing the diagonal constraints <cit.>. 
This, however, is expensive and difficult to implement.]




  
Contributions

We consider a simple fragment of , which we call _0, ∞, obtained
by allowing only lower- and upper-bound constraining intervals (e.g., [0, a) and (b, ∞))
and  <cit.> (adding automata modalities to Event Clock Logic ).
The satisfiability and model-checking problems for _0, ∞ and  are much cheaper
than that of  (PSPACE-complete vs EXPSPACE-complete).
Moreover, we show that they are already as expressive as full —this is in sharp contrast with the situation for
`vanilla' _0, ∞/ and , where the latter is strictly more expressive
when interpreted over timed words <cit.>—making them
expressive yet tractable real-time specification formalisms.
We then show that _0, ∞
admits a much simpler translation into s. 




















Specifically, by effectively decoupling the timing
and operational aspects of automata modalities,
overlapping obligations imposed by a single automaton subformula
can be handled in a purely fifo manner
with a set of sub-components (each of which is a simple one-clock 
with a polynomial-sized symbolic representation),
avoiding the use of diagonal constraints altogether.[For simplicity
we focus on logics with only future modalities, but our results readily carry over to the versions with both future and past modalities,
thanks to the compositional nature of our construction (cf. e.g., <cit.>).]
This makes our construction better suited to be implemented
to work with existing highly efficient algorithmic back ends (e.g., Uppaal <cit.> and
LTSmin <cit.>).





















 



  
Related work
The idea of extending  to capture the full class
of ω-regular languages dates back to the seminal works of Clarke, Sistla, Vardi, and
Wolper <cit.> in the early 1980s.
In particular, it is shown that  with  modalities—which
essentially underlies various industrial specification languages
like ForSpec <cit.> and PSL <cit.>—are expressively equivalent to Büchi automata,
yet the model-checking and satisfiability problems remain
PSPACE-complete, same as .[There are other ways to extend  to achieve
ω-regularity, e.g., adding monadic second-order quantifiers
( <cit.>) or
least/greatest fixpoints ( <cit.>).
These formalisms unfortunately suffer from higher complexity or less readable syntax.]


Our approach generalises the construction in <cit.>
in the case of finite acceptance.

Henzinger, Raskin, and Schobbens <cit.>
proved a number of analogous results in timed settings; in particular, 
they showed that in the continuous semantics (i.e. over finitely variable signals),
(i) _0, ∞ and  are as expressive as , and (ii)
the fragment of  with unconstrained automata modalities 
is as expressive as recursive event-clock automata,
and the verification problems for this fragment can be solved in EXPSPACE.





Our results can be seen as counterparts 
in the pointwise semantics (i.e. over timed words). 












































Besides satisfiability and model checking, extending timed logics with
automata or regular expressions is also a topic of great interest in
runtime verification.
Basin, Krstić, and Traytel <cit.>
showed that  with time-constrained regular-expression modalities admits an efficient runtime monitoring procedure in a pointwise, integer-time setting.
A very recent work of Ničković, Lebeltel, Maler, Ferrère, and Ulus <cit.>
considered a similar extension of  with timed regular expressions
() <cit.> in the context of monitoring and analysis of Boolean and real-valued signals. 



§ TIMED LOGICS AND AUTOMATA




  
Timed languages



A timed word over a finite alphabet Σ is an infinite sequence
of events (σ_i,τ_i)_i ≥ 1 over
Σ×_≥ 0 with (τ_i)_i≥ 1 a non-decreasing
sequence of non-negative real numbers such that for each r ∈_≥ 0,
there is some j ≥ 1 with τ_j ≥ r (i.e. we require all timed words
to be `non-Zeno').
We denote by TΣ^ω the set of all timed words over Σ. A timed language is a
subset of TΣ^ω.






  
Extended timed logics 
A non-deterministic finite automaton () over Σ
is a tuple = ⟨Σ, S, s_0,, F ⟩
where S is a finite set of locations, s_0 ∈ S is the initial location,
⊆ S ×Σ× S is the transition relation,
and F is the set of final locations.
We say that  is deterministic (a ) iff for each s ∈ S
and σ∈Σ, | { (s, σ, s') | (s, σ, s') ∈} | ≤ 1. 
A run of  on σ_1 …σ_n ∈Σ^+
(without loss of generality, we only consider runs of automata modalities over nonempty finite words in this paper) is a
sequence of locations s_0 s_1 … s_n where 
there is a transition (s_i,σ_i+1,s_i+1) ∈
for each i, 0 ≤ i < n.  A run of  is accepting iff
it ends in a final location. A finite word is accepted by 
iff  has an accepting run on it.
We denote by  the set of finite words accepted by .

Extended Metric Interval Temporal Logic () formulae over
a finite set of atomic propositions 
are generated by  


  ϕ:= ⊤|p |ϕ_1 ϕ_2 |ϕ|_I(ϕ_1, …, ϕ_n)

where p∈,  is an  over the n-ary alphabet { 1, …, n },

and I ⊆_≥ 0 is a non-singular interval with endpoints in _≥ 0∪{∞}.[For notational simplicity,
we will occasionally use ϕ_1, …, ϕ_n directly as transition labels (instead of 1, …, n).]
As usual, we omit the subscript I when I = [0, ∞) and write pseudo-arithmetic expressions for lower
or upper bounds, e.g., `< 3' for [0, 3).
We also omit the arguments ϕ_1, …, ϕ_n
and simply write _I, if clear from the context.

Following <cit.>, we consider
the pointwise semantics of  and interpret
formulae over timed words: given an  formula ϕ over , 
a timed word ρ=(σ_1,τ_1)(σ_2,τ_2)… over Σ_ = 2^ and
a position i ≥ 1,


  * (ρ, i)⊤;

  * (ρ, i) p iff p∈σ_i;

  * (ρ, i)ϕ_1ϕ_2 iff (ρ,i)ϕ_1 and 
(ρ,i)ϕ_2;

  * (ρ,i)ϕ iff (ρ,i)ϕ;





  * (ρ,i)_I(ϕ_1, …, ϕ_n) iff there exists
  j≥ i such that (i) τ_j-τ_i∈ I and (ii) there is an
accepting run of  on a_i … a_j where a_ℓ∈{1, …, n}
and (ρ, ℓ) ϕ_a_ℓ  for each ℓ, i ≤ℓ≤ j.[Note that
it is possible for (ρ,i)_I(ϕ_1, …, ϕ_n) and (ρ,i) ^c_I(ϕ_1, …, ϕ_n),
where ^c is the complement of , to hold simultaneously.]

The other Boolean operators are defined as usual:
≡⊤,
ϕ_1ϕ_2 ≡(ϕ_1ϕ_2),
and ϕ_1⇒ϕ_2 ≡¬ϕ_1ϕ_2.
We also define the dual automata modalities
_I(ϕ_1, …, ϕ_n) ≡_I(ϕ_1, …, ϕ_n).







With the dual automata modalities, we can transform every
 formula ϕ into negative normal form, i.e. an  formula using
only atomic propositions, their negations, and the operators ,
, _I, and Ã_I.
It is easy to see that the standard  `until' ϕ_1 _I ϕ_2
can be defined in terms of automata modalities.
We also use the usual shortcuts like
_Iϕ≡⊤_Iϕ, 
_Iϕ≡_Iϕ,
and ϕ_1_I ϕ_2 ≡((ϕ_1)_I(ϕ_2)).
We say that ρ satisfies ϕ (written ρϕ)
iff (ρ,1)ϕ, and we write
ϕ for the timed language of ϕ, i.e. the set of all timed words satisfying ϕ.
_0, ∞ is the fragment of  where all constraining
intervals I must be lower or upper bounds (e.g., < 3 or ≥ 5).
Extended Event Clock Logic () is the fragment of 
where _I is replaced by a more restricted `event-clock' counterpart:


  * (ρ,i)▹_I(ϕ_1, …, ϕ_n) iff 
(i) there is a minimal position j ≥ i such that  has an accepting run on a_i … a_j where a_ℓ∈{1, …, n}
and (ρ, ℓ) ϕ_a_ℓ  for each ℓ, i ≤ℓ≤ j; and
(ii) j satisfies τ_j-τ_i∈ I. 










  
Timed automata
Let X be a finite set of clocks
(_≥ 0-valued variables).
A valuation v for X maps each clock x ∈ X to a value in _≥ 0.
We denote by 0 the valuation that maps every clock to 0,
and we write the valuation simply as a value in _≥ 0
when X is a singleton.
The set (X) of clock constraints g over X is generated
by g:= ⊤| g g | x⋈ c where
⋈∈{≤,<,≥,>}, x∈ X, and c∈_≥ 0.
The satisfaction of a clock constraint g by a valuation v (written v  g) is
defined in the usual way, and we write g for the set of valuations v satisfying g.





For t∈_≥ 0, we let v +t
be the valuation defined by (v +t)(x) = v (x)+t for all x∈
X. For λ⊆ X, we let v [λ← 0] be the valuation
defined by (v[λ← 0])(x) = 0 if x∈λ, and
(v[λ← 0])(x) = v (x) otherwise.




A timed automaton () over Σ is a tuple
= ⟨Σ, S, s_0, X, , ⟩ where S is a finite set of
locations, s_0 ∈ S is the initial location, X is a finite set of clocks,
⊆ S ×Σ×(X) ×
2^X × S is the transition relation,





and ={F_1,…,F_n}, with F_i⊆ S for all i, 1≤ i ≤ n,
is the set of sets of final locations.[We adopt 
generalised Büchi acceptance  for technical convenience; 
indeed, any  with a generalised Büchi acceptance condition can be converted into a
classical Büchi  via a simple standard construction <cit.>.]
We say that  is deterministic (a ) iff for each s ∈ S and σ∈Σ and
every pair of transitions (s, σ, g^1, λ^1, s^1) ∈ and (s, σ, g^2, λ^2, s^2) ∈, g^1  g^2 is not satisfiable.
A state of  is a pair (s, v)
of a location s ∈ S and a valuation v for X.
A run of  on a timed word
(σ_1,τ_1)(σ_2,τ_2)⋯∈ TΣ^ω is a
sequence of states (s_0,v_0)(s_1,v_1)… where (i)
v_0=0 and (ii) for each i≥ 0,
there is a transition (s_i,σ_i+1,g,λ,s_i+1)
such that 
v_i +(τ_i+1-τ_i) g (let τ_0=0) and
v_i+1 =(v_i +(τ_i+1-τ_i))[λ← 0]. 
A run of  is accepting iff
the set of locations it visits infinitely often contains at least
one location from each F_i, 1≤ i≤ n. A timed word
is accepted by  iff  has an accepting run on it.
We denote by  the timed language accepted by .
For two s ^1 = ⟨Σ,S^1,s_0^1,X^1,^1,^1 ⟩ and
^2 = ⟨Σ,S^2,s_0^2,X^2,^2,^2 ⟩ over a
common alphabet Σ, the (synchronous) product 
^1 ×^2 is defined as the  ⟨Σ,S,s_0,X,,⟩
where (i) S=S^1 × S^2, s_0 = (s_0^1, s_0^2), and X = X_1 ∪ X_2;
(ii) ((s^1_1,s^2_1),σ,g,λ,(s^1_2,s^2_2))∈
iff there exists (s^1_1,σ,g^1,λ^1,s^1_2)∈^1
and (s^2_1,σ,g^2,λ^2,s^2_2)∈^2 such that
g=g^1 g^2 and λ = λ^1 ∪λ^2;
and (iii) let ^1={F_1^1,…,F_n^1}, ^2={F_1^2,…,F_m^2}, then
= {F_1^1 × S^2,…,F_n^1× S^2, S^1×
F_1^2,…,S^1× F_m^2}. Note in particular that we have ^1 ×^2 = ^1∩^2.


  
Consider the  over Σ_{p,q} in  <ref>
(following the usual convention, we omit transition labels when they are ⊤'s and use Boolean formulae over atomic propositions to represent letters,
e.g., here p  q stands for {σ∈Σ_{p,q}| p ∈σ, q ∉σ}). It non-deterministically pick an event where p holds but q does not hold (thus
_≤q is not fulfilled immediately) and enforces that q does not hold
in the next time unit. In other words, it accepts (p ∧_≤ 1( q)) = (p⇒_≤ 1q).





  
Alternation One-clock
alternating timed automata (s) extend
one-clock timed automata with the power of
universal choice. Intuitively, a transition of an 
may spawn several copies of the automaton that run in parallel from the
targets of the transition; a timed word is accepted iff
all copies accept it.
Formally, for a set S of
locations, let Γ(S) be the set of formulae defined by


    γ := ⊤||γ_1 γ_2|γ_1 γ_2
      | s | x⋈ c| x.γ
 
where x is the single clock, c∈_≥ 0, ⋈∈{≤,<,≥,>}, and
s ∈ S (the construct x. means “reset x”). For a formula γ∈Γ(S), let its dual γ∈Γ(S)
be the formula obtained by applying


  * ⊤ =; = ⊤;

  * γ_1 γ_2 = γ_1γ_2;
		γ_1 γ_2 = γ_1γ_2;

  * s = s; x ⋈ c =  (x ⋈ c); x.γ = x.γ.

An  over Σ is a tuple =⟨Σ, S, s_0, , F ⟩
where S is a finite set of locations, 
s_0 ∈ S is the initial location,
S×Σ→Γ(S) is the transition
function, and F ⊆ S is the set of final locations.







A state of  is a pair (s,v) of a location s ∈ S and
a valuation v for the single clock x.
Given a set of states M, a formula γ∈Γ(S)
and a clock valuation v, we define


  * M_v ⊤; M_v ℓ iff (ℓ,v)∈ M;
  M_v x⋈ c iff v⋈ c; ;

  * M_v γ_1γ_2 iff M_v γ_1
  and M_v γ_2;

  * M_v γ_1γ_2 iff M_v γ_1
  or M_v γ_2.




We say that M is a model of γ with respect
to v iff M _v γ.[Note that _v is monotonic: if M ⊆ M' and M _v γ then M' _v γ.]




A run of  on a timed word
(σ_1,τ_1)(σ_2,τ_2)…∈ TΣ^ω is a
rooted directed acyclic graph (DAG) G=⟨ V, →⟩ with vertices of the
form (s,v,i)∈ S×_≥ 0×_≥ 0, (s_0,0,0) as the root,
and edges as follows: for every vertex (s,v,i), there is a

model M of the formula (s,σ_i+1)
with respect to v+(τ_i+1-τ_i) (again, τ_0=0) such that
there is an edge (s,v,i) → (s',v',i+1) for every state (s',v') in M.
A run G of  is accepting iff
every infinite path in G visits F infinitely often.


A timed word is accepted by 
iff  has an accepting run on it. We denote by  the timed language accepted by .
For convenience, in the sequel we will regard s as
(untimed) s with finite acceptance conditions and
whose transition functions are simply disjunctions over locations.






























  
  
  Consider the  over Σ_{p,q} in  <ref>
	which accepts (p⇒_≤ 1q).


	A run of it on 
(∅,0.42)({p},0.42)({q},0.7)⋯
	is depicted in  <ref> where the root is
  (s_0,0,0). This vertex has a
  single successor (s_0,0.42,1), which in turn has two successors
  (s_0,0.42,2) and (s_1,0,2) (after firing the
  transition (s_0, {p}) = s_0 ∧ x.s_1). Then, (s_1,0,2) has no successor
  since the empty set is a model of (s_1, {q}) = x ≤ 1 with respect to 0.28. 






  
Verification problems In this work we are concerned with the following standard
verification problems. Given an  formula ϕ, the satisfiability problem
asks whether ϕ = ∅. Given a   and
an  formula ϕ, the  model-checking problem asks whether
⊆ϕ. As s are closed under intersection and
the emptiness problem for s is decidable, both problems above
can be solved by first translating ϕ into an equivalent  _ϕ.
























































































§ EXPRESSIVENESS


In this section we study the expressiveness of  
_0, ∞, , and a `counting' extension of .
It turned out that the class of timed languages captured by
 is robust in the sense that it remains the same
under all these modifications.
For the purpose of the proofs below, let us assume (without loss of generality) that
the automaton = ⟨Σ, S, s_0, , F ⟩ in question is a 
and at most one of ϕ_1, …, ϕ_n may hold at any position in a given timed word <cit.>.




  
Counting in intervals
Recall that the constraining intervals I in the
counting modalities in  <ref>
satisfy 0 ∈ I; this non-trivial extension of  (and ) was first considered by
Hirshfeld and Rabinovich <cit.>.
For the case of timed words, it is shown in <cit.> that allowing arbitrary I (e.g., (1, 2))
makes the resulting logic even more expressive. 
Here we show that, by contrast, adding the ability to count in I—regardless of whether 0 ∈ I—does not increase the expressive power of .[As  can easily express the `until with threshold' modalities of ,
the latter is clearly subsumed by .]
We consider an extention of  (which we call )
that enables specifying the number of positions within a given interval I from now at which final locations can be reached.
More precisely, we have the following semantic clause in :


  * (ρ,i)^≥ k_I(ϕ_1, …, ϕ_n) iff there exists
  j_1 < … < j_k such that for each ℓ, 1 ≤ℓ≤ k, (i) j_ℓ≥ i; (ii) τ_j_ℓ-τ_i∈ I; and (iii) there is an
accepting run of  on some a_i … a_j_ℓ where a_ℓ'∈{1, …, n}
and (ρ, ℓ') ϕ_a_ℓ' for each ℓ', i ≤ℓ' ≤ j_ℓ.  






 and  are equally expressive over timed words.


We give an  equivalent of ^≥ k_I(ϕ_1, …, ϕ_n).
Provided that ϕ_1, …, ϕ_n are already in  and  is deterministic
in the sense above, we can count modulo k the number of positions
where final locations are reached and ensures that I encompasses all possible values of the counter;
in contrast to <cit.>, here the counter can be implemented directly using automata modalities.
We give a concrete example which should illustrate the idea.
Let k = 3 and ^2 be the product of  and ^1 ( <ref>),
i.e. each location of ^2 is of the form ⟨ s, s^1 ⟩ where s ∈ S and s^1 ∈{s_0^1, s_1^1, s_2^1 },
and it is accepting iff s and s^1 are both final.
Then, let ^3 be the automaton obtained from ^2
by:


  * For all the transitions ⟨ s, s_0^1 ⟩→⟨ s', s_1^1 ⟩,
⟨ s, s_1^1 ⟩→⟨ s', s_2^1 ⟩,
and ⟨ s, s_2^1 ⟩→⟨ s', s_0^1 ⟩,
keeping only those with s' ∈ F;

  * For all the transitions ⟨ s, s_0^1 ⟩→⟨ s', s_0^1 ⟩,
⟨ s, s_1^1 ⟩→⟨ s', s_1^1 ⟩,
and ⟨ s, s_2^1 ⟩→⟨ s', s_2^1 ⟩,
keeping only those with s' ∉ F.

Now let ^1,ℓ (ℓ∈{0, 1, 2}) be the automaton
obtained from ^1 by adding an extra final location s^1_F
and the transition s^1_ℓ - 1 (mod 3)→ s^1_F,
and let ^3,ℓ be the corresponding product with ,
keeping transitions ⟨ s, s_ℓ - 1 (mod 3)^1 ⟩→⟨ s', s_F^1 ⟩
with s' ∈ F. The original formula _I^≥ 3 is equivalent
to ⋀_ℓ∈{0, 1, 2}^3, ℓ_I.





  
Restricting to event clocks



We show that the equivalence of  and _0, ∞
carries over to the current setting. 
More specifically, an  formula can be translated
into an equilvalent _0, ∞ formula of polynomial size (in DAG representation).
On the other hand, our translation from _0, ∞
to  induces an exponential blow-up due to the fact that
automata  have to be determinised.


 and _0, ∞ are equally expressive over timed words.


Again, we assume that the arguments ϕ_1, …, ϕ_n are already in the target logic.
The direction from  to _0, ∞ is simple and almost identical
to the translation from  to _0, ∞; for example, ▹_(3, 5)
can be written as _<5∧_≤ 3. For the other direction
consider the following _0, ∞ formulae:


  * (ρ, i) _≤ c: the equivalent formula is simply ▹_≤ c.

  * (ρ, i) _≥ c: as in <cit.>, we consider the subcases where:


  * There is no event in [τ_i, τ_i + c) apart from (σ_i, τ_i):
let ^2 be the product of  and ^1 where ^1 is the automaton depicted in  <ref>.  
We have (ρ, i) [0ex]▹^1_<c∧[0ex]▹^2_≥ c.


  * There are events in [τ_i, τ_i + c) other than (σ_i, τ_i):
let the last event in [τ_i, τ_i + c) be (σ_j, τ_j)
and k > j > i be the minimal position such that there exists
a_i … a_k ∈ with (ρ, ℓ) ϕ_a_ℓ for all ℓ, i ≤ℓ≤ k.
By assumption, a_i … a_k is unique and  must reach a  
specific location s ∈ S after reading a_i … a_j.
The idea is to split the unique run of  on a_i … a_k
at s: we take a disjunction over all possible s ∈ S,
enforce that τ_j - τ_i < c and  reaches
a final location from s by reading a_j+1… a_k.
More specifically, let ^s, ϕ be the automaton obtained from 
by adding a new location s_F, declaring it as the only final location,
and adding new transitions s'  s_F
for every s'  s in .




Let ^s be the automaton obtained from  by adding new non-final locations s_0' and s_1',
adding new transitions s_0' → s_1'
(i.e. labelled with ⊤) and s_1'  s”
for every s  s” in ,
removing outgoing transitions from all the final locations, and finally 
setting the initial location to s_0'.
We have (ρ, i) [0ex]▹^1_<c∧▹∧⋁_s ∈ S[0ex]▹^s, ϕ_<c
where ϕ = ^s. 

The equivalent formula is the disjunction of these.

The other types of constraing intervals, such as [0, c), are handled almost identically.







  
Restricting to one-sided constraining intervals
Recall that a fundamental stumbling block in the algorithmic analysis of s
is that the universality problem is undecidable <cit.>.
s with finite acceptance conditions, on the other hand, can be complemented easily and
have a decidable universality problem. 
This raises the question of whether one can extend  with  modalities
without losing decidability (both are fully decidable formalisms).


Perhaps surprisingly, the resulting formalism already subsumes 
even when punctual constraints are disallowed.
For example, _[d, d]ϕ can be written as
' ”_[1, ∞)ϕ
where ' and ” are the one-clock deterministic s
in  <ref> and  <ref>, respectively
(in particular, note that ' and ” only use lower- and upper-bound constraints).
It follows from <cit.> that the satisfiability problem 
for this formalism is undecidable.




















Based on a similar trick, we obtain the main result of this section: 
_0, ∞ already has the full expressive power of . 


This, together with the fact that the satisfiability and model-checking problems
for _0, ∞ are only PSPACE-complete
(Theorem <ref>) as compared with EXPSPACE-complete for full  <cit.>, makes _0, ∞ a
competitive alternative to other real-time specification formalisms—while a translation from  to _0, ∞
inevitably induces at least an exponential blow-up, it can be argued that many properties of practical interest
can be written in _0, ∞ directly (e.g.,  <ref>
and  <ref>).
The idea of the proof below is similar to that of <cit.>
(_0, ∞ and  are equally expressive in the continuous semantics),
but the technical details are more involved 
due to automata modalities and the fact that 
each event is not necessarily preceded by another one exactly 1 time unit earlier
in a timed word;
the latter is essentially the reason why
the expressive equivalence of _0, ∞ and  fails to hold in the pointwise semantics.


_0, ∞ and  are equally expressive over timed words.


We explain in detail below how to write the  formula _(c, c+1) (ϕ_1, …, ϕ_n) where
c ≥ 0, and ϕ_1, …, ϕ_n  ∈_0, ∞
as an _0, ∞ formula; the other cases, such as (c, c+1] 
and [c, c+1], are similar.




First consider c = 0. If (ρ, i) _(0, 1)
for ρ = (σ_1, τ_1)(σ_2,τ_2)… and i ≥ 1, the finite word
a_i … a_k accepted by  must be at least two letters long.
This again is enforced by ^1 in  <ref>:
let ^2 be the product of  and ^1.
Then, let ^3 be the automaton obtained from ^2
by adding _> 0⊤ ( is the standard  `next' operator <cit.>) to all the transitions ⟨ s, s_0^1 ⟩→⟨ s', s_0^1 ⟩ and _> 0⊤
to all the transitions ⟨ s, s_0^1 ⟩→⟨ s', s_1^1 ⟩ as conjuncts
(in doing so, extend the alphabet as necessary).
It is not hard to see that (ρ, i) ^3_< 1
in the two possible situations:
(i) τ_i+1 - τ_i > 0 and
(ii) τ_j - τ_i > 0 for some j > i + 1 and τ_ℓ - τ_i = 0 for all ℓ, i < ℓ < j.
The other direction ((ρ, i) ^3_< 1⇒ (ρ, i) _(0, 1)) is straightforward.
It follows that the equivalent _0, ∞ formula is ^3_< 1.











Now consider c > 0.
Suppose that (ρ, i) _(c, c + 1)
for ρ = (σ_1, τ_1)(σ_2,τ_2)… and i ≥ 1,
let k > i be the minimal position such that
τ_k - τ_i ∈ (c, c+1) and there exists a_i … a_k ∈
with (ρ, ℓ) ϕ_a_ℓ for all ℓ, i ≤ℓ≤ k
(since at most one of ϕ_1, …, ϕ_n may hold at any position, we fix
a_i … a_k below). 
Consider the following cases (note that they are not mutually disjoint):


  * There exists a maximal j, i < j < k such that (a) τ_k - τ_j = 1 
and (b) there is no ℓ, j < ℓ < k such that a_i … a_ℓ∈
with (ρ, ℓ') ϕ_a_ℓ' for all ℓ', i ≤ℓ' ≤ℓ
( <ref>): 
we take a disjunction over all possible s ∈ S such that 
reaches s after reading a_i … a_j and
enforce that τ_j - τ_i ∈ (c - 1, c) (which we can, by the IH),
  reaches a final location from s by reading a_j+1… a_k, and τ_k - τ_j = 1;
thanks to (b), the last condition, which is otherwise inexpressible in _0, ∞,
can be expressed as a conjunction of two formulae labelled with ≤ 1 and ≥ 1.
To this end, we use ^s, ϕ and ^s as defined in the proof
of Theorem <ref>: we have  

    (ρ, i) ϕ^1 = ⋁_s ∈ S^s, ϕ_(c-1, c)

where ϕ = ^s_≤ 1^s_≥ 1.


  * There exists j, i < j < k such that τ_k - τ_j < 1, 
τ_j - τ_i ∈ (c-1, c], and a_i … a_j ∈
with (ρ, ℓ) ϕ_a_ℓ for all ℓ, i ≤ℓ≤ j ( <ref>): let ^s be the automaton obtained from 
in the same way as ^s except that we do not remove outgoing transitions
from the final locations.
Regardless of whether there is a event at τ_k - 1, 
it is clear that every position ℓ with τ_ℓ - τ_i ∈ (c - 1, c] must 
satisfy _(0, 1)^s where s is
the location of  after reading a_i … a_ℓ.



We have 

    (ρ, i) ϕ^2 = _(c-1, c]⋁_s ∈ S^s, ϕ_(c-1, c]

where ϕ = ^s_(0, 1).


  * There exists 
j, i < j < k such that τ_k - τ_j < 1, 
τ_j - τ_i ∈ (c-1, c], but 

there is no ℓ, i < ℓ < k such that (a) τ_ℓ - τ_i ∈ (c-1, c]
and (b) a_i … a_ℓ∈
with (ρ, ℓ') ϕ_a_ℓ' for all ℓ', i ≤ℓ' ≤ℓ: 
we have 

    (ρ, i) ϕ^3 = _(c-1, c]∧⋁_s ∈ S^s, ϕ_(c-1, c]

where ϕ = ^s_(0, 1).


  * There exists a maximal j, i < j < k such that τ_k - τ_j > 1, τ_j - τ_i ∈ (c-1, c],
and there is no ℓ, j < ℓ < k such that (a) τ_ℓ - τ_i ∈ (c-1, c]
and (b) a_i … a_ℓ∈
with (ρ, ℓ') ϕ_a_ℓ' for all ℓ', i ≤ℓ' ≤ℓ:
observe that (provided that s's are correctly instantiated to the locations  reaches
as it reads a_i … a_k)
while ^s_>1 
may hold arbitrarily often in [τ_i, τ_i + c],
the number of positions ℓ, i ≤ℓ≤ j satisfying

    (ρ, ℓ) ^s_>1∧ (ρ, ℓ + 1) (^s_≤ 1∨ (^s_> 1∧ s ∈ F))

is at most c
(since any two of such positions must be separated by more than 1 time unit).

We define a family of automata modalities {^m | m ≥ 1 } such that
each location of ^m is of the form ⟨ s, d ⟩
with s ∈ S and 1 ≤ d ≤ 2m; see  <ref> for an illustration. 
Each transition updates the s-component as  would, enforces the formula labelled on the corresponding transition of 
and, additionally, the formula as labelled in  <ref> (with s being the target location of
the corresponding transition of ).
The formula ϕ^s (illustrated in  <ref>), which also follows 
with an s-component, checks that the next position either satisfies (a) s ∈ F, 
or (b) ^s_≤ 1 holds continuously until s ∈ F eventually holds.
Let ^m be obtained from ^m by `inlining' ϕ^s: removing the leftmost locations of 
ϕ^s and merge the middle locations of ϕ^s with the rightmost locations of ^m.
Apparently, ^m and ^m are equivalent if there is no constraing interval—the only
difference between them is which position is `timed'.
Now suppose that the number of positions ℓ, i ≤ℓ≤ j satisfying (<ref>) is m. 
Since j is the last of these positions, we have (ρ, i) ^m_< c + 1.
On the other hand, as there are only m - 1 such positions in [τ_i, τ_i + c - 1],
we have (ρ, i) ^m_≤ c - 1.
By the above, we have

    (ρ, i) ϕ^4 = ⋁_1 ≤ m ≤ c(^m_< c + 1^m_≤ c - 1)  .








  * There is no event in (τ_i + c -1, τ_i + c]: We have 

    (ρ, i) ϕ^5 = _(c-1, c]⊤ϕ'  .

If c = 1 then ϕ' can simply be taken as _(0, 2),
which is equivalent to ^3_< 2 by the same argument as before.
If c > 1, then ϕ' can be taken as

    ⋁_1 ≤ m ≤ c - 1(^m_< c + 1^m_≤ c - 2) ∨ϕ”

where ϕ” is

    _(c-2, c-1]⊤∧⋁_1 ≤ m ≤ c - 2(^m_< c + 1^m_≤ c - 3) ∨ϕ”'  .

Intuitively, the former part of ϕ' is used to handle the case when
there is (at least) a event in (τ_i + c-2, τ_i + c-1], and
the former part of ϕ” is for (τ_i + c-3, τ_i + c-2],
and so on.









We omit the other direction as it is (more or less) straightforward.
The equivalent _0, ∞ formula is ϕ^1 ∨ϕ^2 ∨ϕ^3 ∨ϕ^4 ∨ϕ^5.




§ FROM _0, ∞ TO TIMED AUTOMATA





  
Embedding  formulae into s
We give a translation from a given  formula ϕ over  (which we assume to be in negative normal form)
into an  _ϕ = ⟨Σ_, S, s_0, , F ⟩ 
such that _ϕ = ϕ.
While this mostly follows the lines of the translation for  (and ) in <cit.>,
it is worth noting that the 
resulting  _ϕ is weak <cit.>
but not necessarily very-weak <cit.> due to the presence of automata modalities.


The set of locations S of _ϕ
contains (i) s^init; 
(ii) all the locations of  for every subformula _I(ϕ_1, …, ϕ_n);
(iii) all the locations of  for every subformula _I(ϕ_1, …, ϕ_n). 
The initial location s_0 is s^init, and the final locations F are all the locations
of  for every subformula _I(ϕ_1, …, ϕ_n). Finally, 
for each σ∈Σ_,  is defined inductively as follows (let = ⟨Σ^, S^, s_0^, ^, F^⟩ with Σ^ = {1, …, n}):


  * (s^init,σ)=x.(ϕ,σ),
  (⊤,σ)=⊤, and
  (,σ)=;

  * (p,σ) = ⊤ if p∈σ,
  (p,σ)= otherwise;

  * (¬ p,σ) = ⊤ if p∉σ,
  (¬ p,σ)= otherwise;

  * (ϕ_1ϕ_2,σ)=(ϕ_1,σ)(ϕ_2,σ), and
  (ϕ_1ϕ_2,σ)=(ϕ_1,σ)(ϕ_2,σ);

  * (_I(ϕ_1, …, ϕ_n),σ)= x.(s_0^, σ);

  * (s^,σ)= ⋁_a ∈Σ^( (ϕ_a , σ) ^[s_F^← s^_F  x ∈ I](s^, a) ) where s^∈ S^ and ^[s_F^← s^_F  x ∈ I] is obtained from ^ by substituting every s_F^∈ F^ with
s_F^ x ∈ I for some subformula _I(ϕ_1, …, ϕ_n);

  * (_I(ϕ_1, …, ϕ_n),σ)= x.(s_0^, σ);

  * (s^,σ)= ⋀_a ∈Σ^( (ϕ_a , σ) ^[s_F^← s^_F  x ∉ I](s^, a) ) where s^∈ S^ and ^[s_F^← s^_F  x ∉ I] is obtained from ^ by substituting every s_F^∈ F^ with
s_F^ x ∉ I for some subformula _I(ϕ_1, …, ϕ_n).



Given an  formula ϕ in negative normal form, .








 
We now focus on the case where ϕ is an _0, ∞ formula
and give a set of component s whose product  
`implements' the corresponding  _ϕ.
As we will need some notions from <cit.>,
we briefly recall them here to keep the paper self-contained.








  
Compositional removal of alternation in ϕ


Let Φ be the set of temporal subformulae (i.e. whose outermost
operator is _I or Ã_I) of ϕ.  We introduce
a new atomic proposition p_ψ for each ψ∈Φ
(the trigger for ψ)
and let _Φ = { p_ψ|ψ∈Φ}.








For a timed word ρ' over Σ_∪_Φ,
we denote by _(ρ') the timed word obtained from ρ'
by hiding all p ∉ (i.e. p ∈_Φ).
For a timed language  over ∪_Φ
we write _() = {_(ρ') |ρ' ∈}.
Let ψ be the formula obtained from an _0, ∞ formula ψ (in negative normal form) by replacing all of its 
top-level temporal subformulae by their corresponding triggers, 
i.e. ψ is defined
inductively as follows (where p∈):


  * ψ_1ψ_2 =ψ_1ψ_2;


  * ψ_1ψ_2 =ψ_1ψ_2;

  * ψ= ψ when ψ is ⊤ or  or  p or  p;

  * ψ= p_ψ when ψ is _I(ϕ_1, …, ϕ_n)  or _I(ϕ_1, …, ϕ_n).

Note that ψ is simply a positive Boolean combination of atomic propositions.
In this way, we can turn the given _0, ∞ formula ϕ into
an equisatisfiable _0, ∞ formula ϕ' over ∪_Φ: 
the conjunction of ϕ, 

    ⋀_{ψ∈Φ|ψ = _I(ϕ_1, …, ϕ_n) }(p_ψ⇒_I(ϕ_1, …, ϕ_n))  ,
   
and the counterparts for {ψ∈Φ|ψ = _I(ϕ_1, …, ϕ_n) }.
Finally, we construct the component s ^init (which accepts ϕ)
and ^ψ (which accepts, say, (p_ψ⇒_I(ϕ_1, …, ϕ_n))) for every ψ∈Φ.
The timed language of ϕ' is accepted by the product
^init×∏_ψ∈Φ^ψ and, in particular, _(^init×∏_ψ∈Φ^ψ) = _ϕ.
Intuitively, p_ψ being ⊤ (the trigger p_ψ is `pulled')
at some position means that the  _ϕ spawns a copy (several copies)
of  where ψ = _I (ψ = _I) at this position or,
equivalently, an obligation that _I (_I) must hold
is imposed on this position. 
 
















 



































































































































  
Component s for automata modalities
As the construction of ^init is trivial,
we only describe the component s ^ψ for ψ = _I(ϕ_1, …, ϕ_n) and ψ = _I(ϕ_1, …, ϕ_n)
where I = [0, c] or I = [c, ∞) for some c ∈_≥ 0;
the other types of constraining intervals are handled similarly. 
The crucial observation that allows us to bound the number of clocks needed
in ^ψ is that two or more obligations, provided that
their corresponding copies
of  are in the same location(s) at some point(s)
and I is a lower or upper bound,
can be merged into a single one.
Instead of keeping track of the order of the values of its clocks,
^ψ non-deterministically guesses how obligations
should be merged and put them into suitable sub-components accordingly.
To ensure that all obligations are satisfied, we use an extra
variable ℓ such that ℓ = 0 when there is no obligation,
ℓ = 1 when there is at least one pending obligation,
ℓ = 2 when the pending obligations have just been
satisfied and a new obligation has just arrived, and finally
ℓ = 3 when we have to wait the current obligations to be satisfied
(explained below).
In all the cases below we fix Σ = Σ_∪_Φ and |S^| = m.
We write S^src S^tgt,
where S^src and S^tgt are two subsets of S^, iff
S^tgt is a minimal set such that
for each s^, 1∈ S^src, there is a transition
s^, 1 s^, 2 (where a ∈{1, …, n})
of 
with σϕ_a and s^, 2∈ S^tgt.
Similarly, we write S^src S^tgt iff
S^tgt is a minimal set such that
for each s^, 1∈ S^src and each transition
s^, 1 s^, 2 (where a ∈{1, …, n}) of , either s^, 2∈ S^tgt or σϕ_a.




  
ψ = _≤ c
Let C^ψ = ⟨Σ, S, s_0, X, , ⟩ be defined as follows
(to simplify the presentation, in this case we assume that  only accepts words of length ≥ 2):


  * Each location s ∈ S is of the form ⟨ℓ_1, S_1, …, ℓ_m, S_m ⟩ where ℓ_j ∈{0, 1, 2} and S_j ⊆ S^ for all j ∈{1, …, m}; intuitively, ⟨ℓ_j, S_j ⟩ can be seen as a location
of the sub-component C^ψ_j; 

  * s_0 = ⟨ 0, ∅, …, 0, ∅⟩;

  * X = {x_1, …, x_m};

  * = {F_1, …, F_m} where F_j contains all locations with ℓ_j = 0 or ℓ_j = 2;

  *  is obtained by synchronising
the transitions
⟨ℓ, S ⟩⟨ℓ', S' ⟩
of individual sub-components (we omit the subscripts for brevity):
	
	
  * p_ψ∉σ; ℓ' = 0, ℓ = 0; S' = ∅, S = ∅; g = ⊤; λ = ∅.
	
  * p_ψ∉σ; ℓ' = 1, ℓ∈{1, 2}; S  S'; g = ⊤; λ = ∅.
	
  * p_ψ∉σ; ℓ' = 0, ℓ∈{1, 2}; S' = ∅, S = {s^}, s^_F (s^, σ) for some s^_F ∈ F^; g = x ≤ c; λ = ∅.
	
  * p_ψ∈σ; ℓ' = 1, ℓ = 0; {s_0^} S', S = ∅; g = ⊤; λ = { x }. 
	
  * p_ψ∈σ; ℓ' = 1, ℓ∈{1, 2}; S' is the union of
some S” such that S  S” and S”' with {s_0^} S”'; g = ⊤; λ = ∅. 
	
  * p_ψ∈σ; ℓ' = 2, ℓ∈{1, 2}; {s_0^} S', S = {s^}, s^_F (s^, σ) for some s^_F ∈ F^; g = x ≤ c; λ = {x }. 
	
If p_ψ∈σ, then exactly
one of the sub-components takes a `p_ψ∈σ' transition
while the others proceed as if p_ψ∉σ.



^ψ = (p_ψ⇒_≤ c(ϕ_1, …, ϕ_n)).


Let ψ' =  (p_ψ⇒_≤ c(ϕ_1, …, ϕ_n))
and _ψ' be the equivalent  obtained via Proposition <ref>.
If a timed word ρ = (σ_i, τ_i)_i ≥ 1 satisfies ψ', there must be an accepting run
G = ⟨ V, →⟩ of _ψ' on ρ;
in particular, a copy of  is spawned whenever p_ψ holds.
Now consider each `level' 
L_i = { (s, v) | (s, v, i) ∈ V }
 of G in the increasing order of i.
If |{ (s^, v) | (s^, v) ∈ L_i }| ≤ 1 for every s^∈ S^, 
in ^ψ we simply put each corresponding obligation into an unused sub-component (with ℓ = 0 and S = ∅)
when it arrives, i.e. p_ψ holds.
If |{ (s^, v) | (s^, v) ∈ L_i }| > 1 for some s^∈ S^, since
the constraining interval [0, c] is downward closed, the DAG
obtained from G by replacing all the subtrees rooted at nodes (s^, v, i) 
with (s^, v^max, i),
where v^max = max{ v | (s^, v) ∈ L_i },
is still an accepting run of _ψ'; in ^ψ, this amounts to putting
the obligations that correspond to nodes (s^, v, i) into the sub-component
that holds the (oldest) obligation that corresponds to (s^, v^max, i).
We do the same for all such s^, obtain G', and start over from i + 1.
In this way, we can readily construct an accepting run of ^ψ on ρ.
The other direction obviously holds as each sub-component ^ψ_j
does not reset its associated clock x_j when p_ψ∈σ and ℓ_j ∈{1, 2},
unless the (only remaining) obligation in S_j is fulfilled right away.
In other words, ^ψ_j adds an obligation that is at least as strong to S_j
without weakening the existing ones in S_j.




  
ψ = _≥ c
Let ^ψ = ⟨Σ, S, s_0, X, , ⟩ be defined as follows:


  * Each location s ∈ S is of the form ⟨ℓ_1, S_1, T_1 …, ℓ_m, S_m, T_m ⟩ where ℓ_j ∈{0, 1, 2, 3} and S_j, T_j ⊆ S^ for all j ∈{1, …, m}; intuitively, ⟨ℓ_j, S_j, T_j ⟩ can be seen as a location
of the sub-component C^ψ_j;

  * s_0 = ⟨ 0, ∅, ∅, …, 0, ∅, ∅⟩;

  * X = {x_1, …, x_m};

  * = {F_1, …, F_m} where F_j contains all locations with ℓ_j = 0 or ℓ_j = 2;

  *  is obtained by synchronising (in the same way as before) 
⟨ℓ, S, T ⟩⟨ℓ', S', T' ⟩
of individual sub-components:
	
	
  * p_ψ∉σ; ℓ' = 0, ℓ = 0; S' = ∅, S = ∅, T' = ∅, T = ∅; g = ⊤; λ = ∅.
	
  * p_ψ∉σ; ℓ' = 1, ℓ∈{1, 2}; S  S', T' = ∅, T = ∅; g = ⊤; λ = ∅.
	
  * p_ψ∉σ; ℓ' = 3, ℓ = 3; S  S', T  T'; g = ⊤; λ = ∅.
	
  * p_ψ∉σ; ℓ' = 0, ℓ∈{1, 2}; S' = ∅, S = {s^}, s^_F (s^, σ) for some s^_F ∈ F^, T' = ∅, T = ∅; g = x ≥ c; λ = ∅.
	
  * p_ψ∉σ; ℓ' = 2, ℓ = 3; T  S', S = {s^}, s^_F (s^, σ) for some s^_F ∈ F^, T' = ∅; g = x ≥ c; λ = { x }.
	
  * p_ψ∈σ; ℓ' = 1, ℓ = 0; {s_0^} S', S = ∅, T' = ∅, T = ∅; g = ⊤; λ = { x }. 
	
  * p_ψ∈σ; ℓ' = 1, ℓ∈{1, 2}; S' is the union of
some S” such that S  S” and S”' with {s_0^} S”', T' = ∅, T = ∅; g = ⊤; λ = { x }. 
	
  * p_ψ∈σ; ℓ' = 3, ℓ = 1; S  S', {s_0^} T', T = ∅; g = ⊤; λ = ∅. 
	
  * p_ψ∈σ; ℓ' = 3, ℓ = 3; S  S', T' is the union of some T”
such that T  T” and T”' with {s_0^} T”'; g = ⊤; λ = ∅. 
	
  * p_ψ∈σ; ℓ' = 2, ℓ∈{1, 2}; {s_0^} S', S = {s^}, s^_F (s^, σ) for some s^_F ∈ F^, T' = ∅, T = ∅; g = x ≥ c; λ = {x }. 
	
  * p_ψ∈σ; ℓ' = 2, ℓ = 3; S' is the union of some S” such that T  S” and S”' with {s_0^} S”', S = {s^}, s^_F (s^, σ) for some s^_F ∈ F^, T' = ∅; g = x ≥ c; λ = { x }. 
	


^ψ = (p_ψ⇒_≥ c(ϕ_1, …, ϕ_n)).


Similar to the proof of Proposition <ref>, but since
[c, ∞) is upward closed, we 
replace all the subtrees rooted at nodes (s^, v, i) 
with (s^, v^min, i),
where v^min = min{ v | (s^, v) ∈ L_i };
in ^ψ, we still put the obligations that correspond to nodes (s^, v, i) into the sub-component
that holds the (oldest) obligation that corresponds to (s^, v^max, i).
There is, however, a potential issue: since we reset x_j whenever the trigger p_ψ is pulled
and ^ψ_j is chosen, 
it might be the case that x_j never reaches c, i.e. the satisfaction of the obligations in S_j are delayed indefinitely.
Following <cit.>, we solve this by locations with ℓ_j = 3 such that, when entered, 
we stop resetting x_j and put the new obligations into T_j instead;
when the obligations in S_j are fulfilled, we move the obligations in T_j to S_j
and reset x_j.
The other direction obviously holds as each sub-component ^ψ_j
resets x_j when p_ψ∈σ and ℓ_j ∈{1, 2},
unless it goes from ℓ_j = 1 to ℓ_j = 3.
In other words, ^ψ_j adds the new obligation to S_j
while strengthening the existing ones in S_j.




  
ψ = _≤ c
Let ^ψ = ⟨Σ, S, s_0, X, , ⟩ be defined as follows:


  * Each location s ∈ S is of the form ⟨ S_1, …, S_m+1⟩ where S_j ⊆ S^
		for all j ∈{1, …, m+1}; intuitively, S_j can be seen as a location of the sub-component C^ψ_j;

  * s_0 = ⟨∅, …, ∅⟩;

  * X = {x_1, …, x_m+1};

  * = ∅, i.e. any run is accepting;

  *  is obtained by synchronising (in the same way as before) 
S  S'
of individual sub-components:
	
	
  * p_ψ∉σ; S' = ∅, S = ∅; g = ⊤; λ = ∅.

	
  * p_ψ∉σ; S  S', S' ∩ F^ = ∅; g = x ≤ c; λ = ∅.

	
  * p_ψ∉σ; S' = ∅; g = x > c; λ = ∅.

	
  * p_ψ∈σ; {s_0^} S', S' ∩ F^ = ∅, S = ∅; g = ⊤; λ = { x }. 

	
  * p_ψ∈σ; S' is the union of
some S” such that S  S” and S”' with {s_0^} S”', S' ∩ F^ = ∅; g = x ≤ c; λ = { x }. 

	
  * p_ψ∈σ; {s_0^} S', S' ∩ F^ = ∅; g = x > c; λ = {x }. 

	



^ψ = (p_ψ⇒_≤ c(ϕ_1, …, ϕ_n)).


Let ψ' =  (p_ψ⇒_≤ c(ϕ_1, …, ϕ_n))
and _ψ' be the equivalent  obtained via Proposition <ref>.
Consider each level L_i = { (s, v) | (s, v, i) ∈ V }
 of an accepting run G = ⟨ V, →⟩ of _ψ' on ρ = (σ_i, τ_i)_i ≥ 1
in the increasing order of i. In ^ψ, whenever the trigger p_ψ is pulled, 
we attempt to put the corresponding obligation into an unused sub-component (with S = ∅)
or a sub-component that can be cleared (with x > c);
if this is not possible, since for every s^∈ S^ all the subtrees rooted at nodes
(s^, v, i) can be replaced with the subtree rooted at 
(s^, v^min, i) where v^min = min{ v | (s^, v) ∈ L_i },
at least one sub-component C^ψ_j becomes redundant, i.e. all of its obligations are implied by
the other sub-components C^ψ_k, k ≠ j. A consequence
is that the obligations in the sub-component C^ψ_k with the minimal non-negative
value of x_j - x_k can be merged with the obligations in C^ψ_j, freeing up a sub-component for
the current incoming obligation.
This can be repeated to construct an accepting run of ^ψ on ρ.
The other direction holds as each C^ψ_j adds the new obligation to S_j
while strengthening the existing obligations in S_j.




  
ψ = _≥ c
Let ^ψ = ⟨Σ, S, s_0, X, , ⟩ be defined as follows
(for simplicity, assume that c > 0):


  * Each location s ∈ S is of the form ⟨ S_1, T_1 …, S_m+1, T_m+1⟩ where S_j, T_j ⊆ S^ for all j ∈{1, …, m + 1}; intuitively, ⟨ S_j, T_j ⟩ can be seen as a location
of the sub-component C^ψ_j;

  * s_0 = ⟨∅, ∅, …, ∅, ∅⟩;

  * X = {x_1, …, x_m+1};

  * = ∅, i.e. any run is accepting;

  *  is obtained by synchronising (in the same way as before) 
⟨ℓ, S, T ⟩⟨ℓ', S', T' ⟩
of individual sub-components:
	
	
  * p_ψ∉σ; S' = ∅, S = ∅, T' = ∅, T = ∅; g = ⊤; λ = ∅.

	
  * p_ψ∉σ; S' = ∅, S = ∅, T  T', T' ∩ F^ = ∅; g = ⊤; λ = ∅.

	
  * p_ψ∉σ; S  S', T' = ∅, T = ∅; g = x < c; λ = ∅.

	
  * p_ψ∉σ; S  S', T  T', T' ∩ F^ = ∅; g = x < c; λ = ∅.

	
  * p_ψ∉σ; S' = ∅, T' is the union of some T” such that S  T”
and T”' with T  T”', T' ∩ F^ = ∅; g = x ≥ c; λ = ∅.

	
  * p_ψ∈σ; {s_0^} S', S = ∅, T' = ∅, T = ∅; g = ⊤; λ = { x }. 

	
  * p_ψ∈σ; {s_0^} S', S = ∅, T  T', T' ∩ F^ = ∅; g = ⊤; λ = { x }. 

	
  * p_ψ∈σ; S' is the union of
some S” such that S  S” and S”' with {s_0^} S”', T' = ∅, T = ∅; g = x < c; λ = ∅. 

	
  * p_ψ∈σ; S' is the union of
some S” such that S  S” and S”' with {s_0^} S”', 
T  T', T' ∩ F^ = ∅; g = x < c; λ = ∅. 

	
  * p_ψ∈σ; {s_0^} S', T' is the union of some T” such that S  T”
and T”' with T  T”', T' ∩ F^ = ∅; g = x ≥ c; λ = {x }. 
	


^ψ = (p_ψ⇒_≥ c(ϕ_1, …, ϕ_n)).


As in the proof of Proposition <ref>, whenever p_ψ is pulled in C^ψ,
we attempt to put the corresponding obligation into an unused sub-component (with S = ∅)
or a sub-component that can be cleared (if x > c, we move the obligations in S to T and let them remain there).
If this is not possible, since for every s^∈ S^ all the subtrees rooted at nodes
(s^, v, i) can be replaced with the subtree rooted at 
(s^, v^max, i) where v^max = max{ v | (s^, v) ∈ L_i },
some C^ψ_j becomes redundant, and the obligations in the sub-component C^ψ_k with the minimal non-negative
value of x_k - x_j can be merged with the obligations in C^ψ_j, freeing up a sub-component for
the current incoming obligation.
This can be repeated to construct an accepting run of ^ψ on ρ.
The other direction holds as each C^ψ_j
adds an obligation that is at least as strong to S_j
without weakening the existing obligations in S_j.




Finally, thanks to the fact that each location of C^ψ
can be represented using space polynomial in the size of ,
and the product ^init×∏_ψ∈Φ^ψ need not to be constructed
explicitly, we can state the main result of this section.


The satisfiability and model-checking problems for _0, ∞ over timed words
are PSPACE-complete.



The satisfiability and model-checking problems for  over timed words
are PSPACE-complete.






§ CONCLUSION


It is shown that _0, ∞ and  are already as expressive as
 over timed words, a somewhat unexpected yet very pleasant result.
We also provided a compositional construction
from _0, ∞ to diagonal-free s
based on one-clock alternating timed automata (s);
this allows satisfiability and model checking 
based on existing algorithmic back ends for s.
The natural next step would be to implement the construction
and evaluate its performance on real-world use cases.
Another possible future direction is to investigate whether
similar techniques can be used to handle full  or
larger fragments of s (like <cit.>).
  


The author would like to thank
Thomas Brihaye, Chih-Hong Cheng, Thomas Ferrère, Gilles Geeraerts, Timothy M. Jones, Arthur Milchior, and Benjamin Monmege
for their help and fruitful discussions.
The author would also like to thank the anonymous reviewers for their comments. This work is supported by the gsidepsrcEngineering and Physical Sciences Research Council (EPSRC)https://epsrc.ukri.org/
through grant gsidepsrcEP/P020011/1 and
(partially) by gsidfrsfnrsF.R.S.-FNRShttp://www.fnrs.be/ PDR
grant gsidfrsfnrsSyVeRLo.




ACM-Reference-Format
 




§ PROOF OF PROPOSITION <REF>



We first show that _ϕ⊆ϕ. Suppose that
_ϕ = ⟨Σ, S, s_0, , F ⟩ has an accepting run G = ⟨ V, →⟩ on ρ = (σ_1,τ_1)(σ_2,τ_2)⋯ and let 
L_i = { (s, v) | (s, v, i) ∈ V }.
We claim that:



  * For each s^∈ S^ where  occurs in a subformula _I(ϕ_1, …, ϕ_n)
and i ≥ 1, L_i _v s^ implies that 
there is a finite rooted DAG G' = ⟨ V', →' ⟩ with V' ⊆ S^×_≥ 0,
(s^, i) as the root, and for each vertex (s, k) either (a) k > i, v + (τ_k - τ_i) ∈ I, and s ∈ F^, or (b) there is some a_k+1∈Σ^
such that L_k+1_v + (τ_k+1 - τ_i)(ϕ_a_k+1, σ_k+1)
and there is a model M of the
formula ^(s, a_k+1) such that (s,k) →' (s',k+1)
.


  * For each s^∈ S^ where  occurs in a subformula _I(ϕ_1, …, ϕ_n)
and i ≥ 1, L_i _v s^ implies that 
there is a rooted DAG G' = ⟨ V', →' ⟩ with V' ⊆ S^×_≥ 0,
(s^, i) as the root, and each vertex (s, k) satisfies (a) if k > i then v + (τ_k - τ_i) ∈ I implies s ∉ F^, and (b) for every a_k+1∈Σ^,
either L_k+1_v + (τ_k+1 - τ_i)(ϕ_a_k+1, σ_k+1)
or there is a model M of the
formula ^(s, a_k+1) such that (s,k) →' (s',k+1)
for every state .



We prove (1); (2) can be proved similarly.
First note that every branch labelled with locations of  must terminate. 
If (s^, v, i) is a leaf with respect to S^ in G, we must have N _v + (τ_i+1 - τ_i)(ϕ_a , σ_i+1) ^[s_F^← s^_F  x ∈ I](s^, a) for some a ∈Σ^ and N ⊆ (S ∖ S^) ×_≥ 0
such that N ⊆ L_i+1.
It follows that either (i) N _v + (τ_i+1 - τ_i)(ϕ_a , σ_i+1) ^(s^, a)
or (ii) v + (τ_i+1 - τ_i) ∈ I and N ∪ M _v + (τ_i+1 - τ_i)(ϕ_a , σ_i+1) ^(s^, a)
for some nonempty M ⊆ F^×{ v + (τ_i+1 - τ_i) }.
In case (i), (b) trivially holds.
In case (ii) note that N _v + (τ_i+1 - τ_i)(ϕ_a , σ_i+1), and let { (s', i+1) | (s', v') ∈ M } be the successors
of (s^, i) in G': each of them satisfies (a).
If (s^, v, i) is not a leaf with respect to S^ in G, we have N ∪ M _v + (τ_i+1 - τ_i)(ϕ_a , σ_i+1) ^[s_F^← s^_F  x ∈ I](s^, a) for some a ∈Σ^, N ⊆ (S ∖ S^) ×_≥ 0
such that N ⊆ L_i+1, and nonempty M ⊆ S^×{ v + (τ_i+1 - τ_i) }
such that M ⊆ L_i+1. It follows that either (i) N ∪ M _v + (τ_i+1 - τ_i)(ϕ_a , σ_i+1) ^(s^, a)
or (ii) v + (τ_i+1 - τ_i) ∈ I and N ∪ M' _v + (τ_i+1 - τ_i)(ϕ_a , σ_i+1) ^(s^, a)
for some M' ⊃ M with M' ∖ M ⊆ F^×{ v + (τ_i+1 - τ_i) }.
In case (i), let { (s', i+1) | (s', v') ∈ M } be the successors
of (s^, i) in G'; applying the IH on L_i+1_v + (τ_i+1 - τ_i) s'
for all such s' yields the corresponding sub-DAGs, which we combine to obtain G'.
Case (ii) is similar.


We now claim that for each subformula ψ of ϕ and  i ≥ 1,
L_i  _0 (ψ, σ_i) implies ρ, i ψ.
The cases of atomic propositions, negation, and Boolean operators
are trivial. For ψ = _I(ϕ_1, …, ϕ_n), as L_i _0 (s_0^, σ_i)
we have, for some a ∈Σ^, (i) L_i _0 (ϕ_a, σ_i)
and (ii) L_i _0 ^[s_F^← s^_F  x ∈ I](s_0^, a).
From (i) and the IH we obtain ρ, i ϕ_a.
From (ii) we deduce that there is M ⊆ (S^∖ F^) ×{ 0 }
such that M ⊆ L_i, and M' ⊇ M such that
M' ∖ M ⊆ F^×{ 0 } and M' _0 ^(s_0^, a).
Applying (1) on every s^∈ M and the IH (note that by the definition of ,
we have L_k+1_0 (ϕ_a_k+1, σ_k+1) if L_k+1_v + (τ_k+1 - τ_i)(ϕ_a_k+1, σ_k+1))
and combining sub-DAGs gives ρ, i ψ.
The case of ψ = _I(ϕ_1, …, ϕ_n)  is analogous.


Finally, as s^init∈ L_0, we have L_1 _τ_1 x.(ϕ, σ_1),
which is equivalent to L_1 _0 (ϕ, σ_1). It follows that ρ, 1 ϕ; this finishes the proof of _ϕ⊆ϕ.

For the other direction, observe that _ϕ = (_ϕ)^c (up to renaming of locations)
where (_ϕ)^c is obtained from _ϕ by dualising the transition function and 
swapping the sets of final and non-final locations.
The desired result (ϕ⊆_ϕ)
immediately follows from the fact that _ϕ is a tree-like  <cit.>.





























