Making Metric Temporal Logic Rational
S. Krishna
krishnas,[email protected]
Khushraj Madnani
krishnas,[email protected]
P. K. Pandya
[email protected]
Abstract
We study an extension of MTL in pointwise time with rational expression guarded modality
RatI(re) where re is a rational expression over subformulae. We study the decidability and expressiveness of this extension (MTL+φURatI,reφ+RatI,reφ), called RatMTL, as well as its fragment
SfrMTL where only star-free rational expressions are allowed. Using the technique of temporal projections, we show that RatMTL has decidable satisfiability by giving an equisatisfiable reduction to MTL. We also identify a subclass MITL+URat
of RatMTL for which our equi-satisfiable reduction gives rise to formulae of MITL, yielding elementary decidability. As our second main result, we show
a tight automaton-logic connection between SfrMTL and partially ordered (or very weak) 1-clock alternating timed automata.
1 Introduction
Temporal logics provide constructs to specify qualitative ordering between events in time. Real time logics are quantitative extensions of temporal logics with the ability to specify real time constraints amongst events. Logics MTL and TPTL are amongst the prominent real time logics [2]. Two notions of MTL semantics have been studied in the literature : continuous and pointwise [4]. The expressiveness and decidability results vary
considerably with the semantics used : while the satisfiability checking of MTL is undecidable in the continuous semantics even for finite timed words [1], it is decidable in pointwise semantics with non-primitive recursive complexity [15].
Due to limited expressive power of MTL, several additional modalities have been proposed : the threshold\leavevmode counting modality [17] CI≥nϕ states that in time interval I relative to current point, ϕ occurs at least n times. The Pnueli modality [17] PnI(ϕ1,…,ϕn) states that there is a subsequence of n time points inside interval I where at ith point the formula ϕi holds. In a recent result, Hunter [9] showed that, in continuous time semantics, MTL enriched with C modality (denoted MTL+C) is as expressive as FO with distance FO[<,+1], which is as expressive as TPTL. Unfortunately, satisfiability and model checking of all these logics are undecidable. This has led us to
focus on the pointwise case with only the future modality, i.e. logic MTL[UI], which we abbreviate as MTL in rest of the paper.
Also, MTL+op means MTL with modalities UI as well as op.
In pointwise semantics, it can be shown that MTL⊂MTL+C⊂MTL+Pn (see [11]). In this paper, we propose
a generalization of threshold counting and Pnueli modalities by a rational\leavevmode expression modality RatIre(ϕ1,…,ϕk), which
specifies that the truth of the subformulae, ϕ1,…,ϕk, at the set of points within interval I is in accordance with the
rational expression re(ϕ1,…,ϕk). The resulting logic is called RatMTL and is the subject of this paper.
The expressive power of logic RatMTL raises several points of interest.
It can be shown that MTL+Pn⊂RatMTL, and it can express several new and interesting properties:
(1) Formula Rat(1,2)((aa)∗) states that within time interval (1,2) there is an even number of occurrences of a. We will define
a derived modulo counting modality which states this directly as the formula MC(1,2)0%2a.
(2) An exercise regime lasting between 60 to 70 seconds consists of arbitrary many repetitions of three pushup cycles which must be completed
within 2 seconds. There is no restriction on delay between two cycles to
accomodate weak athletes. This is given by
Rat[60,70]((UPP.up.up)∗) where
UPP=(up\leavevmode URat(0,2],upup).
The inability to specify rational expression constraints has been an important lacuna of LTL and its practically useful extensions
such as PSL sugar [7], [6] (based on Dymanic Logic [8]) which extend LTL with both counting and
rational expressions. This indicates that our logic RatMTL is a natural and useful logic for specifying properties.
However, to our knowledge, impact of rational expression constraints on metric temporal modalities have not been studied before.
As we show in the paper, timing and regularity constraints interact in a fairly complex manner.
As our first main result, we show that satisfiability of RatMTL is decidable by giving an equisatisfiable reduction to MTL. The reduction
makes use of the technique of oversampled temporal projections which was previously proposed [10], [11] and used for proving the decidability of MTL+C. The reduction given here has several novel features such as an MTL encoding of the run tree of an alternating automaton which restarts the DFA of a given rational expression at each time point (section 3.1).
We identify two syntactic subsets of RatMTL denoted MITL+URat with 2EXPSPACE hard satisfiability, and its further subset MITL+UM with EXPSPACE-complete satisfiability.
As our second main result, we show that the star-free fragment SfrMTL of RatMTL characterizes exactly the class of partially ordered 1-clock alternating timed automata, thereby giving a tight logic automaton connection. The most non-trivial part
of this proof is the construction of SfrMTL formula
equivalent to a given partially ordered 1-clock alternating timed automaton A (Lemma 4.5).
2 Timed Temporal Logics
This section describes the syntax and semantics of the timed temporal logics
needed in this paper : MTL and TPTL.
Let Σ be a finite set of propositions. A finite timed word over Σ is a tuple
ρ=(σ,τ). σ and τ are sequences σ1σ2…σn and τ1τ2…τn respectively, with σi∈P(Σ)−∅, and τi∈R≥0
for 1≤i≤n and ∀i∈dom(ρ), τi≤τi+1, where dom(ρ) is the set of positions {1,2,…,n} in the timed word. For convenience, we assume τ1=0.
The σi’s can be thought of as labeling positions i in dom(ρ).
For example, given Σ={a,b,c}, ρ=({a,c},0)({a},0.7)({b},1.1) is a timed word.
ρ is strictly monotonic iff τi<τi+1 for all i,i+1∈dom(ρ).
Otherwise, it is weakly monotonic.
The set of finite timed words over Σ is denoted TΣ∗.
Given ρ=(σ,τ) with σ=σ1…σn,
σsingle denotes the set of
words {w1w2…wn∣wi∈σi}. For ρ as above,
σsingle consists of ({a},0)({a},0.7)({b},1.1)
and ({c},0)({a},0.7)({b},1.1).
Let Iν be a set of open, half-open or closed time intervals.
The end points of these intervals are in N∪{0,∞}. For example,
[1,3),[2,∞). For τ∈R≥0 and interval ⟨a,b⟩, with <∈{(,[} and >∈{],)},
τ+⟨a,b⟩ stands for the interval
⟨τ+a,τ+b⟩.
Metric Temporal Logic(MTL). Given a finite alphabet Σ, the formulae of MTL are built from Σ using boolean connectives and
time constrained version of the modality U as follows:
φ::=a(∈Σ)\leavevmode ∣true\leavevmode ∣φ∧φ\leavevmode ∣\leavevmode ¬φ\leavevmode ∣\leavevmode φUIφ,
where I∈Iν.
For a timed word ρ=(σ,τ)∈TΣ∗, a position
i∈dom(ρ), and an MTL formula φ, the satisfaction of φ at a position i
of ρ is denoted (ρ,i)⊨φ, and is defined as follows: (i)
ρ,i⊨a ↔ a∈σi, (ii) ρ,i⊨¬φ ↔ ρ,i⊭φ,
(iii) ρ,i⊨φ1∧φ2 ↔
ρ,i⊨φ1
and ρ,i ⊨ φ2, (iv)
ρ,i ⊨ φ1UIφ2 ↔ ∃j>i,
ρ,j ⊨ φ2,τj−τi∈I, and ρ,k ⊨ φ1 ∀ i<k<j.
The language of a MTL formula φ is L(φ)={ρ∣ρ,1⊨φ}.
Two formulae φ and ϕ are said to be equivalent denoted as φ≡ϕ iff L(φ)=L(ϕ).
Additional temporal connectives are defined in the standard way:
we have the constrained future eventuality operator ◊Ia≡trueUIa
and its dual
□Ia≡¬◊I¬a.
We also define the next operator as OIϕ≡⊥UIϕ.
Non strict versions of operators
are defined as ◊Insa=a∨◊Ia,□Insa≡a∧□Ia, aUInsb≡b∨[a∧(aUIb)] if 0∈I, and
[a∧(aUIb)] if 0∈/I. Also, aWb is a shorthand for □a∨(aUb).
The subclass of MTL obtained by restricting the intervals I in the until modality
to non-punctual intervals is denoted MITL.
Timed Propositional Temporal Logic (TPTL).
TPTL is a prominent real time extension of LTL, where timing constraints are specified with the help of freeze clocks.
The set of TPTL formulas are defined inductively as
φ::=a(∈Σ)\leavevmode ∣true\leavevmode ∣φ∧φ\leavevmode ∣\leavevmode ¬φ\leavevmode ∣\leavevmode φUφ\leavevmode ∣\leavevmode y.φ\leavevmode ∣\leavevmode y∈I.
C is a set of
clock variables progressing at the same rate,
y∈C, and I is an interval as above. For a timed word ρ=(σ1,τ1)…(σn,τn), we define the satisfiability relation, ρ,i,ν⊨ϕ saying that the formula ϕ is true at position
i of the timed word ρ with valuation ν of all the clock
variables as follows:
(1) ρ,i,ν⊨a ↔ a∈σi,
(2) ρ,i,ν⊨¬φ ↔ ρ,i,ν⊭φ,
(3) ρ,i,ν⊨φ1∧φ2 ↔ ρ,i,ν⊨φ1
and ρ,i,ν ⊨ φ2,
(4) ρ,i,ν⊨x.φ ↔ ρ,i,ν[x←τi]⊨φ,
(5) ρ,i,ν⊨x∈I ↔ τi−ν(x)∈I,
(6) ρ,i,ν ⊨ φ1Uφ2 ↔ ∃j>i,
ρ,j,ν ⊨ φ2, and
ρ,k,ν ⊨ φ1 ∀ i<k<j.
ρ satisfies ϕ denoted ρ⊨ϕ iff ρ,1,0ˉ⊨ϕ. Here 0ˉ
is the valuation obtained by setting all clock variables to 0.
We denote by k−TPTL the fragment of TPTL using at most k clock variables.
Theorem 2.1** ([15]).**
MTL* satisfiability is decidable over finite timed words and is non-primitive recursive.*
MTL with Rational Expressions(RatMTL)
We propose an extension of MTL with rational expressions, that forms the core of the paper.
These modalities can assert the truth of a rational expression (over subformulae) within a particular time interval with respect to the present point.
For example, Rat(0,1)(φ1.φ2)+ when evaluated at a point i, asserts the existence of 2k points
τi<τi+1<τi+2<⋯<τi+2k<τi+1, k>0,
such that φ1 evaluates to true at τi+2j+1, and φ2 evaluates to true at
τi+2j+2, for all 0≤j<k.
RatMTL Syntax: Formulae of RatMTL are built from Σ (atomic propositions) as follows:
φ::=a(∈Σ)\leavevmode ∣true\leavevmode ∣φ∧φ\leavevmode ∣\leavevmode ¬φ\leavevmode ∣\leavevmode RatIre(S)\leavevmode ∣\leavevmode φURatI,re(S)φ,
where I∈Iν
and S is a finite set of formulae of interest, and re(S) is defined as a rational expression over S.
re(S)::=φ(∈S)\leavevmode ∣\leavevmode re(S).re(S)\leavevmode ∣\leavevmode re(S)+re(S)\leavevmode ∣\leavevmode [re(S)]∗. Thus, RatMTL
is MTL+URat+Rat.
An atomic rational expression re is any well-formed formula φ∈RatMTL.
RatMTL Semantics:
For a timed word ρ=(σ,τ)∈TΣ∗, a position
i∈dom(ρ), and a RatMTL formula φ, a finite set S of formulae, we define the satisfaction of φ at a position i
as follows. For positions i<j∈dom(ρ), let Seg(S,i,j) denote
the untimed word over P(S)
obtained by marking the positions k∈{i+1,…,j−1} of ρ with
ψ∈S iff ρ,k⊨ψ.
For a position i∈dom(ρ) and an interval I,
let TSeg(S,I,i) denote
the untimed word over P(S)
obtained by marking all the positions k
such that τk−τi∈I
of ρ with
ψ∈S iff ρ,k⊨ψ.
-
ρ,i⊨φ1URatI,re(S)φ2 ↔ ∃j>i,
ρ,j⊨ φ2,τj−τi∈I, ρ,k ⊨ φ1 ∀i<k<j and,
[Seg(S,i,j)]single∩L(re(S))=∅, where L(re(S)) is the language
of the rational expression re formed over the set S.
The subclass of RatMTL using only the URat modality is denoted
RatMTL[URat] or MTL+URat and if only non-punctual intervals are used, then it is denoted RatMITL[URat]
or MITL+URat.
2. 2.
ρ,i⊨RatIre ↔
[TSeg(S,I,i)]single∩L(re(S))=∅.
The language accepted by a RatMTL formula φ is given by
L(φ)={ρ∣ρ,0⊨φ}.
Example 1.
Consider the formula φ=aURat(0,1),ab∗b. Then re=ab∗, and the subformulae
of interest are a,b.
For ρ=({a},0)({a,b},0.3)({a,b},0.99),
ρ,1⊨φ, since a∈σ2,b∈σ3, τ3−τ1∈(0,1) and
a∈[Seg({a,b},1,3)]single∩L(ab∗).
On the other hand, for the word ρ=({a},0)({a},0.3)({a},0.5)({a},0.9)({b},0.99), we know that
ρ,1⊭φ, since even though b∈σ5,a∈σi for i<5,
[Seg({a,b},1,5)]single=aaa and aaa∈/L(ab∗).
Example 2.
Consider the formula φ=Rat(0,1)[¬Rat(0,1)a].
For the word ρ=({a,b},0) ({a,b},0.91)({a},1.2),
to check φ at position 1, we check position 2 of the word, since τ2−τ1∈(0,1). The formulae of interest for marking
is {¬Rat(0,1)a}. Position 2 is not marked, since
ρ,2⊨Rat(0,1)a.
Then [TSeg(S,(0,1),1)]single=∅∈/L(¬Rat(0,1)a). However, for the word
ρ=({a,b},0) ({a,b},0.91)({b},1.1),
ρ,1⊨φ, since position 2 is marked with
¬Rat(0,1)a, and
¬Rat(0,1)a∈L(¬Rat(0,1)a)∩[TSeg(S,(0,1),1)]single.
Example 3.
Consider the formula φ=Rat(0,1)[Rat(0,1)a]∗.
For \rho=(\{a,b\},0)$$(\{a,b\},0.7)(\{b\},0.98)(\{a,b\},1.4), we have
ρ,1⊭Rat(0,1)[Rat(0,1)a]∗, since
point 2 is not marked Rat(0,1)a, even though point 3 is.
Generalizing Counting, Pnueli & Mod Counting Modalities
The following reductions show that RatMTL subsumes most of the extensions of MTL studied in the literature.
(1) Threshold Counting constraints [17], [12], [11] specify the number of times a property holds within some time region is at least (or at most) n. These can be expressed in RatMTL:
(i) CI≥nφ≡RatI(reth),
(ii) ϕ1UTI,φ≥nϕ2≡ϕ1URatI,rethϕ2, where
\mathsf{re}_{th}={true^{*}\!\underbrace{\varphi.true^{*}.\ldots.\varphi.true^{*}}_{\text{n times}}}.
(2) Pnueli Modalities [17], which enhance the expressiveness of MITL in continuous semantics preserving the complexity, can be
written in RatMTL:
Pn(ϕ1,ϕ2,…,ϕk) can be written as RatI(true∗.ϕ1.true∗ϕ2.….true∗.ϕk.true∗).
(3) Modulo Counting constraints [3], [13]
specify the number of times a property holds modulo n∈N, in some region.
We extend these to the timed setting by proposing two modalities MCIk%n and
UMI,φ=k%n. MCIk%nφ checks if the number of times φ
is true in interval I is M(n)+k, where M(n) denotes a non-negative integer multiple of n, and
0≤k≤n−1, while φ1UMI,#ψ=k%nφ2 when asserted at a point i, checks
the existence of j>i such that τj−τi∈I, φ2 is true at j, φ1 holds
between i,j, and the number of times ψ is true
between i,j is M(n)+k, 0≤k≤n−1. As an example, ψ=trueUM(0,1),#b=1%2(a∨b), when asserted at a point i, checks the existence
of a point j>i such that a or b∈σj, τj−τi∈(0,1),
and the number of points between i,j where b is true is odd.
Both these modalities can be rewritten equivalently in RatMTL as follows:
MCIk%nφ≡RatI(remod) and
ϕ1UMI,φ=k%nϕ2≡ϕ1URatI,remodϕ2
where
\mathsf{re}_{mod}=([\underbrace{(\neg\varphi)^{*}.\varphi.\ldots.(\neg\varphi)^{*}.\varphi}_{\text{n times}}]^{*}.[\underbrace{(\neg\varphi)^{*}.\varphi.\ldots.(\neg\varphi)^{*}.\varphi}_{\text{k times}}].
The extension of MTL (MITL) with only UM
is denoted MTL+UM (MITL+UM) while MTL+MC (MITL+MC) denotes the extension
using MC.
3 Satisfiability of RatMTL and Complexity
The main results of this section are as follows.
Theorem 3.1**.**
*(1) Satisfiability of RatMTL is decidable.
(2) Satisfiability of MITL+UM is EXPSPACE-complete.
(3) Satisfiability of MITL+URat is in 2EXPSPACE.
(4) Satisfiability of MITL+MC is Fωω-hard.*
Details of Theorems 3.1.2, 3.1.3, 3.1.4 can be found in Appendices E.2, E.3 and E.4.
Theorem 3.2**.**
MTL+URat⊆MTL+Rat, MTL+UM⊆MTL+MC.
Theorem 3.2 shows that the Rat modality can capture URat (and likewise, MC captures
UM). Thus, RatMTL≡MTL+Rat. Observe that any re can be decomposed into finitely many factors, i.e.
re=i=1∑nR1i.R2i.
Given trueURat[l,u),reϕ2,
we assert R1i
within interval (0,l] and R2i in the prefix of the
latter part within [l,u), followed by ϕ2.
trueURat[l,u),reϕ2≡i∈{1,2…,n}⋁Rat(0,l)R1i∧Rat[l,u)R2i.ϕ2.Σ∗.
The proofs can be seen in Appendix G.
3.1 Proof of Theorem 3.1.1
Equisatisfiability We will use the technique of equisatisfiability modulo oversampling [10]
in the proof of Theorem 3.1.
Using this technique, formulae φ in one logic (say RatMTL) can be
transformed into formulae ψ over a simpler logic (say MTL) such that
whenever ρ⊨φ for a timed word ρ over alphabet Σ,
one can construct a timed word ρ′ over an extended set of positions and an extended alphabet
Σ′ such that ρ′⊨ψ and vice-versa [10], [11].
In oversampling, (i) dom(ρ′) is
extended by adding some extra positions between the first and last point of ρ, (ii) the labeling of a position
i∈dom(ρ) is over the extended alphabet Σ′⊃Σ and can be a superset of the previous labeling over Σ,
while the new positions are labeled using only the new symbols Σ′−Σ.
We can recover ρ from ρ′ by erasing the new points and the new symbols.
A restricted use of oversampling, when one only extends
the alphabet and not the set of positions of a timed word ρ is called simple extension.
In this case, if ρ′ is a simple extension of ρ, then dom(ρ)=dom(ρ′), and by erasing the new symbols from ρ′, we obtain ρ.
See Figure 1 for an illustration.
The formula ψ over the larger alphabet Σ′⊃Σ such that ρ′⊨ψ iff ρ⊨φ
is said to be equisatisfiable modulo temporal projections to φ. In particular, ψ is equisatisfiable to
φ modulo simple extensions or modulo oversampling, depending on how the word ρ′ is constructed
from the word ρ.
The oversampling technique is used in the proofs of
parts 3.1.1,
3.1.3 and 3.1.4.
Equisatisfiable Reduction : RatMTL to MTL
Let φ be a RatMTL formula. To obtain equisatisfiable MTL formula ψ, we do the following.
-
We “flatten” the reg modalities to simplify the formulae, eliminating nested
reg modalities. Flattening results in extending the alphabet.
Each of the modalities RatI,URat that appear in the formula φ are replaced with fresh witness propositions to obtain a flattened formula. For example,
if φ=Rat(0,1)[aURat(1,2),Rat(0,1)(a+b)∗b], then flattening
yields the formula φflat=w1∧□ns[w1↔Rat(0,1)w2]∧□ns[w2↔aURat(1,2),w3b]∧□ns[w3↔Rat(0,1)(a+b)∗], where w1,w2,w3 are fresh witness propositions.
Let W be the set of fresh witness propositions such that Σ∩W=∅.
After flattening, the modalities RatI,URat appear only in this simplified form as □ns[w↔RatI,URat].
This simplified appearance of reg modalities are called
temporal definitions
and have the form
□ns[w↔RatI\and] or □ns[w↔xURatI′,\andy], where \and is a rational expression over Σ∪Wi, Wi being the set of fresh witness propositions used in the flattening,
and I′ is either a unit length interval or an unbounded interval.
2. 2.
The elimination of reg modalities is achieved by obtaining equisatisfiable MTL formulae ψi
over Xi, possibly a larger set of propositions
than Σ∪Wi corresponding to
each temporal definition Ti
of φflat. Relativizing these MTL formulae and conjuncting them, we obtain an MTL
formula ⋀iRel(ψi,Σ) that is equisatisfiable to φ (see Figure 1 for relativization).
The above steps are routine [10], [11]. What remains is to handle the temporal definitions.
Embedding the Runs of the DFA
For any given ρ over Σ∪W, where W is the set of witness propositions used in the temporal definitions
T of the forms □ns[w↔RatI\and] or □ns[w↔xURatI′,\andy],
the rational expression \and has a corresponding minimal DFA recognizing it. We
define an LTL formula GOODRUN(ϕe) which takes a formula ϕe as a parameter
with the following behaviour. ρ,i⊨GOODRUN(ϕe) iff for all k>i,
(ρ,k⊨ϕe)→(ρ[i,k]∈L(\and)). To achieve this,
we use two new sets of symbols Threads and Merge for this information.
This results in the extended alphabet
Σ∪W∪Threads∪Merge for the simple extension ρ′ of ρ. The behaviour of Threads and
Merge are explained below.
Consider \and=re(S).
Let A\and=(Q,2S,δ,q1,QF) be the minimal DFA for \and
and let Q={q1,q2,…,qm}. Let In={1,2,…,m} be the indices of the states.
Conceptually, we consider multiple runs of A\and with a new run (new thread) started at each point in ρ. Threads records the state of each previously started run. At each step, each thread is updated from it previous value according to the transition function δ of A\and and also augmented with a new run in initial state. Potentially, the number of threads would grow unboundedly in size but notice that once two runs are the same state at position i they remain identical in future. Hence they can be merged into single thread (see
Figure2). As a result, m threads suffice. We record whether threads are merged in the current state using variables Merge. An LTL formula records the evolution of Threads and Merge over any behaviour ρ. We can define formula GOODRUN(ϕe) in LTL over
Threads and Merge.
-
At each position, let Thi(qx) be a proposition that denotes that the ith thread is active and is in state qx,
while Thi(⊥) be a proposition that denotes that the ith thread is not active.
The set Threads consists of propositions Thi(qx),Thi(⊥) for 1≤i,x≤m.
2. 2.
If at a position e, we have Thi(qx) and Thj(qy) for i<j, and if δ(qx,σe)=δ(qy,σe),
then we can merge the threads i,j at position e+1. Let merge(i,j) be a proposition that signifies that threads i,j have been merged.
In this case, merge(i,j) is true at position e+1. Let Merge be the set of all propositions
merge(i,j) for 1≤i<j≤m.
We now describe the conditions to be checked in ρ′.
Initial condition(φinit)- At the first point of the word, we start the first thread and initialize all other threads as ⊥ :
φinit=((Th1(q1))∧1<i≤m⋀Thi(⊥)).
Initiating runs at all points(φstart)- To check the rational expression within an arbitrary interval, we need to start a new run from every point.
φstart=□ns(i≤m⋁Thi(q1))
Disallowing Redundancy(φno−red)- At any point of the word, if i<j and Thi(qx) and Thj(qx) are both true, qx=qy.
φno−red=x∈In⋀□ns[¬1≤i<j≤m⋁(Thi(qx)∧Thj(qx))]
Merging Runs(φmerge)- If two different threads Thi,Thj(i<j) reach the same state qx on reading the input at the present point,
then we merge thread Thj with Thi. We remember the merge with the proposition merge(i,j).
We define a macro Nxt(Thi(qx)) which is true at a point e if and only if Thi(qy) is true at e and δ(qy,σe)=qx,
where σe⊆AP is the maximal set of propositions true at e:
{(qy,prop)∈(Q,2AP)∣δ(qy,prop)=qx}⋁[prop∧Thi(qy)].
Let ψ(i,j,k,qx) be a formula that says that at the next position, Thi(qx) and Thk(qx) are true for k>i, but for all j<i,
Thj(qx) is not. ψ(i,j,k,qx) is given by
Nxt(Thi(qx))∧j<i⋀¬Nxt(Thj(qx))∧Nxt(Thk(qx)).
In this case, we merge threads Thi,Thk, and either restart Thk in the initial state, or deactivate the kth thread at the next position.
This is given by the formula NextMerge(i,k)=O[merge(i,k)∧(Thk(⊥)∨Thk(q1))∧Thi(qx)].
φmerge=x,i,k∈In∧k>i⋀□ns[ψ(i,j,k,qx)→NextMerge(i,k)].
Propagating runs(φpro,φNO−pro)- If Nxt(Thi(qx)) is true at a point, and if for all j<i, ¬Nxt(Thj(qx)) is true,
then at the next point, we have Thi(qx). Let NextTh(i,j,qx) denote the formula Nxt(Thi(qx))∧¬Nxt(Thj(qx)).
The formula
φpro is given by
i,j∈In∧i<j⋀□ns[NextTh(i,j,qx)→O[Thi(qx)∧¬merge(i,j)]].
If Thi(⊥) is true at the current point, then at the next point, either Thi(⊥) or Thi(q1).
The latter condition corresponds to starting a new run on thread Thi.
φNO−pro=i∈In⋀□ns{Thi(⊥)→O(Thi(⊥)∨Thi(q1))}
Let Run be the formula obtained by conjuncting all formulae explained above.
Once we construct the simple extension ρ′, checking whether the rational expression \and holds in some interval I in the timed word ρ,
is equivalent to checking that
if u is the first action point within I, and if Thi(q1) holds at u, then after a series of merges of
the form merge(i1,i),merge(i2,i1),
…merge(j,in), at the last point v in the interval I, Thj(qf) is true,
for some final state qf.
This is encoded as GOODRUN(qf).
It can be seen that
the number of possible sequences of merges are bounded.
Figure 2 illustrates the threads and merging.
We can easily write a 1- TPTL formula that will check the truth of Rat[l,u)\and at a point v on the simple extension
ρ′ (see Appendix C). However, to write an MTL formula that checks the truth of
Rat[l,u)\and at a point v, we need to oversample ρ′ as shown below.
Lemma 3.3**.**
Let T=□ns[w↔RatI\and] be a temporal definition built from Σ∪W.
Then we synthesize a formula ψ∈MTL
over Σ∪W∪X such that
T is equivalent to ψ modulo oversampling.
Proof 3.4**.**
Lets first consider the case when the interval I is bounded of the form [l,u).
Consider a point in ρ′ with time stamp τv. To assert w
at τv,
we look at the
first action point after time point
τv+l, and check that GOODRUN(last(qf)) holds, where last(qf) identifies the
last action point
just before τv+u.
The first difficulty is the possible absence of time points τv+l and τv+u.
To overcome this difficulty, we oversample ρ′ by introducing
points at times t+l,t+u, whenever t is a time point in ρ′. These new points are labelled with a new proposition
ovs. Sadly, last(qf) cannot be written in MTL.
To address this, we introduce new time points at every integer
point of ρ′. The starting point 0 is labelled c0. Consecutive integer time points
are marked ci,ci⊕1, where ⊕ is addition modulo
the maximum constant used in the time interval in the RatMTL formula. This helps in measuring the time elapse
since the first action point after τv+l, till the last action point before τv+u as follows:
if τv+l lies between points marked cj,cj⊕1, then
the last integer point before τv+u is uniquely marked cj⊕u.
Anchoring at τv, we assert the following at distance l:
no action points are seen until the first action point where Thi(q1) is true for some
thread Thi.
Consider the next point where
cj⊕u is seen. Let Thik1 be the thread to which Thi
has merged at the last action point just before cj⊕u.
Let us call Thik1 the “last merged thread” before cj⊕u.
The sequence of merges from Thi till Thik1
asserts a prefix of the run
that we are looking for between τv+l and τv+u.
To complete the run we mention the sequence of merges from Thik1
which culminates in some Thik(qf) at the last action point before
τv+u.
Anchoring at τv, we assert the following at distance u:
we see no action points since Thik(qf) at the action point
before τv+u for some thread Thik, and there is a path linking
thread Thik1 to Thik
since the point cj⊕u. We assert that the “last merged thread”,
Thik1 is active at cj⊕u : this is the linking thread which is last merged
into before cj⊕u, and which is the first thread which merges into another thread after cj⊕u.
These two formulae thus “stitch” the actual run observed between points τv+l and τv+u. The formal technical details can be seen
in Appendix D.
If I was an unbounded interval of the form [l,∞), then
we will go all the way till the end of the word, and assert Thik(qf) at the last action point of the word.
Thus, for unbounded intervals, we do not need any oversampling at integer points.
In a similar manner, we can eliminate the URat modality, the proof of which can be found in Appendix E.
If we choose to work on logic MITL+URat, we obtain a 2EXPSPACE upper bound for satisfiability checking,
since elimination of URat results in an equisatisfiable MITL formula. This is an interesting consequence
of the oversampling technique; without oversampling, we can eliminate
URat obtaining 1-TPTL (Appendix C). However, 1-TPTL does not enjoy
the benefits of non-punctuality, and is non-primitive recursive (Appendix F).
4 Automaton-Metric Temporal Logic-Freeze Logic Equivalences
The focus of this section is to obtain equivalences between automata,
temporal and freeze logics.
First of all, we identify a fragment of RatMTL denoted
SfrMTL, where the rational
expressions in the formulae are all star-free.
We then show the equivalence between po-1-clock ATA, 1−TPTL,
and SfrMTL (po-1-clock ATA ⊆SfrMTL⊆1−TPTL≡po-1-clock ATA).
The main result of this section gives a tight automaton-logic connection in Theorem 4.1, and is
proved using Lemmas 4.3, 4.4 and
4.5.
Theorem 4.1**.**
1−TPTL, SfrMTL and po-1-clock ATA are all equivalent.
We first show that partially ordered 1-clock alternating timed automata (po-1-clock ATA) capture exactly the same class of languages as 1−TPTL. We also show that 1−TPTL is equivalent to the subclass SfrMTL of RatMTL where the rational expressions
re involved in the formulae are such that L(re) is star-free.
A 1-clock ATA [15] is a tuple A=(Σ,S,s0,F,δ), where
Σ is a finite alphabet, S is a finite set of locations,
s0∈S is the initial location and F⊆S is the set
of final locations. Let x denote the clock variable in the 1-clock ATA, and x⋈c denote a clock constraint
where c∈N and ⋈∈{<,≤,>,≥}. Let X denote a finite set
of clock constraints of the form x⋈c. The transition function is defined as
δ:S×Σ→Φ(S∪Σ∪X) where
Φ(S∪Σ∪X) is a set of formulae defined by the grammar φ::=⊤∣⊥∣φ1∧φ2∣φ1∨φ2∣s∣x⋈c∣x.φ where
s∈S, and x.φ is a binding construct corresponding to resetting the clock x to 0.
The notation Φ(S∪Σ∪X) thus allows boolean combinations
as defined above of locations, symbols of Σ, clock constraints and ⊤,⊥, with or without
the binding construct (x.). A configuration of a 1-clock ATA is a set consisting of locations along with their clock valuation.
Given a configuration C,
we denote by δ(C,a) the configuration D obtained by applying
δ(s,a) to each location s such that (s,ν)∈C.
A run of the 1-clock ATA starts from the initial configuration
{(s0,0)}, and proceeds with alternating time elapse transitions and
discrete transitions obtained on reading a symbol from Σ. A configuration is accepting iff it is either empty, or
is of the form {(s,ν)∣s∈F}.
The language accepted by a 1-clock ATA A, denoted
L(A) is the set of all timed words ρ such that starting
from {(s0,0)}, reading ρ leads to an accepting configuration.
A po-1-clock ATA is one in which
(i) there is a partial order denoted ≺ on the locations, such that whenever
sj appears in Φ(si), sj≺si, or sj=si.
Let ↓si={sj∣sj≺si}, (ii) x.s does not appear in δ(s,a) for all s∈S,a∈Σ.
Example 4.2**.**
Consider the po-1-clock ATA A=({a,b},{s0,sa,sℓ},s0,{s0,sℓ},δ) with transitions
δ(s0,b)=s0,δ(s0,a)=(s0∧x.sa)∨sℓ,
δ(sa,a)=(sa∧x<1)∨(x>1)=δ(sa,b), and
δ(sℓ,b)=sℓ,δ(sℓ,a)=⊥.
The automaton accepts all strings where every non-last a
has no symbols at distance 1 from it, and has some symbol
at distance >1 from it.
Lemma 4.3**.**
po-1-clock ATA and 1−TPTL are equivalent in expressive power.
The translation from 1−TPTL to po-1-clock ATA is easy, as in the
translation from MTL to po-1-clock ATA. For the reverse direction,
we start from the lowest location (say s) in the partial order, and
replace the transitions of s by a 1-TPTL formula that models timed words which are accepted,
when started in s. The accepting behaviours
of each location s, denoted Beh(s) is computed bottom up. The 1-TPTL formula
that we are looking for is Beh(s0) where s0 is the initial location.
In example 4.2, Beh(sℓ)=□nsb,
Beh(sa)=(x<1)Uns(x>1),
Beh(s0)=[(a∧x.OBeh(sa))∨b]W(a∧OBeh(sℓ))
=((a∧(x.O[(x<1)Unsx>1]))∨b)W(a∧O□nsb).
Step by step details for Lemma 4.3 can be seen in Appendix H.
We next show that starting from a SfrMTL formula φ, we can construct
an equivalent 1−TPTL formula ψ.
The proof of Lemma 4.4 can be found in Appendix I.
Lemma 4.4**.**
SfrMTL⊆1−TPTL**
The idea is to iteratively keep replacing the Rat modality level by level, starting with the innermost one,
until we have eliminated the topmost one.
Consider the SfrMTL formula φ=Rat(0,1)[Rat(1,2)(a+b)∗].
To eliminate
Rat(1,2)(a+b)∗ at a point, we freeze a clock x, and wait till x∈(1,2),
and check (a+b)∗ on this region. The LTL formula for (a+b)∗ is □(a∨b).
Treating x∈(1,2) as a proposition, we obtain
ζ=x.(x∈/(1,2)U[ψ1∧ψ2]) where
ψ1=x∈(1,2)∧[x∈(1,2)UO(□(x∈/(1,2)))] and
ψ2=□[x∈(1,2)→(a∨b)].
ζ asserts □(a∨b)
exactly on the region (1,2), eliminating the modality Rat(1,2). To eliminate
the outer Rat(0,1), we
assert the existence of a point in (0,1) where Rat(1,2)(a+b)∗ is true by saying
x.(x∈/(0,1)U([x∈(0,1)∧ζ∧O(□(x∈/(0,1)))])).
This is 1-TPTL equivalent to φ.
Lemma 4.5**.**
*(po-1-clock ATA to SfrMTL)
Given a po-1-clock ATA A, we can construct a SfrMTL formula
φ such that L(A)=L(φ).*
Proof 4.6**.**
(Sketch)
We give a proof sketch here, a detailed proof can be found in Appendix J.
Let A be a po-1-clock ATA with locations S={s0,s1,…,sn}.
Let K be the maximal constant used in the guards x∼c occurring in the transitions.
Let R2i=[i,i],R2i+1=(i,i+1),0≤i<K and RK+=(K,∞) be the regions
R of x. Let Rh≺Rk denote that region Rh
precedes region Rk.
For each location s, Beh(s) as computed in Lemma 4.3 is a 1-TPTL formula that gives the timed behaviour starting at s,
using constraints x∼c since the point where x was frozen.
In example 4.2, Beh(sa)=(x<1)Uns(x>1), allows symbols a,b as long as x<1
keeping the control in sa, has no behaviour at x=1, and allows
control to leave sa when x>1.
For any s, we “distribute” Beh(s) across regions by untiming it. In example 4.2,
Beh(sa) is □ns(a∨b) for regions R0,R1, it is ⊥ for R2 and
is (a∨b) for R1+. Given any Beh(s), and a pair of regions Rj⪯Rk, such that
s has a non-empty behaviour in region Rj, and control leaves s in Rk,
the untimed behaviour of s between regions Rj,…,Rk is written as LTL formulae
φj,…,φk. This results in a “behaviour description” (or BD for short)
denoted BD(s,Rj,Rk) : this is a 2K+1 tuple with BD[Rl]=φl
for j≤l≤k, and BD[R]=⊤ denoting “dont care” for the other regions.
Let BDSet(s) denote the set of all BDs for a location s.
For the initial location s0, consider all BD(s0,Rj,Rk)∈BDSet(s0)
that have a behaviour starting in Rj, and ends in an accepting configuration in Rk.
Each LTL formula BD(s0,Rj,Rk)[Ri] (or BD[Ri] when s,Rj,Rk are clear)
is replaced with a star-free rational expression
denoted re(BD(s0,Rj,Rk)[Ri]). Then BD(s0,Rj,Rk)
is transformed into a SfrMTL formula φ(s0,Rj,Rk)=⋀j≤g≤kRatRgre(BD(s0,Rj,Rk)[Rg]).
The language accepted by the po-1-clock ATA A is then given by
⋁0≤j≤k≤2Kφ(s0,Rj,Rk).
Computing BD(s,Ri,Rj) for a location s and pair of regions Ri⪯Rj.
We first compute BD(s,Ri,Rj) for locations s which are lowest in the partial order, followed
by computing BD(s′,Ri,Rj) for locations s′ which are higher in the order.
For any location s, Beh(s) has the form φ or φ1Wφ2
or φ1Unsφ2, where φ,φ1,φ2
are disjunctions of conjunctions over Φ(S∪Σ∪X), where S is the set of locations
with or without the binding construct x., and X is a set of clock constraints
of the form x∼c. Each conjunct
has the form ψ∧x∈R where ψ∈Φ(Σ∪S) and R∈R.
Let φ1=⋁(Pi∧Ci),φ2=⋁(Qj∧Ej) where Pi,Qj∈Φ(Σ∪S) and Ci,Ej∈R.
Let C and E be shorthands for any Ck,El.
If Beh(s) is an expression without U,W (the case of φ above),
then BD(s,Ri,Ri) is defined for a region Ri if φ=⋁(Qj∧Ej)
and there is some El with x∈Ri. It is a 2K+1 tuple with BD(s,Ri,Ri)[Ri]=Ql, and
the rest of the entries are ⊤ (for dont care). If Beh(s) has the form
φ1Wφ2 or φ1Unsφ2, then
for Ri⪯Rj, and a location s, BD(s,Ri,Rj)
is a 2K+1 tuple with
(i) formula ⊤ in regions R0,…,Ri−1,Rj+1,…,RK+,
(ii) If Ck=El=(x∈Rj) for some Ck,El, then the LTL formula in region Rj is PkUQl if s is not accepting,
and is PkWQl if s is accepting, (iii) If no Ck is equal to any El, and
if El=(x∈Rj) for some l, then the formula in region Rj is Ql. If Cm=(x∈Ri) for some m, then
the formula for region Ri is □nsPm. If there is some Ch=(x∈Rw) for i<w<j, then
the formula in region Rw is □nsPh∨ϵ, where ϵ signifies that
there may be no points in regions Rw. If there are no Cm’s such that Cm=(x∈Rw)
for Ri≺Rw≺Rj, then the formula in region Rw is ϵ.
ϵ is used as a special symbol in LTL whenever there is no behaviour
in a region.
BD(s,Ri,Rj)** for location s lowest in po***. Let s be a location that is lowest in the partial order.
In general, if s is the lowest in the partial order, then
Beh(s) has the form φ1Wφ2
or φ1Unsφ2 or φ where φ,φ1,φ2
are disjunctions of conjunctions over Φ(Σ∪X). Each conjunct
has the form ψ∧x∈R where ψ∈Φ(Σ) and R∈R.
See Figure 4, with regions R0,R1,R2,R1+, and some example *BD*s.
In Figure 4,
using the *BDs of the lowest location s3, we write
the SfrMTL formula for Beh(s3) :
ψ(s3)=φR0(s3)∧φR1(s3)∧φR2(s3)∧φR1+(s3), where
each φR
describes the behaviour of s3
starting from region R.
For a fixed region Ri, φRi(s3) is
⋀Rg≺RiRatRgϵ∧RatRiΣ+→{⋁Ri≺Rjφ(s3,Ri,Rj)}, where
φ(s3,Ri,Rj) is described above. RatRgϵ means that
there is no behaviour in Rg.
φR0(s3) is given by
RatR0Σ+→{(RatR0a∗∧RatR1[a∗+ϵ]∧RatR2[a∗+ϵ]∧RatR1+[a∗+a∗b])}.
BD(s,Ri,Rj)** for a location s which is higher up***.
If s is not the lowest in the partial order, then Beh(s)
can have locations s′∈↓s. s′ occurs as O(s′) or x.O(s′) in
Beh(s).
For x.OBeh(s3) in BD(s,Ri,Rj), since the clock is frozen, we plug-in the SfrMTL formula ψ(s3) computed above
for x.OBeh(s3) in BD(s1,Ri,Rj).
For instance, in figure 4, x.OBeh(s3)
appears in BD(s2,R2,R2)[R2].
We simply plug in the SfrMTL formula ψ(s3) in its place.
Likewise, for locations s,t, if OBeh(t) occurs in
BD(s,Ri,Rj)[Rk],
we look up BD(t,Rk,Rl)∈BDSet(t) for all Rk⪯Rl
and combine BD(s,Ri,Rj),BD(t,Rk,Rl)
in a manner described below. This is done to detect
if the “next point” for t has a behaviour in Rk or later.*
*If the next point for t is in Rk itself, then we combine
BD1=BD(s,Ri,Rj) with
BD2∈{BD(t,Rk,Rl)∣Rk⪯Rl}⊆BDSet(t) as follows.
combine(BD1,BD2) results in BD3 such that
BD3[R]=BD1[R] for R≺Rk,
BD3[R]=BD1[R]∧BD2[R] for Rk≺R, where ∧ denotes component wise conjunction.
BD3[Rk] is obtained by replacing OBeh(s2) in BD1[Rk]
with BD2[Rk]. Doing so enables the next point
in Rk, emulating the behaviour of t in Rk.
*
Assume the next point for t lies in Rb, Rk≺Rb.
The difference with case (a) is that we combine
BD1=BD(s,Ri,Rj) with BD2∈{BD(t,Rb,Rl)∣Rk≺Rb⪯Rl}⊆BDSet(t).
Then combine(BD1,BD2) results in a BD, say BD3 such that
BD3[R]=BD1[R] for R≺Rk,
BD3[R]=BD1[R]∧BD2[R] for all Rb⪯R, and
BD3[R]=ϵ for Rk≺R≺Rb. The OBeh(t)
in BD1[Rk] is replaced with □⊥ to signify that
the next point is not enabled for t.
See Figure 5 where Rb=R2. The conjunction
with □⊥ in R0 signifies that the next point for s2 is not in R0;
the ϵ in R1 signifies that
there are no points in R1 for s2. Conjuncting □⊥
in a region signifies that the next point
does not lie in this region.
*We look at the “accepting” *BD*s in BDSet(s0), viz., all BD(s0,Rj,Rk),
such that acceptance happens in Rk, and s0 has a behaviour starting in Rj.
The LTL formulae BD(s0,Rj,Rk)[R] are replaced with
star-free expressions re(BD(s0,Rj,Rk)[R]).
Each accepting BD(s0,Rj,Rk) gives an SfrMTL formula
⋀Rj⪯R⪯RkRatRre(BD(s0,Rj,Rk)[R]). The disjunction of these across all accepting *BDs
is the SfrMTL formula equivalent to L(A).
5 Discussion
We propose RatMTL which significantly increases the expressive power of MTL
and yet retains decidability over pointwise finite
words.
The Rat operator added to MTL syntactically subsumes several other modalities in literature including threshold counting, modulo counting
and the pnueli modality. Decidability of RatMTL
is proved by giving an equisatisfiable reduction to MTL
using oversampled temporal projections. This reduction has elementary complexity and allows us to identify two
fragments of RatMTL with 2EXPSPACE and EXPSPACE satisfibility.
In previous work [10], oversampled temporal projections were used to
reduce MTL with punctual future and non-punctual past to MTL. Our reduction
can be combined with the one in [10] to obtain decidability of RatMTL and elementary decidability
of MITL+URat + non-punctual past. These are amongst the most expressive decidable
extensions of MTL known so far.
We also show an exact logic-automaton correspondence between the fragment SfrMTL and
po-a-clock ATA. Ouaknine and Worrell reduced MTL to po-1 clock ATA. Our SfrMTL achieves the
converse too. It is not difficult to see that full RatMTL can be reduced to equivalent 1 clock alternating timed automata. This provides
an alternative proof of decidability of RatMTL but the proof will not extend to decidability of RatMTL+ non-punctual past, nor prove elementary
decidability of MITL+URat+non-punctual past. Hence, we believe that our proof technique has some advantages.
An interesting related formalism of timed regular expressions was defined by Asarin, Maler, Caspi, and shown to be expressively equivalent
to timed automata. Our RatMTL has orthogonal expressivity, and it is boolean closed.
The exact expressive power of RatMTL which is between 1-clock ATA and po-1-clock ATA is open.
Appendix A Rational Expressions and Star-Free Expressions
We briefly introduce rational expressions and star-free expressions over an alphabet Σ.
A rational expression over Σ is constructed inductively
using the atomic expressions a∈Σ,ϵ,∅
and combining them using concatenation, Kleene-star and union.
A star-free expression also has the same atomic expressions, and allows combination using
union, concatenation and complementation.
For instance, Σ∗ is star-free since it can be written as ¬∅.
Appendix B Exclusive Normal Form
We eliminate RatI\and and xURatI′,\andy respectively from temporal definitions
□ns[w↔RatI\and] or □ns[w↔xURatI′,\andy].
The idea is to first mark each point of the timed word ρ over Σ∪W
with the information whether \and is true or not at that point, obtaining a simple extension ρ′
of ρ, and then to refine
this information by checking if \and is true within an interval I.
Assume \and=re(S). To say that re(S) is true starting at a point in the timed word, we have to look at the truth of subformulae in S. The alphabet of the minimal DFA to check re(S) is hence 2S=S′. This results in the minimal DFA
accepting an expression re′(S′), and not re(S). In the following, we show that
re′(S′) is equivalent to re(S).
The first thing we do to avoid dealing with sets of formulae of S being true at each point is to assume that
the sets S are exclusive: that is, at any point, exactly one formula from S can be true.
If the sets S are all exclusive, then the formula is said to be in
Exclusive Normal Form.
If S is exclusive, then we will be marking positions in the word
over S and not P(S). This way, the untimed words
Seg(S,i,j) as well as TSeg(S,i,I) that were used in the semantics
of φ1URatI,re(S)φ2, RatI,re(S) respectively
will be words over S. The satisfaction of φ1URatI,re(S)φ2, RatI,re(S) at any point i will then amount to simply checking
if Seg(S,i,j),TSeg(S,i,I)∈L(re(S)).
We now show that the exclusiveness of S can be achieved by a simple translation.
Lemma B.1**.**
Given any RatMTL formula φ of the form RatI,re(S)S or φ1URatI,re(S)Sφ2,
there exists an equivalent formula ψ∈RatMTL in exclusive normal form.
Proof B.2**.**
Let S={ϕ1,…,ϕn}. Construct set S′ consisting
of all formulae of the form ⋀i∈Kϕi∧⋀i∈/K¬ϕi for all possible subsets K⊆{1,2,…,n}.
Consider any formula of the form RatI(re(S)).
Let Wi denote the set consisting of all subsets of {1,2,…,K} which contains i.
The satisfaction of φi is then equivalent to that of W∈Wi∑ϕW.
We can thus replace any φi occurring in re(S) with W∈Wi∑ϕW.
This results in obtaining a rational expression re′ over S′.
It can be shown that re(S) is equivalent to re′(S′) by inducting on the structure of re.
Thus, the minimal DFA we construct for re(S) in the temporal definition will end up
accepting re′(S′), equivalent to re(S).
Appendix C 1-TPTL for Rat[l,u)\and
We encode in 1-TPTL an accepting run going through a sequence of merges capturing Rat[l,u)\and
at a point e.
To encode an accepting run going through a sequence of merges capturing Rat[l,u)\and
at a point e, we assert φchk1∨φchk2 at e, assuming l=0.
If l=0, we assert φchk3. Recall that m is the number of states in the minimal DFA accepting \and.
Let cond1=0≤n<m, and
Let cond2=1≤i1<i2<…<in<i≤m.
φchk1=cond1⋁cond2⋁x.◊(x<l∧O[(x≥l)∧GoodRun])
φchk2=cond1⋁cond2⋁x.(O[(x≥l)∧GoodRun])
φchk3=cond1⋁cond2⋁x.GoodRun
where
GoodRun is the formula which describes the run starting in q1 in thread Thi, going through a sequence of merges, and
witnesses qf in a merged thread Thi1 at a point when x∈[l,u), and is the maximal point in [l,u).
GoodRun is given by Thi(q1)∧[{¬Mrg(i)}U[merge(in,i)∧{¬Mrg(in)}U[merge(in−1,in)…{¬Mrg(i2)}U[merge(i1,i2)∧q∈QF⋁Nxt(Thi1(q))∧x∈[l,u)∧O(x>u)]…]]]]
where Mrg(i) is the formula j<i⋁merge(j,i).
The idea is to freeze the clock at the current point e, and start checking a good run from the first point in the interval [l,u).
φchk1 is the case when the next point after point e is not at distance [l,u)
from e, while φchk2
handles the case when the next point after e is at distance [l,u) from e. In both cases, l>0. (If l=0, we assert φchk3).
Let Thi be the thread
having the initial state q1 in the start of the interval I.
Let i1 be the index of the thread to which Thi eventually merged (at the last point in the interval [l,u) from e).
The next expected state of thread Thi1 is one of the final states if and only if the sub-string within the interval [l,u) from the point e satisfies the regular expression \and. Note that when the frozen clock is ≥l,
we start the run with Thi(q1), go through the merges, and check that
x∈I when we encounter a thread Thi1(qf), with qf being a final state.
To ensure that we have covered checking all points in τe+I, we ensure that at the next point after
Thi1(qf), x>u. The decidability of 1−TPTL gives the decidability
of RatMTL.
Appendix D Proof of Lemma 3.3
Proof D.1**.**
Starting with the simple extension ρ′ having the information about the runs of A\and,
we explain the construction of the oversampled extension ρ′′ as follows:
*We first oversample ρ′ at all the integer timestamps and mark them with propositions in C={c0,…,cmax−1} where max is the maximum constant used in timing constraints of the input formulae.
An integer timestamp k is marked ci if and only if k=M(max)+i where M(max) denotes a non-negative integral multiple of max and
0≤i≤max−1. This can be done easily by the formula *
c0∧i∈{0,…max−1}⋀□ns(ci→¬◊(0,1)(⋁C)∧◊(0,1]ci⊕1)*
where x⊕y is addition of x,y modulo max.*
Next, a new point marked ovs is introduced at all time points τ whenever τ−l or τ−u is marked with ⋁Σ.
This ensures that for any time point t in ρ′′, the points t+l,t+u are also available
in ρ′′.
*After the addition of integer time points, and points marked ovs, we obtain the
oversampled extension (Σ∪W∪Threads∪Merge,C∪{ovs}) ρ′′
of ρ′.
To check the truth of Rat[l,u)\and at a point v,
we need to assert the following: starting from the time point τv+l,
we have to check the existence of an accepting run R in A\and
such that the run starts from the first action point in the interval [τv+l,τv+u), is a valid run which goes through some possible sequence of merging of threads, and
witnesses a final state at the last action point in [τv+l,τv+u). To capture this, we start
at the first action point in [τv+l,τv+u) with initial state q1
in some thread Thi, and proceed for some time with Thi active, until we reach a point
where Thi is merged with some Thi1. This is followed by Thi1 remaining active until
we reach a point where Thi1 is merged with some other thread Thi2 and so on, until we reach
the last such merge where some thread say Thn witnesses a final state at the last action point
in [τv+l,τv+u). A nesting of until formulae captures this sequence of merges of the threads,
starting with Thi in the initial state q1. Starting at v,
we have the point marked ovs at τv+l, which helps us to anchor there and
start asserting the existence of the run.*
The issue is that the nested until can not
keep track of the time elapse since τv+l.
However, note that the greatest integer point in [τv+l,τv+u) is uniquely marked
with cj⊕u whenever cj≤τv≤cj⊕1 are the closest integer points to τv.
We make use of this by (i) asserting the run of A\and
until we reach cj⊕u from τv+l. Let the part of the run R that has been witnessed until
cj⊕u be Rpref. Let R=Rpref.Rsuf be the accepting run. (ii) From τv+l, we jump to τv+u, and
assert the reverse of Rsuf till we reach cj⊕u. This ensures that
R=Rpref.Rsuf is a valid run in the interval [τv+l,τv+u).
Let Mrg(j)=[k<j⋁merge(k,j)∨cj⊕u].
We first write a formula that captures Rpref. Given a point v, the formula
captures a sequence of merges through threads i>i1>⋯>ik1,
and m is the number of states of A\and.
Let φPref,k1=⋁m≥i>i1>⋯>ik1MergeseqPref(k1) where MergeseqPref(k1) is the formula
[TABLE]
[TABLE]
Note that this asserts the existence of a run till ci⊕u going through a sequence of merges starting at τv+l. Also, Thik1 is the guessed
last active thread till we reach ci⊕u which will be merged
in the continuation of the run from ci⊕u.
Now we start at τv+u
and assert that we witness a final state sometime as part of some thread Thik,
and walk backwards such that some thread it got merged to ik, and so on,
we reach a thread Thic to which thread Thik1 merges with.
Note that Thik1
was active
when we reached ci⊕u. This thread Thik1 is thus the “linking point” of the forward and reverse runs. See Figure 6.
*Let φSuf,k,k1=⋁1≤ik<⋯<ik1≤mMergeseqSuf(k,k1)
where MergeseqSuf(k,k1) is the formula
◊[u,u]{¬(⋁Σ∨ci⊕u)S[(Thik(qf))∧(¬Mrg(ik)S*
[merge(ik,ik−1)∧(¬Mrg(ik−1)S
[merge(ik−1,ik−2)∧…merge(ic,ik1)∧(¬Mrg(ik1)Sci⊕u)])])]}.*
For a fixed sequence of merges, the formula
[TABLE]
captures an accepting run
using the merge sequence. Disjuncting over all possible sequences for a starting thread Thi, and disjuncting over all
possible starting threads gives the required formula capturing an accepting run.
Note that
this resultant formulae is also relativized with respect to Σ and also conjuncted with
Rel(Run,Σ) (where Run is the formula capturing the run information in ρ′ as seen in section 3.1) to obtain the equisatisfiable MTL formula. The relativization of Run with respect to Σ
can be done as illustrated in Figure 1.)
Note that S can be eliminated obtaining an equisatisfiable MTL[UI] formula
modulo simple projections [16].
If I was an unbounded interval of the form [l,∞), then in formula φk,k1, we do not require MergeseqSuf(k,k1); instead,
we will go all the way till the end of the word, and assert Thik(qf) at the last action point of the word.
Thus, for unbounded intervals, we do not need any oversampling at integer points.
Appendix E Elimination of URatI,re
Lemma E.1**.**
Let T=□ns[a↔xURatI,rey] be a temporal definition built from Σ∪W.
Then we synthesize a formula ψ∈MTL
over Σ∪W∪X such that T is equivalent to ψ modulo oversampling.
Proof E.2**.**
We discuss first the case of bounded intervals.
The proof technique is very similar to Lemma 3.3. The differences that arise are as below.
-
Checking re in RatIre at point v is done at all points j such that τj−τv∈I.
To ensure this, we needed the punctual modalities ◊[u,u],◊[l,l].
On the other hand, to check URatI,re from a point v, the check on re is done from the first point after τv, and
ends at some point within [τv+l,τv+u). Assuming τv lies between integer points ci,ci⊕1,
we can witness the forward run in MergeseqPref from the next point after τv till ci⊕1, and
for the reverse run, go to some point in τv+I where the final state is witnessed in a merged thread, and walk back till
ci⊕1, ensuring the continuity of the threads merged across ci⊕1.
The punctual modalities are hence not required
and we do not need points marked ovs.
2. 2.
The formulae MergeseqPref(k1), MergeseqSuf(k,k1)
of the lemma 3.3 are replaced as follows:
MergeseqPref(k1):{¬(⋁Σ∨ci⊕1)U[Thi(q1)∧(¬Mrg(i)U[merge(i1,i)∧(¬Mrg(i1)U
[merge(i2,i1)∧…(¬Mrg(ik1)Uci⊕1)])])]}.
MergeseqSuf(k,k1):◊I{[(Thik(qf))∧(¬Mrg(ik)S*
*[merge(ik,ik−1)∧(¬Mrg(ik−1)S
[merge(ik−1,ik−2)∧*
…merge(ic,ik1)∧(¬Mrg(ik1)Sci⊕1)])])]}*
The above takes care of re in xURatI,rey : we also need to
say that x holds continously from the current point to some point in I. This is done by pushing x into re
(see the translation of φ1URatI,reφ2 to
RatIre′ in Appendix G).
The resultant formulae is relativized with respect to Σ and also conjuncted with
Rel(Run,Σ) to obtain the equisatisfiable MTL formula.
*Now we consider unbounded intervals.
The major challenge for the unbounded case is that the point where we asserting Thik(qf) (call this point w)
may be far away from the point v where we begin : that is, if τv is flanked between integer points
marked ci and ci⊕1, it is possible to see multiple occurrences of
ci⊕1 between τv and
and the point in τv+I which witnesses Thik(qf).
In this case, when walking back reading the reverse of the suffix, it is not easy to stitch
it back to the first ci⊕1 seen after τv.
The possible non-uniqueness of ci⊕1 thus poses a problem in reusing our technique in the bounded interval case.
Thus we consider two cases:
Case 1: In this case, we assume that our point w lies within
[τv+l,⌈τv+l⌉). Note that ⌈τv+l⌉ is the nearest point from v marked with
ci⊕l⊕1. This can be checked by asserting ¬ci⊕l⊕1 all the way till ci⊕1 while walking backward
from w, where Thik(qf) is witnessed.
The formula MergeseqPref(k1) does not change. MergeseqSuf(k,k1) is as follows:
[TABLE]
[TABLE]
*where Mrg′(i)=[j<i⋁merge(j,i)∨ci⊕l⊕1]
Case 2: In this case, we assume the complement. That is the point w occurs after ⌈τv+l⌉. In this case, we assert the prefix till ci⊕l⊕1 and then continue asserting the suffix from this point in the forward fashion unlike other cases. The changed MergeseqPref and MergeseqSuf are as follows:*
MergeseqPref(k1):
[TABLE]
[TABLE]
MergeseqSuf(k,k1):
[TABLE]
[TABLE]
(Thik(qf))])])]}*
where Mrg(i)=[j<i⋁merge(j,i)]*
E.1 Complexity of RatMTL Fragments
Given a formula φ in (MITL or MTL or RatMTL), the size of φ denoted ∣φ∣
is defined by taking into consideration, the number of temporal modalities UI,OI, the number of boolean connectives, as well as the maximal constant occurring in the formulae (encoded in binary). The size is
defined as
logK×(the number of temporal modalities in φ + number of boolean connectives in φ), where
K is the max constant appearing in the formulae.
For example, ∣aU(0,2)(¬b∧cU(0,1)d)∣=log2×4.
In all our complexity results, we assume a binary encoding
of all constants involved in the formulae.
To prove the complexity results we first need the following lemma.
Lemma E.3**.**
Given any MITL formula φ with ∣φ∣=O(2n) (for some n∈N) with maximum constant K used in timing intervals, the satisfiability checking for φ is EXPSPACE in n and log(K).
Proof E.4**.**
Given any MITL formula φ with ∣φ∣=O(2n), there are at most expn=O(2n) number of temporal modalities and boolean connectives. Let K be the maximal constant used in φ.
We give a satisfiability preserving reduction from φ to ψ∈MITL[U0,∞,S].
MITL[U0,∞,S] is the fragment of MITL with untimed
past and the intervals in future modalities
are only of the form ⟨0,u⟩ or ⟨l,∞).
The satisfiability checking for MITL[U0,∞,S] is in PSPACE [1].
Hence, the reduction from a MITL formula with expn=O(2n) number of modalities
to an MITL[U0,∞,S] formula with O(poly(K.expn)) modalities preserving
the max constant K, gives an EXPSPACE upper bound in n,logK. The EXPSPACE hardness of MITL can be found in [1].
The reduction from MITL to MITL[U0,∞,S] is achieved as follows:
- (a)
Break each UI formulae in MITL where I is a bounded interval, into disjunctions of UIi modality, where each Ii is a unit length interval and union of all Ii is equal to I. That is, ϕ1U⟨l,u⟩ϕ2≡ϕ1U⟨l,l+1)ϕ2∨ϕ1U[l+1,l+2)ϕ2…∨ϕ1U[u−1,u⟩ϕ2. This increases the size from expn to expn×K.
2. (b)
Next, we flatten all the modalities containing bounded intervals. This results in replacing subformulae of the form
ϕ1U[l,l+1)ϕ2 with new witness variables. This results in the conjunction
of temporal definitions of the form □ns[a↔ϕ1U[l,l+1)ϕ2] to the formula,
and creates only a linear blow up in the size.
Now consider any temporal definition □ns[a↔ϕ1U[l,l+1)ϕ2].
We show a reduction to an equisatisfiable MITL[U0,∞,S] formula by eliminating each
□ns[a↔ϕ1U[l,l+1)ϕ2] and replacing it with untimed
S and U modalities with intervals <0,u> and <l,∞).
First we oversample the words at integer points C={c0,c1,c2,…,cK−1}.
An integer timestamp k is marked ci if and only if k=M(K)+i, where M(K) denotes a non-negative integer multiple of K, and
0≤i≤K−1.
This can be done easily by the formula
c0∧i∈{0,…K−1}⋀□ns(ci→¬◊(0,1)(⋁C)∧◊(0,1]ci⊕1)**
where x⊕y is (x+y)%K (recall that (x+y)%K=M(K)+(x+y),0≤x+y≤K−1).
Consider any point p within a unit integer interval whose end points are marked ci−1,ci.
Then ϕ1U[l,l+1)ϕ2 is true at that point p if and only if, ϕ1 is true on all the action points till a point j in the future, such that
either j occurs within [l,∞) from p and there is no ci⊕l between p and j (τj∈[τp+l,⌈τp+l⌉]* ) (see figure 7)*
ϕC1,p=(ϕ1∧¬ci⊕l)U[l,∞)ϕ2**
or, j occurs within [0,l+1) from p, and j is within a unit
interval whose end points are marked ci⊕l and ci⊕l⊕1 (τj∈[⌈τp+l⌉,τp+l+1)* ) (see figure 8)*
ϕC2,p=ϕ1U[0,l+1)(ϕ2∧(¬(⋁C))Sci⊕l)**
*The temporal definition □ns[a↔ϕ1U[l,l+1)ϕ2] is then captured by *
i=1⋁K−1□ns[{a∧(¬(⋁C)Uci)}↔ϕC1,i∨ϕC2,i]**
To eliminate each bounded interval modality as seen in (a),(b) above,
we need an O(K) increase in size. Each temporal definition is replaced with a formula with
of size O(K). Thus the size of the new formula is O(2n)×O(K)×O(K), and the total number of propositions needed is 2Σ∪{c0,…,cK−1}. Assuming binary encoding for K, we get a MITL[U0,∞,S] formulae whose size is exponential in n and logK. As the satisfiability checking for MITL[U0,∞,S] is in PSPACE [1], we get an EXPSPACE upper bound
in n,logK. The EXPSPACE hardness of MITL can be found in [1].
E.2 Proof of Theorem 3.1.2 : MITL+UM is EXPSPACE-complete
Starting from an MITL+UM formula, we first show how to obtain an equivalent
MITL formula modulo simple projections. The constants appearing in a MITL+UM formula
come from those which are part of the time intervals I decorating the temporal modalities, as well as
those from counting constraints k%n. If we consider some
U modality, say U(l,u),#b=k%n, then the number of bits needed to encode
this modality is (logl+logu+logk+logn)=O(log(u)+log(n)). Let nmax and
umax be the maximal constants appearing in the counting constraints as well as time intervals
of a MITL+UM formula ϕ. Then
∣ϕ∣=(log(nmax)+log(umax))×(the number of temporal modalities in ϕ+ number of boolean connectives in ϕ).
Elimination of UM
In this section, we show how to eliminate UM
from MTL+UM
over strictly monotonic timed words.
This can be extended to weakly monotonic timed words.
Given any MTL+UM formula φ over Σ, we first
“flatten" the UM modalities
of φ and obtain a flattened formula.
Example. The formula
φ=[aU(e∧(fU(2,3),#b=2%5y))]
can be flattened by replacing the
UM with a fresh witness proposition w to obtain
φflat=[aU(e∧w)]∧□ns{w↔(fU(2,3),#b=2%5y)}.
Starting from χ∈MTL+UM, in the following, we now show how to
obtain equisatisfiable MTL formulae corresponding to each temporal projection containing a UM modality.
-
Flattening : Flatten χ obtaining χflat over Σ∪W, where W is the set of witness propositions
used, Σ∩W=∅.
2. 2.
Eliminate Counting : Consider, one by one,
each temporal definition Ti of χflat.
Let Σi=Σ∪W∪Xi, where Xi is
a set of fresh propositions, Xi∩Xj=∅ for i=j.
For each temporal projection Ti containing a UM modality
of the form xUI,#b=k%ny, Lemma E.5
gives ζi∈MTL over Σi such that ζi
is equisatisfiable to Ti modulo simple extensions.
3. 3.
Putting it all together : The formula
ζ=⋀i=1kζi∈MTL is such that
it is equisatisfiable to modulo simple extensions, over the extra propositions
X=⋃i=1kXi.
For elimination of UM,
marking witnesses correctly is ensured using an extra set of symbols B={b0,...,bn} which act as counters incremented in a circular fashion. Each time a witness of the formula which is being counted is encountered, the counter increments, else it remains same.
The evaluation of the mod counting formulae can be reduced to checking the difference between indices between the first and the last symbol in the time region where the counting constraint is checked.
Construction of Simple Extension
Consider a temporal definition T=□ns[a↔xUMI,#b=k%ny], built from Σ∪W.
Let ⊕ denote addition modulo n+1.
-
Construction of a (Σ∪W,B)- simple extension. We introduce a fresh set of propositions B={b0,b1,…,bn−1} and construct a family of simple extensions
ρ′=(σ′,τ) from ρ=(σ,τ) as follows:
C1: σ1′=σ1∪{b0}. If bk∈σi′
and if b∈σi+1, σi+1′=σi+1∪{bk⊕1}.
C2: If bk∈σi′ and b∈/σi+1, then σi+1′=σi+1∪{bk}.
C3: σi′ has exactly one symbol from B for all 1≤i≤∣dom(ρ)∣.
2. 2.
Formula specifying the above behaviour.
The variables in B help in counting the number of b’s in ρ.
C1,C2 and C3 are written in MTL as follows:
δ1=k=0⋀n□ns[(Ob∧bk)→Obk⊕1] and
δ2=k=0⋀n□ns[(O¬b∧bk)→Obk]
δ3=k=0⋀n□ns[bk→j=k⋀¬bj]
Lemma E.5**.**
Consider a temporal definition
T=□ns[a↔xUI,#b=k%ny], built from Σ∪W.
Then we synthesize a formula ψ∈MTL
over Σ∪W∪X which is equivalent to T modulo simple extensions.
Proof E.6**.**
-
Construct a simple extension ρ′ as shown in section E.2.
2. 2.
Now checking whether at point i in ρ, xUI,#b=k%ny is true, is equivalent to checking that at point i in ρ′ there exist a point j in the future where y is true and for all the points between j and i, x is true and the difference between the index values of the symbols from B at i and j is k%n.
ϕmark,a=□nsi∈{1,…n−1}⋀(a∧bi↔[xUI(y∧bj)])
where j=k+i%n.
3. 3.
The formula δ1∧δ2∧δ3∧ϕmark,a is equivalent to T modulo simple projections.
Notice that in the above reduction, if we start with an MITL+UM formula, we will obtain an MITL formula since we do not introduce any new punctual intervals.
Lemma E.7**.**
Satisfiability of MITL+UM is EXPSPACE-complete.
Proof E.8**.**
Assume that we have a MITL+UM formula ϕ with ∣ϕ∣=m, and hence
≤m UM modalities. Let ϕ be over the alphabet Σ. The number of propositions
used is hence 2Σ, and let
K be the maximal constant appearing in the intervals of ϕ.
Let k1%n1,…,km%nm be the
modulo counting entities in ϕ. Let nmax be the maximum of n1,…,nm.
Going by the construction above, we obtain m temporal definitions T1,…,Tm,
corresponding to the m UM modalities.
To eliminate
each Ti, we introduce nmax formulae of the form ϕmark,a,
evaluated on timed words over 2Σ∪B1∪⋯∪Bm.
This is enforced by δ1,δ2,δ3. The number of propositions
in the obtained MITL formula is hence ∣2Σ∣.∣B1+B2+⋯+Bm∣.
The size of the new formula is
is O(m.nmax), while the maximum constant appearing in the intervals
is same as K. Thus we have an exponential size (the size now is
O(m.2lognmax)) MITL formulae with max constant as K.
The EXPSPACE-hardness of MITL+UM follows from that of MITL.
Lemma E.3 now shows that satisfiability checking for MITL+UM is EXPSPACE-complete.
E.3 Proof of Theorem 3.1.3 : MITL+URat is in 2EXPSPACE
Proof E.9**.**
Consider a URat modality aURatI,re(S)b, where re is a rational expression
over S and a,b∈Σ.
The size of a URat modality is size(re)+log(l)+log(u), where l,u are the lower and upper bounds of the interval I, and
size(re) is the size of the rational expression re.
We first flatten φ by introducing witness propositions for each URat modality obtaining
temporal definitions of the form □ns(w↔URatI,re(S)ψ). Flattening only creates a linear blow up
in formula size.
Assume that φ is flattened.
Let Ti=□ns(wi↔aURatIi,rei(Si)Sibi)
be a temporal definition, and let there be t temporal definitions. Let li,ui be the bounds
of the interval Ii. The size of φ, ∣φ∣ is then defined as
O(∑i=1t(ni+log(li)+log(ui)), where ni is the size of rei. Let u be the maximum
constant appearing in the intervals Ii.
Let us consider a temporal definition T=□ns(w↔URatI,re(S)ψ).
-
We look at the number of propositions needed in obtaining the equisatisfiable MTL formula.
- (a)
The size of the rational expression re in T is n. The DFA accepting re has ≤2n states.
The transitions of this DFA are over formulae from S. Since we convert the formulae into ExNF,
we also convert this DFA into one whose transitions are over 2S.
Hence, the number of transitions
in the DFA is ≤2n×2∣S∣. Let S′=2S.
2. (b)
This DFA is simulated using the symbols Threads,Merge. There can be at most 2n threads, and
each thread be in one of the 2n states. Thus, the number of propositions Thi(q)
is at most 2n2n. Given that there are t temporal definitions, we need t×2n2n extra symbols.
3. (c)
Each integer point in the timed word is marked with a symbol ci, 0≤i≤u−1 (see
the proof of lemma 3.3 in Appendix D).
4. (d)
*The number of propositions *merge(i,j)is ≤2n×2n.
5. (e)
Thus, the number of symbols needed is 2∣Σ∣×u×t×2n2n×(2n×2n).
2. 2.
Next, we count the size of the formulae needed while constructing the equisatisfiable MTL formula.
- (a)
For each temporal definition, we define the formulae Nxt(Thi(qx)) for each thread Thi.
The argument of Nxt can take at most 2n possibilities (2n* states of a DFA) on each of the 2n threads.
Thus, the total number of Nxt(Th(q)) formulae is 2n×2n=O(poly(2n)).
Note that each Nxt formulae simulates the transition function of the DFA.
Nxt(Thi(q′)) is determined depending on the present state q of the thread Thi, and the formulae (in S′) that are true at the present point. Thus, the size of each Nxt formulae is 2n×2∣S∣.
Thus, the total size of all the Nxt formulae is O(poly(2n))×O(poly(2n×2∣S∣))=O(poly(2n+∣S∣).*
2. (b)
Next, we look at formulae NextMerge(i,k).
Note that both the arguments refer to threads, and hence can take at most 2n values. Thus,
the total number of formulae is 2n×2n=O(poly(2n). Each NextMerge formulae
checks whether the states at the 2 threads Thi,Thk are equal or not.
Thus, the size of each formulae is O(2n). The total blow up due to NextMerge formulae is hence,
O(2n×2n×2n)=Opoly(2n).
3. (c)
Next, we look at formulae MergeseqPref(k1).
This formulae states all the possible merges from the present point to the integer point within the interval (l−1,l).
There are at most 2n merges possible, as the merge always happens from a higher indexed thread to a lower one.
The number of merges is equal to the nesting depth of the formula MergeseqPref(k1).
Note that the nesting depth can be at most 2n.
The number of propositions merge(i,j) is 2n×2n. Let there be k≤2n merges
until we see the integer point in (l−1,l). At each of these k merges, we have 2n×2n possibilities,
the maximum possible number of propositions merge(i,j) (i,j≤2n).
Hence, the number of possible merge sequences
we can generate is (2n×2n)k≤(2n×2n)2n. There are 2n possible values of k and the possible number of disjunctions of the formulae is at most (2n×2n)2n×2n=O(poly(2poly(2n))).
4. (d)
The counting for MergeseqSuf(k1,k) is symmetric.
Adding all the blow ups due to various formulae Nxt(Th(q)), NextMerge(i,k), MergeseqPref(k1) and
MergeseqSuf(k1,k), we see the number to be doubly exponential
O(poly(2poly(2n))). Thus, we obtain an MITL formula of doubly exponential size, with doubly exponential number
of new propositions. By applying the reduction as in lemma E.3,
we will obtain a formula in MITL[U0,∞,S], which is still
doubly exponential, and which preserves the max constant. The PSPACE procedure
of MITL[U0,∞,S] thus ensures that we have a
2EXPSPACE procedure for satisfiability checking for MITL+URat. Arriving at a tighter complexity for this class is an interesting problem and is open.
E.4 Proof of Theorem 3.1.4: MITL+MC is Fωω-hard
In this section, we discuss the complexity of MITL+MC, proving
Theorem 3.1.4.
To prove this, we obtain a reduction from the reachability problem of Insertion Channel Machines with Emptiness
Testing (ICMET).
We now show how to encode the reachability problem of ICMET in
MITL+MC.
Recalling ICMET
A channel machine A consists of a tuple having a finite set of states
S, a finite alphabet M used to write on the channels,
a finite set C of channels, and a transition relation Δ⊆S×Op×S
where Op is a finite set of operations on the channels.
These operations have the forms c!a, c?a and c=ϵ which respectively write a message
a to the tail of channel c, read the first message a from a channel c, and test if channel c is empty.
A configuration of the channel machine A is a pair
(s,U) where s is a state and U is a tuple of length ∣C∣
which describes the contents of all the ∣C∣ channels. Each entry in this tuple is hence a string
over the alphabet M. We use Conf to denote the configurations of the channel machine.
The configurations are connected to each other depending on the operations performed. In particular,
- (a)
From a configuration (q,U), the transition
(q,c!a,q′) results in a configuration
(q′,U′) where U′ is the ∣C∣-tuple which does not alter
the contents of channels other than c, and appends a to channel c.
2. (b)
From a configuration (q,U),
the transition (q,c?a,q′)
results in a configuration
(q′,U′) where U′ is the ∣C∣-tuple which does not alter
the contents of channels other than c, and reads a from the head of channel c.
3. (c)
From a configuration (q,U), the transition
(q,c=ϵ,q′) results in the configuration (q′,U) if channel c is empty.
The contents of all the channels are unaltered. If channel c is non-empty, then the machine
is stuck.
If the only transitions allowed are as above, then we call A an error-free channel-machine.
We now look at channel machines with insertion errors. These allow extra transitions between configurations as follows.
- (d)
If a configuration (q,U) can evolve into (q′,V) using one transition
as above, then we allow any configuration (q,U′), where U′ is a ∣C∣-tuple of words
obtained by deleting any number of letters from any word in U,
to evolve into (q′,V′) where V′ is obtained by adding any number of letters
to any word in V. Thus insertion errors are created by
inserting arbitrarily many symbols into some word.
The channel machines as above are called ICMET. A run of an ICMET is a
sequence of transitions γ0→op0γ1…→opn−1γn… that is consistent with the above operational semantics.
Reduction from ICMET reachability to satisfiability of MITL+MC
Consider any ICMET C=(S,M,Δ,C), with
set of states S={s0,…,sn} and channels C={c1,…,ck}. Let M be a finite set of messages used for communication
in the channels.
We encode the set of all possible configurations of C, with a timed language over the alphabet
Σ=Ma∪Mb∪Δ∪S∪{H}, where Ma={ma∣m∈M} Mb={mb∣m∈M},
and H is a new symbol.
-
The jth configuration for j≥0 is encoded in the interval [(2k+2)j,(2k+2)(j+1)−1) where
k refers to number of channels.
The jth configuration begins at the time point (2k+2)j. At a distance
[2i−1,2i] from this point, 1≤i≤k,
the contents of the ith channel are encoded as shown in the point 7. The intervals of the form (2i,2i+1), 0≤i≤k+1 from the start of any configuration are time intervals within which no action takes place.
The current state at the jth configuration is encoded at (2k+2)j, and the transition
that connects configurations j,j+1 is encoded at (2k+2)j+(2k+1).
-
Lets look at the encoding of the contents of channel i in the jth configuration.
Let mhi be the message at the head of the channel i. Each message mi is encoded using consecutive occurrences of symbols mi,a and mi,b.
In our encoding of channel i, the first point marked mhi,a in the interval (2k+2)j+[2i−1,2i] is the head of the channel i and denotes that mhi is the message at the head of the channel. The last point marked mti,b in the interval is the tail of the channel,
and denotes that message mti is the message stored at the tail of the channel.
-
Exactly at 2k+1 time units after the start of the jth configuration, we encode the transition
from the state at the jth configuration to the (j+1)st configuration (starts at (2k+2)(j+1)).
Note that the transition has the form (s,c!m,s′) or (s,c?m,s′) or (s,c=ϵ,s′).
4. 4.
We introduce a special symbol H, which acts as separator between the head
of the message and the remaining contents, for each channel.
5. 5.
A sequence of messages w1w2w3…wz in any channel is encoded as a sequence
w1,aw1,bHw2,aw2,bw3,aw3,b…wz,awz,b.
Let S=⋁i=0nsi denote the states of the ICMET,
α=⋁i=0mαi, denote the transitions αi of the form (s,c!m,s′) or (s,c?m,s′) or (s,c=ϵ,s′).
Let action=true and let Ma=⋁mx∈M(mx,a), Mb=⋁mx∈M(mx,b), with M=Ma∨Mb.
-
All the states must be at distance 2k+2 from the previous state (first one being at 0) and all the propositions encoding transitions must be at the distance 2k+1 from the start of the configuration.
φS=\leavevmode s0∧□[S⇒{◊(0,2k+2](S)∧□(0,2k+2)(¬S)∧◊(0,2k+1]α∧□[0,2k+1)(¬α)∧◊(2k+1,2k+2)(¬α)}]
2. 2.
All the messages are in the interval [2i−1,2i] from the start of configuration. No action takes place at (2i−2,2i−1) from the start of any configuration.
φm=\leavevmode □{S⇒⋀i=1k□[2i−1,2i](M∨H)∧
□(2i−2,2i−1)(¬action)}
3. 3.
Consecutive source and target states must be in accordance with a transition α. For example, sj appears consecutively after si
reading αi iff αi is of the form (si,y,sj)∈Δ, with y∈{ci!m,ci?m,ci=ϵ}.
φΔ=⋀s,s′∈S□{(s∧◊(0,2k+2]s′)⇒(◊(0,2k+1]⋁Δs,s′)}
where Δs,s′ are possible αi between s,s′.
4. 4.
We introduce a special symbol H along with other channel contents which acts as a separator between the
head of the channel and rest of the contents. Thus H has following properties
There is one and only one time-stamp in the interval (2i−1,2i) from the start of the configuration where H is true. The following formula says that there is an occurrence of a H:
φH1=□[(S∧◊(2i−1,2i)M)⇒(⋀i=1k◊(2i−1,2i)(H))]
The following formula says that there can be only one H:
φH2=□(H⇒¬◊(0,1)H)
Every message mx is encoded by truth of proposition mx,a immediately followed by mx,b. Thus for any message mx, the configuration encoding the channel contents has a sub-string of the form (mx,amx,b)∗ where mx is some message in M.
φm=□[mx,a⇒O(0,1]mx,b]∧□[mx,b⇒O(0,1)Ma
∨O(⋁Δ∨H)]∧(¬MbUMa)
If the channel is not empty (there is at least one message mamb in the interval (2i−1,2i) corresponding to channel i contents) then there is one and only one mb before H.
The following formula says that there can be at most one mb before H.
φH3=□[¬{Mb∧◊(0,1)(Mb∧◊(0,1)H)}]
The following formula says that there is one Mb before H in the channel, if the channel is non-empty.
φH4=□[S⇒{⋀j=1k(◊[2j−1,2j](Mb)⇒
◊[2j−1,2j](Mb∧◊(0,1)H))}]
Let φH=φH1∧φH2∧φH3∧φH4.
5. 5.
Encoding transitions:
We first define a macro for copying the contents of the ith channel to the next configuration with insertion errors.
If there were some mx,a,mx,b at times t,t′, mx,b is copied to
t′′+2k+2 (where t′′∈[t,t′)), representing the channel contents in the next configuration. This is specified by means of an even count check.
From any 3 consecutive points u,v,w such that mx,a and mx,b are true at v and w, respectively,
we assert that there are even (or odd) number of mx,b within (0,2k+2) from both v and w.
This implies that there must be an odd number of mx,b’s within time interval [τv+2k+2,τw+2k+2]. Thus, there must be at least one mx,b copied from the point w to some point in the interval [τv+2k+2,τw+2k+2]. The rest of the even number of erroneous mx,b in [τv+2k+2,τw+2k+2], along with the arbitrary insertion errors within [τu+2k+2,τv+2k+2] models the insertion error of the ICMET (see Figure 11). The formula copyg is as follows.
□[2i−1,2i][⋀mx∈M(mx,a∧iseven(0,2k+2)(mx,b))⇒O(iseven(0,2k+2)(mx,b))]∧□[2i−1,2i][⋀mx∈M(mx,a∧¬iseven(0,2k+2)(mx,b))⇒O(¬iseven(0,2k+2)(mx,b))]
If the transition is of the form ci=ϵ. The following formulae checks that there are no events in the interval
(2i−1,2i) corresponding to channel i,
while all the other channel contents are copied.
φci=ϵ=S∧□(2i−1,2i)(¬action)∧g=1⋀kcopyg
If the transition is of the form ci!mx where m∈M. An extra message is appended to the tail of channel i, and all the mamb’s are copied to the next configuration.
Mb∧□(0,1)(¬M)) denotes the last time point of channel i; if this occurs at time t,
we know that this is copied at a timestamp strictly less than 2k+2+t (by 5(a)). Thus we assert that
truth of ◊(2k+2,2k+3)mx,b at t.
φci!m=S∧g=1⋀kcopyg∧◊[2i−1,2i){(M∧□(0,1)(¬M))⇒(◊(2k+2,2k+3)(mx,b))}
If the transition is of the form ci?m where m∈M. The contents of all channels other than i are copied to the intervals encoding corresponding channel contents in the next configuration. We also check the existence of a first message
in channel i; such a message has a H at distance (0,1) from it.
φci?mx=S∧j=i,g=1⋀kcopyg∧◊(2i−1,2i){mx,b∧◊(0,1)(H)}∧□[2i−1,2i][⋀mx∈M(mx,a∧iseven(0,2k+2)(mx,b)∧¬◊(0,1)H)⇒O(iseven(0,2k+2)(mx,b))]∧□[2i−1,2i][⋀mx∈M(mx,a∧¬iseven(0,2k+2)(mx,b)∧¬◊(0,1)H)⇒O(¬iseven(0,2k+2)(mx,b))]
6. 6.
Channel contents must change in accordance to the relevant transition. Let L be a set of labels (names) for the transitions.
Let l∈L and αl be a transition labeled l.
φC=□[S⇒⋀l∈L(◊(0,2k+1](⋁αl⇒φl))]
where φl are the formulae as seen in 5 above (φci?mx,φci!m,φci=ϵ).
7. 7.
Let st be a state of the ICMET whose reachability we are interested in. We check st is reachable from s0 :
ϕreach=◊(st)
Thus the formula encoding ICMET is:
φS∧φΔ∧φm∧φH∧φC∧φreach
This is a formula in MITL+UM, and we have reduced the reachability problem
of ICMET with insertion errors to
checking satisfiability of this formula.
Appendix F Non-punctual 1-TPTL is NPR
In this section, we show that non-punctuality does not provide any benefits in terms of complexity
of satisfiability for TPTL as in the case of MITL.
We show that satisfiability checking of non-punctual TPTL is itself non-primitive recursive.
This highlights the importance of our oversampling reductions from RatMTL and RatMITL
to MTL and MITL respectively, giving RegMITL an elementary complexity.
It is easier to reduce RatMITL[URat] to 1-variable, non-punctual, TPTL without using oversampling, but this
gives a non-primitive recursive bound on complexity. Our reduction of RatMITL[URat] to equisatisfiable MITL using oversampling, however
has a 2EXPSPACE upperbound.
Non-punctual TPTL with 1 Variable (1−OpTPTL)
We study a subclass of 1−TPTL called open 1−TPTL and denoted as 1−OpTPTL. The restrictions
are mainly on the form of the intervals used in comparing the clock x as follows:
Whenever the single clock x lies in the scope of even number of negations, x
is compared only with open intervals, and
Whenever the single clock x lies in the scope of an odd number of negations,
x is compared to a closed interval.
Note that this is a stricter restriction than non-punctuality as it can assert a property only within an open timed region.
Our complexity result hence applies to TPTL with non-punctual intervals.
Our hardness result uses a reduction from counter machines.
Counter Machines
A deterministic k-counter machine is a k+1 tuple M=(P,C1,…,Ck), where
-
C1,…,Ck are counters taking values in N∪{0} (their initial values are set to zero);
2. 2.
P is a finite set of instructions with labels p1,…,pn−1,pn.
There is a unique instruction labelled HALT. For E∈{C1,…,Ck}, the instructions P are of the following forms:
- (a)
pi: Inc(E), goto pj,
2. (b)
pi: If E=0, goto pj, else go to pk,
3. (c)
pi: Dec(E), goto pj,
4. (d)
pn: HALT.
A configuration W=(i,c1,…,ck) of M is given by the value of the current program counter i and values c1,c2,…,ck of the counters C1,C2,…,Ck. A move of the counter machine (l,c1,c2,…,ck)→(l′,c1′,c2′,…,ck′) denotes that configuration (l′,c1′,c2′,…,ck′) is obtained from (l,c1,c2,…,ck) by executing the lth instruction pl.
If pl is an increment or decrement instruction, cl′=cl+1 or cl−1, while ci′=ci for i=l and pl′ is the respective
next instruction, while
if pl is a zero check instruction, then ci′=ci for all i, and pl′=pj
if cl=0 and pk otherwise.
Incremental Error Counter Machine (IECM)
An incremental error counter machine (IECM) is a counter machine where a particular configuration can have counter values with arbitrary positive error.
Formally, an incremental error k-counter machine is a k+1 tuple M=(P,C1,…,Ck) where P is a set of instructions like above and C1 to Ck are the counters. The difference between a counter machine with and without incremental counter error is as follows:
-
Let (l,c1,c2…,ck)→(l′,c1′,c2′…,ck′) be a move of a counter machine without error when executing lth instruction.
2. 2.
The corresponding move in the increment error counter machine is
[TABLE]
Thus the value of the counters are non deterministic. We use these machines for proving lower bound complexity in section F.1.
Theorem F.1**.**
[14]** The halting problem for deterministic k counter machines is undecidable for k≥2.
Theorem F.2**.**
[5]** The halting problem for incremental error k-counter machines is non primitive recursive for k≥5.
F.1 Satisfiability Checking for 1−OpTPTL
Theorem F.3**.**
Satisfiability Checking of \mbox{1-\mathsf{OpTPTL}}[\Diamond,\mathsf{O}] is decidable with non primitive recursive lower bound over finite timed words.
Proof F.4**.**
We encode the runs of k counter incremental error counter machine using 1−OpTPTL formulae with ◊,O modalities.
We will encode a particular computation of any counter machine using timed words. The main idea is to construct a \mbox{1-\mathsf{OpTPTL}}[\Diamond,\mathsf{O}] formula φIECM for any given k-incremental counter machine IECM such that φIECM is satisfied by only those timed words that encode the halting computation of IECM.
Moreover, for every halting computation C of the IECM, at least one timed word ρC encodes C
and satisfies φIECM.
We encode each computation of a k-incremental counter machine (P,C) where P={p1,…,pn} is the set of instructions and C={c1,…,ck}
is the set of counters using
timed words over the alphabet ΣIECM=⋃j∈{1,…,k}(S∪F∪{aj,bj}) where S={sp∣p∈1,…,n} and F={fp∣p∈1,…,n} as follows:
The ith configuration, (p,c1,…,ck) is encoded in the timed region [i,i+1) with the sequence
sp(a1b1)c1(a2b2)c2…(akbk)ckfp.
The concatenation of these time segments of a timed word encodes the whole computation.
Untiming our language yields the language
[TABLE]
where S=p∈{1,2,…,n}⋁sp and F=p∈{1,2,…,n}⋁fp.
To construct a formula φIECM, the main challenge is to propagate the behaviour from the time segment
[i,i+1) to the time segment [i+1,i+2) such that the latter encodes the i+1th configuration of the IECM in accordance with the counter values of the ith configuration.
The usual idea is to copy all the a’s from one configuration to another using punctuality. This is not possible in a non-punctual logic.
We preserve the number of as and bs using the following idea:
Given any non last (aj,t)(bj,t′) before F(for some counter cj), of a timed word encoding a computation.
We assert that the last symbol in (t,t+1) is aj and the last symbol in
(t′,t′+1) is bj.
We can easily assert that the untimed sequence of the timed word is of the form
[TABLE]
The above two conditions imply that there is at least one aj within time (t+1,t′+1). Thus, all the non last aj,bj are copied to the segment encoding next configuration.
Now appending one ajbj,two ajbj’s or no ajbj’s depends on whether the instruction was copy, increment or decrement operation.
φIECM* is obtained as a conjunction of several formulae. Let S,F be a shorthand for
p∈{1,…,n}⋀sp and p∈{1,…,n}⋀fp, respectively. We also define macros Aj=w≥j⋁aw and Ak+1=⊥
We now give formula for encoding the machine. Let C={1,…,k} and P={1,…,n} be the indices of the counters and the instructions.*
Expressing untimed sequence*: The words should be of the form*
[TABLE]
This could be expressed in the formula below
φ1=j∈C,p∈P⋀□ns[sp→O(A1∨fp)]∧□ns[aj→O(bj)]∧\leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode \leavevmode □ns[bj→O(Aj+1∨fp)]∧□ns[fp→O(S∨□ns(false))]**
Initial Configuration*: There is no occurrence of ajbj within [0,1]. The program counter value is 1.*
φ2=x.{s1∧O(f1∧x∈(0,1))}**
Copying S,F: Any (S,u) (read as any symbol from
S at time stamp u)
(F,v) (read as (read as any symbol from
F at time stamp v)) has a next occurrence (S,u′), (F,v′) in the future such that
u′−u∈(k,k+1) and v′−v∈(k−1,k).
Note that this condition along with φ1 and φ2 makes sure that S and F occur only
within the intervals of the form [i,i+1) where i is the configuration number. Recall that sn,fn
represents the last instruction (HALT).
φ3=[□nsx.{(S∧¬sn)→¬◊(x∈[0,1]∧S)∧◊(S∧x∈(1,2))}∧□nsx.{(F∧¬fn)→◊(F∧x∈(0,1))}]**
Note that the above formula ensures that subsequent configurations are encoded in
smaller and smaller regions within their respective unit intervals, since consecutive
symbols from S grow apart from each other (a distance >1), while consecutive
symbols from F grow closer to each other (a distance <1). See Figure 13.
Beyond pn=HALT, there are no instructions
φ4 = □ns[fn→□(false)]**
At any point of time, exactly one event takes place. Events have distinct time stamps.
φ6 = [y∈ΣIECM⋀□ns[y→¬(ΣIECM∖{y}⋀(x))]∧□ns[□(false)∨O(x∈(0,∞))]**
Eventually we reach the halting configuration ⟨pn,c1,…,ck⟩: φ6=◊nssn
Every non last (aj,t)(bj,t′) occurring in the interval (i,i+1) should be copied in the interval (i+1,i+2). We specify this
condition as follows:
state that from every non last aj the last symbol within (0,1) is aj.
Similarly from every non last bj, the last symbol within (0,1) is bj.
Thus (aj,t)(bj,t′) will have a (bj,t′+1−ϵ) where ϵ∈(0,t′−t).
Thus all the non last
ajbj will incur a bj in the next configuration. φ1 makes sure that there is an aj between two bj’s. Thus this
condition along with φ1 makes sure that the non last ajbj sequence is conserved. Note that there can be some ajbj which are arbitrarily inserted. These insertions errors model the incremental error of the machine.
Any such inserted (aj,tins)(bj,tins′) in (i+1,i+2) is such that
there is a (aj,t)(bj,t′) in (i,i+1) with tins′∈(t+1,t′+1).
Just for the sake of simplicity we assume that ak+1=false.
*Let nl(aj)=aj∧¬last(aj), nl(bj)=bj∧¬last(bj), ψnh=¬◊(fn∧x∈[0,1]), *
last(aj)=aj∧O(O(F∨Aj+1)))* and last(bj)=bj∧O(F∨Aj+1).*
φ7=j∈C⋀□nsx.[(nl(aj)∧ψnh)→◊(aj∧x∈(0,1)∧O(x∈(1,2)))]∧□nsx.[(nl(bj)∧ψnh)→◊(bj∧x∈(0,1)∧O(x∈(1,2)))]**
We define a short macro CopyC∖W: Copies the content of all the intervals encoding counter values except counters in W. Just for the sake of simplicity we denote
CopyC∖W=j∈C∖W⋀□nsx.{last(aj)→(aj∧x∈(0,1)∧O(bj∧x∈(1,2)∧O(F)))}**
Using this macro we define the increment,decrement and jump operation.
-
Consider the zero check instruction pg: If Cj=0 goto ph, else goto pd. δ1 specifies the next configuration when the check for zero succeeds. δ2 specifies the else condition.
φ8g,j=0 = CopyC∖{∅}∧δ1∧δ2**
δ1=□ns[{sg∧((¬aj)UF)}→(¬S)Ush)]**
δ2=□ns[{sg∧((¬aj)Uaj)}→(¬S)Usd)].
2. 2.
pg: Inc(Cj) goto ph. The increment is modelled by appending exactly one ajbj in the next interval just after the last copied ajbj
φ8g,incj =CopyC∖∅∧□ns(sg→(¬S)Ush)∧ψ0inc∧ψ1inc**
The formula ψ0inc=□ns[(sg∧(¬ajUfg))→(¬SUx.(sh∧◊(x∈(0,1)∧aj))] specifies the increment of the counter j when the value of j is zero.
The formula
ψ1inc=□ns[{sg∧((¬F)U(aj))}→(¬F)Ux.{last(aj)∧◊(x∈(0,1)∧(aj∧OO(last(aj)∧x∈(1,2))))}]
specifies the increment of counter j when j value is non zero by appending exactly one pair of ajbj after the last copied ajbj in the next interval.
3. 3.
pg: Dec(Cj) goto ph. Let second−last(aj)=aj∧O(O(last(aj))). Decrement is modelled by avoiding copy of last ajbj in the next interval.
φ8g,decj = CopyC∖j∧□ns(sg→(¬S)Ush)∧ψ0dec∧ψ1dec**
The formula ψ0dec=□ns[{sg∧(¬aj)Ufg)}→{(¬S)U{sh∧((¬aj)U(F)}] specifies that the counter remains unchanged if decrement is applied to the j when it is zero.
The formula ψ1dec=□ns[{sg∧((¬F)U(aj))}→(¬F)Ux.{second−last(aj)∧◊(x∈(0,1)∧(aj∧OO([Aj+1∨F]∧x∈(1,2))))}] decrements the counter j, if the present value of j is non zero. It does that by disallowing copy of last ajbj of the present interval to the next.
The formula φIECM=i∈{1,…,7}⋀φi∧p∈P⋀φ8p.
Appendix G Details on Expressiveness
Theorem G.1**.**
-
MTL+URat⊆MTL+Rat**
2. 2.
MTL+UM⊆MTL+MC**
Proof G.2**.**
-
We first prove MTL+URat⊆MTL+Rat.
Note that ϕ1URatI,reϕ2 is equivalent to trueURatI,re′S′ϕ2, where re′ is a regular expression obtained by conjuncting
ϕ1 to all formulae ψ occurring in the top level subformulae of re, and S′=S∪{ϕ1}.
For example, if we had aURat(0,1),(Rat(1,2)[Rat(2,3)(b+c)∗])d, then
we obtain trueURat(0,1),(a∧Rat(1,2)[Rat(2,3)(b+c)∗])d.
When evaluated at a point i, the conjunction ensures that ϕ1 holds good at all
the points between i and j, where τj−τi∈I.
To reduce trueURatI,re′S′ϕ2 to a RatI formula, we need the following lemma.
Lemma G.3**.**
Given any regular expression R, there exist
finitely many regular expressions R11,R21,…,R1n,R2n
such that R=⋃i=1nR1i.R2i. That is,
for any string σ∈R and for any decomposition of σ as σ1.σ2,
there exists some i≤n such that σ1∈R1i and σ2∈R2i.
Proof G.4**.**
Let A be the minimal DFA for R. Let the number of states in A be n.
The set of strings that leads to some state qi from the initial state q1 is definable by a regular expression R1i.
Likewise, the set of strings that lead from qi to some final state of A is also definable by some regular expression R2i.
Given that there are n states in the DFA A, we have L(A)=⋃i=1nR1i.R2i.
Consider any string σ∈L(A), and any arbitrary decomposition of σ as σ1.σ2.
If we run the word σ1 over A, we might reach at some state qi. Thus σ1∈L(R1i).
If we read σ2 from qi, it should lead us to one of the final states (by assumption that σ∈R) . Thus σ2∈L(R2i).
Lets consider trueURatI,re′ϕ2 when I=[l,u).111If I=[l,l], then
trueURatI,re′ϕ2=Rat[0,l]re′.ϕ2
If trueURat[l,u),re′ϕ2 evaluates to true at a point i,
we know that ϕ2 holds good at some point j such that τj−τi∈[l,u), and that [Seg(S′,i,j)]single∩L(re′)=∅.
By the above lemma, for any word σ∈L(re′), and any decomposition σ=σ1.σ2, there exist an i∈{1,2,…,n} such that
σ1∈L(R1i) and σ2∈L(R2i).
Thus we decompose at a point j′ with every possible R1k.R2k pair such that
τj′∈τi+[l,u), [TSeg(S,(0,l),i)]single∩L(R1k)=∅,
[TSeg(S,[l,u),i)]single∩L(R2k).ϕ2.Σ∗=∅,
where ϕ2∈S.
Note that (i)ϕ2* holds good at the point j such that τj∈[τi+l,τi+u),
and, (ii) the expression R2k evaluates to true in [l,τj). We simply assert Σ∗ on the remaining part (τj,u)
of the interval.*
Thus trueURat[l,u),re′ϕ2≡i∈{1,2…,n}⋁Rat(0,l)R1i∧Rat[l,u)(R2i.ϕ2.Σ∗).
2. 2.
We first show that the UM modality can be captured by MC.
Consider any formula ϕ1UMI,#ϕ3=k%nϕ2. At any point i this formulae is true if and only if there exists a point j in future such that τj−τi∈I and the number of points between i and j where ϕ3 is true is k%n, and ϕ1 is true at all points between i and j. To count between i and j, we can first count the behaviour ϕ3 from i to the last point of the word, followed by the counting from j to the last point of the word.
Then we check that the difference between these counts to be k%n.
Let cntϕ(x,ϕ3)={ϕ∧MC(0,∞)x%n(ϕ3)}.
Using this macro, ϕ1UMI,#ϕ3=k%nϕ2 is equivalent to
⋁k1=0n−1[ψ1∨ψ2] where
ψ1={cnttrue(k1,ϕ3)∧(ϕ1UIcntϕ2∧¬ϕ3(k2,ϕ3))},
ψ2={cnttrue(k1,ϕ3)∧(ϕ1UIcntϕ2∧ϕ3(k2−1,ϕ3))},
k1−k2=k**
The only difference between ψ1,ψ2 is that in one, ϕ3 holds at
position j, while in the other, it does not. The k2−1 is to avoid the
double counting in the case ϕ3 holds at j.
Appendix H po-1-clock ATA to 1−TPTL
In this section, we explain the algorithm which converts a
po-1-clock ATA A into a 1−TPTL formula
φ such that L(A)=L(φ).
-
Step 1. Rewrite the transitions
of the automaton. Each δ(s,a) can be written in an equivalent form
as (i) C1∨C2 or (ii) C1 or (iii) C2 where
C1 has the form s∧φ1, where φ1∈Φ(↓s∪{a}∪X),
C2 has the form φ2, where φ2∈Φ(↓s∪{a}∪X)
In particular, if s is the lowest location in the partial order,
then φ1,φ2∈Φ({a}∪X). Denote this equivalent form
by δ′(s,a).
For the example above, we obtain
δ′(s0,a)=(s0∧(a∧x.sa))∨(a∧sℓ),δ′(s0,b)=s0∧b,
δ′(sa,a)=(sa∧x<1)∨(x>1)
δ′(sℓ)=(sℓ∧b)
2. 2.
Step 2. For each location s, construct Δ(s) which
combines δ′(s,a) for all a∈Σ, by disjuncting them first, and again
putting them in the form in step 1.
Thus, we obtain Δ(s)=⋁aδ′(s,a)
which can be written as a disjunction D1∨D2 or simply D1 or simply D2 where
D1,D2 have the forms s∧φ1 and φ2 respectively, where φ1,φ2∈Φ(↓s∪Σ∪X).
For the example above, we obtain
Δ(s0)=(s0∧[(a∧x.sa))∨b])∨(a∧sℓ),
Δ(sa)=(sa∧x<1)∨(x>1)
Δ(sℓ)=sℓ∧b.
3. 3.
Step 3. We now convert each Δ(s) into a normal form
N(s). N(s) is obtained from Δ(s) as follows.
If s occurs in Δ(s), replace it with Os.
Replace each s′ occurring in each Φi(↓s) with
Os′.
Let N(s)=N1∨N2, where
N1,N2 are normal forms. Intuitively, the states appearing on the right side of each transition
are those which are taken up in the next step. The normal form
explicitely does this, and takes us a step closer to
1−TPTL.
Continuing with the example, we obtain
N(s0)=(Os0∧[(a∧x.Osa))∨b])∨(a∧Osℓ)
N(sa)=(Osa∧x<1)∨(x>1)
N(sℓ)=Osℓ∧b.
4. 4.
Step 4.
Start with the state sn which is
the lowest in the partial order.
Let
N(sn)=(Osn∧φ1)∨φ2,
where φ1,φ2∈Φ(Σ,X).
Solving N(sn), one obtains the solution
Beh(sn) as φ1Wφ2
if sn is an accepting location, and as
φ1Unsφ2 if sn is non-accepting.
Intuitively, Beh(sn) is the behaviour of sn: that is,
it describes the timed words that are accepted when we start in sn.
In the running example, we obtain
Beh(sℓ)=bW⊥=□nsb and
Beh(sa)=(x<1)Unsx>1.
Consider now some N(si)=(Osi∧φ1)∨φ2.
First replace each s′ in φi with Beh(s′).
Beh(si) is then obtained as
Beh(φ1)WBeh(φ2)
if si is an accepting location, and as
Beh(φ1)UnsBeh(φ2) if si is non-accepting.
Substituting Beh(sa) and Beh(sℓ) in N(s0), we obtain
(Os0∧[(a∧x.OBeh(sa))∨b])∨(a∧OBeh(sℓ)), solving which, we get
Beh(s0)=[(a∧x.OBeh(sa))∨b]W(a∧OBeh(sℓ)).
Thus, Beh(s0) which represents all timed words which are accepted when we start at s0 is given by
((a∧(x.O[(x<1)Unsx>1]))∨b)W(a∧O□nsb).
The 1−TPTL formula equivalent to L(A) is
then given by Beh(s0).
H.1 Correctness of Construction
The above algorithm is correct; that is, the 1−TPTL formula
Beh(s0) indeed captures the language accepted by the po-1-clock ATA.
For the proof of correctness, we define a 1-clock ATA with a TPTL look ahead. That is,
δ:S×Σ→Φ(S∪X∪χ(Σ∪{x})), where χ(Σ∪{x}) is a TPTL formula over alphabet
Σ and clock variable x. We allow open TPTL formulae for look ahead; that is,
one which is not of the form x.φ. All the freeze quantifications x. lie within φ.
The extension now allows to take a transition (s,ν)→[κ∧ψ(x)], where ψ(x) is a TPTL formula,
if and only if the suffix of the input word with value of x being ν satisfies ψ(x). We induct on the level of the partial order on the states.
Base Case: Let the level of the partial order be zero.
Consider 1-clock ATA having only one location s0.
Let the transition function be δ(s0,a)=Ba(ψa(x),X,s0) for every a∈Σ.
By our construction, we reduce s0 into Δ(s0)=a∈Σ⋁[Ba(ψa(x),X,O(s0))].
Let Δ(s0)=⋁(Pi∧ψi(x)∧Xi∧Os0)∨⋁(Qj∧ψj(x)∧Xj).
δ(s0,a)=s0∧X1∧ψ1(x) specifies that the clock constraints X1 are satisfied and the suffix satisfies the formula ψ1(x) on reading an a. Thus for this δ(s0,a), we have Os0∧X1∧ψ1(x)∧a as a corresponding disjunct in Δ which specifies the same constraints on the word from the current point onwards. Thus the solution to the above will be satisfied at a point with some x=ν if and only if there is an accepting run from s0 to the final configuration with x=ν.
If the s0 is a final location, the solution to this is φ=⋁(Pi∧ψi(x)∧Xi∧Os0)W⋁(Qj∧ψj(x)∧Xj). If it is non-final, then it would be U instead of W. Note that this implies that whenever s0 is invoked with value of x being ν, the above formula would be true with x=ν thus getting an equivalent 1−TPTL formulae.
Assume that for automata with n−1 levels in the partial order, we can construct an equivalent 1−TPTL formula as per our construction.
Consider an automaton with n levels. Consider all the locations at the lowest level (that is, those location that can only call itself), s0,…,sk.
Apply the same construction. As explained above, the constructed formulae, while eliminating a location will be true at a point if and only if there is an accepting run starting from the corresponding location with the same clock value. Let the formula obtained for any si be φi.
The occurrence of an si in any Δ(si<n) can be substituted with φi as a look ahead. This gives us an n−1 level 1-clock ATA with
TPTL look ahead. By induction, we obtain that every 1-clock po-ATA can be reduced to 1−TPTL formulae.
Appendix I Proof of Lemma 4.4
Proof I.1**.**
Let ρ be a timed word such that ρ,i⊨RatIre. re can be either a simple star-free expression
over Σ, or can be of the form RatI′re′ or RatI1re1+RatI2re2
or RatI1re1.RatI2re2 or (RatI′re′)∗. Recursively, each of re′, re1,re2
also can be expanded out as above. The idea of the proof is to eliminate “all levels” of RatI
starting from the inner most one, by replacing them
with 1−TPTL formulae using structural induction. We first explain the proof in the case of RatIre,
where re is a star-free expression over Σ, and then look at general cases.
We first consider the case when all intervals are bounded.
-
Given RatIre, and a point i in a word ρ,
RatI checks re at all points j in ρ
such that τj−τi∈I.
We first eliminate the interval I from RatIre
by imagining a witness variable
wI that evaluates to true at all points j of ρ such that
τj−τi∈I. wI is used to cover all points
distant I from i.
2. 2.
We eliminate the interval I in RatI
by rewriting RatIre as
Rat((¬wI)∗.re.(¬wI)∗), which,
when asserted at a point i, checks the truth of the expression
(¬wI)∗.re.(¬wI)∗ in the suffix from i.
If wI indeed captures τj−τi∈I, then indeed we are checking re in the interval I.
Let φre be an LTL formula that is equivalent to re. This is possible since L(re) is a star-free language.
3. 3.
We next replace wI by using a freeze clock variable x which checks x∈I
whenever we assert wI.
- (a)
We will look at the simplest case when re is a regular expression over Σ. Let φre be the LTL formula equivalent to re.
- i.
Let re=a for a∈Σ.
We expand the alphabet by allowing proposition x∈I (and its negation x∈/I).
The formula
ψ=((x∈/I)U{φre∧[(x∈I)∧(O(□(x∈/I)))]})
is then an LTL formula that says that there is a single point in the region I, and a holds at that point.
Then ψre=x.ψ is a 1-TPTL* formula that captures RatIa.*
2. ii.
Let re=a.b for b∈Σ. Then we inductively assume
LTL formulae φa and φb that capture a and b.
As above, we allow the proposition x∈I.
Then the formula
ψre=x.{(x∈/I)U[(x∈I∧φa∧O(x∈I∧φb∧O(□(x∈/I))))]}
asserts the existence of two points in the interval I respectively satisfying
in order, a and b. This argument can be extended to work for any finite concatenation
re=a1.a2.….an.
3. iii.
Let re=(re1)∗ be rational expression over Σ. Let φre1
be the LTL formula equivalent to re1. Then the formula
x.[(x∈/I)U((x∈I)∧□[(x∈I)→φre1])]
is a 1-TPTL* formula that asserts the formula φre1 at all points in I.*
4. iv.
Let re=re1+re2 be a rational expression over Σ.
Let φre1 and φre2 be
LTL formulae equivalent to re1,re2. Then
((x∈/I)U{(φre1∨φre2)∧[(x∈I)∧(O(□(x∈/I)))]})
is then an LTL formula that says that there is a single point in the region I, and
one of φre1,φre2 holds
at that point.
2. (b)
Finish the base case of the structural induction, where re was a rational expression over Σ, we now
move on to general cases.
- i.
Let us now consider the case when we have a formula
RatI1[RatI2re].
Then we first obtain as seen above,
x.ζre equivalent to RatI2re. Let x.ζre=w.
Then,
ζout=((x∈/I1)U{w∧(x∈I1)∧O(□(x∈/I1))})
is
an LTL formula which asserts the existence of a single point lying in the interval I1 where w is true.
Then x.ζout is a 1-TPTL* formula over Σ that is equivalent to
RatI1[RatI2re].*
2. ii.
If we have RatI[RatI1re1.RatI2re2], then let
w1=x.ζre1,w2=x.ζre2. Then the formula
x.{(x∈/I)U[(x∈I∧w1∧O(x∈I∧w2∧O(□(x∈/I))))]}
asserts the existence of two points in the interval I respectively satisfying
in order, RatI1re1 and RatI2re2.
3. iii.
If we have RatI[(RatI1re1)∗], then let w1=x.ζre1.
Let w=(x∈/I)U((x∈I)∧□[(x∈I)→w1]).
Then x.w is a 1-TPTL* formula that asserts that at all points in I, the formula RatI1re1
evaluates to true.*
4. iv.
If we have RatI(RatI1re1+RatI2re2), then let
w1=x.ζre1 and w2=x.ζre2. Then
x.{(x∈/I)U((w1∨w2)∧x∈I∧(O(□(x∈/I))))}
is a 1-TPTL* formula that checks that RatI1re1 or RatI2re2 evaluates to true at the single point
in the interval I.*
Note that the boolean combinations like conjunction, disjunction and unary operations like negation can be handled in a straightforward way, once we are done with the above. While encountering boolean combinations, we simply combine the 1-TPTL* formulae obtained
so far.*
In case I is an unbounded interval, then we need not concatenate
O(□(x∈/I))
at the end, since the time stamps of all points in the suffix lie in I.
The rest of the proof is the same. ∎
Appendix J Proof of Lemma 4.5
The Main Idea:
Let A be a po-1-clock ATA with locations S={s0,s1,…,sn}.
Let K be the maximal constant used in the guards x∼c occurring in the transitions.
Let R2i=[i,i],R2i+1=(i,i+1),0≤i<K and RK+=(K,∞) be the regions
R of x. Let Rh≺Rk denote that region Rh
precedes region Rk.
For each location s, Beh(s) as seen above (also Figure 4) gives the timed behaviour starting at s,
using constraints x∼c since the point where x was frozen.
In example 4.2, Beh(sa)=(x<1)Uns(x>1), allows symbols a,b as long as x<1
keeping the control in sa, has no behaviour at x=1, and allows
control to leave sa when x>1.
For any s, we “distribute” Beh(s) across regions by untiming it. In example 4.2,
Beh(sa) is □ns(a∨b) for regions R0,R1, it is ⊥ for R2 and
is (a∨b) for R1+. Given any Beh(s), and a pair of regions Rj⪯Rk, such that
s has a non-empty behaviour in region Rj, and control leaves s in Rk,
the untimed behaviour of s between regions Rj,…,Rk is written as LTL formulae
φj,…,φk. This results in a “behaviour description” (or BD for short)
denoted BD(s,Rj,Rk) : this is a 2K+1 tuple with BD[Rl]=φl
for j≤l≤k, and BD[R]=⊤ denoting “dont care” for the other regions.
Each LTL formula BD(s,Rj,Rk)[Ri] (or BD[Ri] when s,Rj,Rk are clear)
is replaced with a star-free rational expression
denoted re(BD(s,Rj,Rk)[Ri]). Then BD(s,Rj,Rk)
is transformed into a SfrMTL formula φ(s,Rj,Rk)=⋀j≤g≤kRatRgre(BD(s,Rj,Rk)[Rg]).
The language accepted by the po-1-clock ATA A is then given by
⋁0≤j≤k≤2Kφ(s0,Rj,Rk) where s0 is the initial location, and
the word is accepted while in region Rk. This disjunction allows all possible accepting behaviours
from the initial location s0.
Each location s is associated with a set of BDs. Let BDSet(s) denote the of BDs that are associated with
s. If s is the lowest location in the partial order, then BDSet(s)={BD(s,Ri,Rj)∣Ri⪯Rj}.
Computing BD(s,Ri,Rj) for a location s and pair of regions Ri⪯Rj.
The proof proceeds by first computing BD(s,Ri,Rj) for locations s which are lowest in the partial order, followed
by computing BD(s′,Ri,Rj) for locations s′ which are higher in the order.
For any location s, Beh(s) has the form φ1Wφ2
or φ1Unsφ2, or φ, where φ,φ1,φ2
are disjunctions of conjunctions over Φ(S∪Σ∪X), where S is the set of locations
with or without the binding construct x., and X is a set of clock constraints
of the form x∼c. Each conjunct
has the form ψ∧x∈R where ψ∈Φ(Σ∪S) and R∈R.
Let φ1=⋁(Pi∧Ci),φ2=⋁(Qj∧Ej) where Pi,Qj∈Φ(Σ∪S) and Ci,Ej∈R.
Let C and E be a shorthand notation to represent any Ck,El.
For Ri⪯Rj, and a location s, BD(s,Ri,Rj) is empty if Beh(s) has no constraint x∈Ri occurring in C,E, and
if control cannot exit s in Rj.
If Beh(s) has no U,W modalities, then
BD(s,Ri,Ri) is computed when Beh(s)=⋁(Qj∧Ej) and there is some El with
x∈Ri. In this case, BD(s,Ri,Ri)[Ri]=Ql, and the remaining entries are ⊤ representing “dont care”.
If Beh(s) has U,W modalities,
then BD(s,Ri,Rj) is computed when
(1) there is a constraint x∈Ri in C or E (this allows us to start observing the behaviour in region Ri)
(2) there is a constraint x∈Rj in some E (this allows us to exit the control
location s while in region Rj).
If so, the BD Beh(s,Ri,Rj) is a 2K+1 tuple with
(i) formula ⊤ in regions R0,…,Ri−1,Rj+1,…,RK+ (denoting dont care),
(ii)If Ck=El=(x∈Rj) for some Ck,El, then the LTL formula in region Rj is PkUQl if s is not an accepting location,
and is PkWQl if s is an accepting location, (iii)If no Ck is equal to any El for any k,l, and
if El=(x∈Rj) for some l, then the formula in region Rj is Ql. If Cm=(x∈Ri) for some m, then
the formula for region Ri is □nsPm. If there is some Ch=(x∈Rw) for i<w<j, then
the formula in region Rw is □nsPh∨ϵ, where ϵ signifies the fact that
there may be no points in regions Rw. If there are no Cm’s such that Cm=(x∈Rw)
for Ri≺Rw≺Rj, then the formulae in region Rw is ϵ.
We allow ϵ as a special symbol in LTL to signify that there is no behaviour
in a region.
BD(s,Ri,Rj)** for location s lowest in po**. Let s be a location that is lowest in the partial order.
The locations sℓ,sa in Example 4.2 are lowest in the partial order, and
Beh(sℓ)=bW⊥=□nsb, Beh(sa)=[(a∨b)∧(x<1)]Uns[(a∨b)∧(x>1)].
In general, if s is the lowest in the partial order, then
Beh(s) has the form φ1Wφ2
or φ1Unsφ2, or φ, where φ,φ1,φ2
are disjunctions of conjunctions over Φ(Σ∪X). Each conjunct
has the form ψ∧x∈R where ψ∈Φ(Σ) and R∈R.
In example 4.2, the regions are R0=[0,0],R1=(0,1),R2=[1,1],R1+=(1,∞).
Beh(sℓ,R1,R1+)=(⊤,□nsb,□nsb∨ϵ,bW⊥), and
Beh(sa,R0,R1+)=(□ns(a∨b),□ns(a∨b)∨ϵ,ϵ,(a∨b)).
If ϵ in the sole entry in a region, it represents that there is no behaviour in that region.
If ϵ is a disjunct ψ∨ϵ, then it represents a possibility of no behaviour, or a behaviour ψ.
Using the BDs of sa, we can write the SfrMTL formula that describes the behaviour of sa.
This fomula is given by ψ(sa)=φR0(sa)∧φR1(sa)∧φR2(sa)∧φR1+(sa), where
each φRi
describes the behaviour starting from region Ri, while in location sa.
For a fixed region Ri, φRi(sa) is
⋀Rg≺RiRatRgϵ∧RatRiΣ+→{⋁Ri≺Rjφ(sa,Ri,Rj)}, where
φ(sa,Ri,Rj) is described above. RatRgϵ represents that there is no behaviour
in Rg. Recall that φ(sa,Ri,Rj) describes a possible behaviour of sa that starts at Ri and ends in Rj.
For instance,
φR0(sa) is
RatR0Σ+→{(RatR0(a+b)∗∧RatR1[(a+b)∗+ϵ]∧RatR2ϵ∧RatR1+(a+b)∗)}
while
φR1(sa) is
RatR0ϵ∧RatR1Σ+→{(RatR1(a+b)∗∧RatR2ϵ∧RatR1+(a+b)∗)}.
Similarly, φR2(sa) is empty since sa has no behaviour in R2.
Finally, φR1+(sa) is
⋀Rg≺R1+RatRgϵ∧RatR1+Σ+→RatR1+(a+b)∗. In a similar manner, we can write the SfrMTL formula ψsℓ that describes the behaviour
of sℓ across regions.
BD(s,Ri,Rj)** for a location s which is higher up**.
If s is not the lowest in the partial order, then Beh(s)
has locations s′∈↓s. s′ occurs as O(s′) or x.O(s′) in
Beh(s). We now elaborate the operations needed to combine BDs.
Boolean Combinations of BDs.
Let s1,s2 be two locations of the po-1-clock ATA A.
Assume Beh(s1)=φ1Unsφ2 or
φ1Wφ2 and
Beh(s2)=ψ1Unsψ2 or
ψ1Wψ2.
We have already seen how to handle x.OBeh(s1)
or x.OBeh(s2). So let us assume s1,s2 appear in Beh(s) as
OBeh(s1) and OBeh(s2).
Consider BDSet(s1) and BDSet(s2), and consider any pair
of BDs, say BD(s1,Ri,Rj) and BD(s2,Ri,Rj)
from these respectively. The boolean operations are defined
for each pair taken from BDSet(s1) and BDSet(s2).
Take BD(s1,Ri,Rj) and BD(s2,Ri,Rk) respectively from
BDSet(s1) and BDSet(s2).
We now define boolean operations ∧ and ∨ on these BDs.
The BDSet for s1∧s2:
Consider BD1=BD(s1,Ri,Rj) and BD2=BD(s2,Ri,Rk), both which describe behaviours of s1,s2 starting in region Ri.
Assume Rj≺Rk (the case of Rk≺Rj is similar). To obtain a
BD conjuncting these two, starting in region Ri, we do the following.
Construct BD′ by conjuncting
the entries of BD1,BD2 component wise.
This will ensure that we take the possible behaviour of Beh(s1) at region Ri and conjunct it with the possible behaviour of Beh(s2) in the same region. BD′∈BDSet(s1∧s2).
In a similar way, we can also compute the BDSet(s1∨s2).
Elimination of OBeh(s′) from BD(s,Ri,Rj)
Given any Beh(s) of the form [⋁i(Pi∧Ci)]Uns[⋁j(Qj∧Ej)] or [⋁i(Pi∧Ci)]W[⋁j(Qj∧Ej)]
with Pi,Qj∈Φ(Σ∪S), and Ci,Ej are clock constraints of the form x∈R.
Assume that we have calculated BD(s′,R,R′) for all s′∈↓s and all regions R,R′.
There might be some propositions of the form OBeh(s′) as a conjunct in some entries of
BD(s,Ri,Rj). This occurrence of OBeh(s′) is eliminated by “stitching”
the behaviour of s′ with BD(s,Ri,Rj) as follows:
We consider three cases here, depending on how OBeh(s′) occurs in BD1=BD(s,Ri,Rj).
As a first case, let BD1=(X0,…,Xg−1,Qj∧O(Beh(s′)),Xg+1,…,X2K).
-
To eliminate
OBeh(s′) from BD1, we first recall that s′∈↓s and that BD(s′,Rk,Rl) has been computed
for all regions Rk,Rl. Beh(s) will not occur in any of these BDs corresponding to s′.
2. 2.
The first thing to check is which region (Rg or later) where the next point can be enabled, based on the behaviour
of s′. There are 2K−g+1 possibilities, depending on which region ≥g the next point lies with respect to Qj∧O(Beh(s′)).
Suppose the next point can be taken in Rg itself. This means that from the next point, all the possible behaviours described by
any of the BD’s BD(s′,Rg,Rh) will
apply along with BD1.
We define a binary operation combine which combines two BDs, BD1=BD(s,Ri,Rj) and
BD2=BD(s′,Rg,Rh), producing a new BD, BD3=combine(BD1,BD2).
To combine the behaviours from the point where Beh(s′) is encountered, we substitute
OBeh(s′) with the LTL formula asserted at region Rg in BD2. If BD2[Rg] represents
the gth component, then we replace OBeh(s′) in BD1[Rg] with BD2[Rg].
Thus, BD3[Rg]=Qj∧BD2[Rg].
For all Rw≺Rg, BD3[Rw]=BD1[Rw].
For all Rw such that Rg≺Rw, BD3[Rw]=BD1[Rw]∧BD2[Rw].
Now consider the case when the next point is taken a region >Rg.
The next point can occur in region Rg+1 or higher. Let
b∈{g+1,…,2K}, and assume that the next point where Beh(s′) has a behaviour is in Rb.
Then given BD1=BD(s,Ri,Rj) and BD2=BD(s′,Rg,Rh) such that
BD2[g+1],…,BD2[b−1]=ϵ, we obtain BD3 as follows.
For all Rw≺Rg, BD3[Rw]=BD1[Rw]. For w=g, BD3[Rg]=Qj∧□⊥. The conjunction
with □⊥ signifies that the next point in Rg is not available for s′, since s′ has no behaviour
in Rg. For all b>w>g, BD3[Rw]=BD1[Rw]∧ϵ=ϵ.
This implies the next point from where the assertion Qj∧O(Beh(s′)) was made is in a region ≥Rb.
For all w≥b, BD3[Rw]=BD1[Rw]∧BD2[Rw].
This combines the assertions of both the behaviours from the next point onwards.
As a second case, consider BD1=[X0,…,Xg−1,□ns(Pj∧O(Beh(s′))),Xg+1,…,X2K]. Elimination
of OBeh(s′) in this case is similar to case 1.
As the third case, let BD1=[X0,…,Xg−1,Pi∧O(Beh(s1))UnsQj∧O(Beh(s2)),Xg+1,…,X2K], and we have to eliminate both OBeh(s1) and OBeh(s2).
Either Qj∧O(Beh(s2)) is true at the present point or,
Pi∧O(Beh(s1)) is true until some point in the future within the region Rg, at which point, Qj∧O(Beh(s2))
becomes true. Thus, BD1 can be replaced with two BDs
BD1′=[X0,…,Xg−1,Qj∧O(Beh(s2)),Xg+1,…,X2K], and
BD1′′=[X0,…,Xg−1, Pi∧O(Beh(s1))UQj∧O(Beh(s2)),Xg+1,…,X2K].
Elimination of OBeh(s2) is done from BD1′ as seen in case 1.
Consider BD1′′ which guarantees that the next point from which the assertion
Pi∧O(Beh(s1))UQj∧O(Beh(s2)) is made is within region Rg,
and that O(Beh(s1)) is called for the last time within Rg.
BD1′′ has to be combined with any BD(s1,Rg,Rh),
which has a starting behaviour of s1 from region Rg.
s2 can have an enabled transition from any point either within region Rg or a succeeding region.
Consider the case where s2 has an enabled transition from within the region Rg.
In this case, we have to combine BD1′′ with
some BD3=BD(s1,Rg,Rh) and
with some BD4=BD(s2,Rg,Rj).
Let BD3=(Y0,…,Y2K) and let BD4=(Z0,…,Z2K).
We now show to combine BD1′′,BD3 and BD4
obtaining a BD (A0,…,A2K).
For every w<g, Aw=Xw.
For w=g, Ag is obtaining by replacing OBeh(s1) with Yg and OBeh(s2) with Zg
For all w>g, Aw=Xw∧Yw∧Zw.
Now consider the case where s2 has an enabled transition from a region Rb such that Rg≺Rb.
In this case, Aw=Xw for w<g. The main difference with the earlier case is that we have to assert that from the last point in Rg, the next point only occurs in the region Rb. Thus all the regions between Rg and Rb should be ϵ
in (A0,…,A2K). That is, Aw=ϵ for g<w<b.
For w=g, Ag=(Pi∧Yg)U(Qj∧□⊥), where Pi,Qj are obtained from BD1′′[Rg].
Here again, conjuncting □⊥ with Qj signifies that the next point
is not enabled for s2. Finally, for w≥b, Aw=Xw∧Yw∧Zw.
Note that elimination of OBeh(s′) from any BD in the set BDSet(s)
results in stitching some BD from BDSet(s′) to certain elements
of BDSet(s). At the end of the stitching, we obtain BDSet(s) such that
in each BD of BDSet(s), OBeh(s′) has been replaced.
Obtaining SfrMTL Formulae
Finally, we show that given a BD for Beh(s), we can construct an SfrMTL formula, ψs, equivalent to x.O(s).
That is, ρ,i⊨ψs if and only if ρ,i,ν⊨x.O(Beh(s)), for any ν.
Recall that Beh(s) is a 1-TPTL formula, as computed in lemma 4.3.
We give a constructive proof as follows:
Assume ρ,i,ν⊨x.O(Beh(s)). Note that according to the syntax of TPTL, every constraint x∈I checks the time elapse between the last point where x was frozen. Thus satisfaction of formulae of the form x.ϕ at a point is independent of the clock valuation.
ρ,i,ν⊨x.O(Beh(s)) iff ρ,i,ν[x←τi]⊨OBeh(s).
We have precomputed BD(s,Ri,Rj) for all regions Ri⪯Rj; and
BD(s,Ri,Rj) is guided by the 1-TPTL formula Beh(s). The entry in region Ri
of BD(s,Ri,Rj) depends on the behaviour allowed in region Ri from location s;
likewise, the entry in each region Rg of BD(s,Ri,Rj) is
obtained by looking up Beh(s). In case Beh(s) does not admit any behaviour in a region Rg, then
the gth entry in BD(s,RiRj) is ϵ.
Thus, ρ,i,ν⊨x.O(Beh(s)) iff for all w∈0,…,2K, such that
Beh(s) has an allowed behaviour in region Rw,
ρ,i+1,τi⊨(x∈Rw).
In addition, we also know that there is some BD(s,Rw,Rj) such that
BD[Rk] is the LTL formula that describes the behaviour in region Rk of location s.
Note that, ρ,i+1,τi⊨(x∈Rw) is true, iff, ρ,i⊨g∈{1,…,w−1}⋀[RatRgϵ]∧RatRwΣ+. This is true iff
ρ,i⊨BD=BD(s,Rw,Rj)⋁k∈{1,…,2K}⋀RatRk(re(BD[Rk])), where re(BD[Rk]) is a star-free rational expression equivalent to the LTL formula BD[Rk].
Thus, ρ,i,ν⊨x.O(Beh(s)), iff, ρ,i⊨(ψ1→ψ2) where
ψ1=w∈{0,…,2K}∖E⋀g∈{1,…,w−1}⋀RatRgϵ∧RatRwΣ+ and
ψ2=BD=BD(s,Rw,Rj)⋁k∈{1,…,2K}⋀RatRk(re(BD[Rk])).
where E is the set of regions where Beh(s) has no behaviour.
The SfrMTL formula ψs0 is one which begins in the initial location s0, stitches
the behaviours of locations sj that appear in a run from s0 such that L(ψs0)
is non-empty iff the language accepted by the po-1-clock ATA A is non-empty, and
L(ψs0)=L(A).
Consider the po-1-clock ATA A=({a,b},{s0,sa,sℓ},s0,{s0,sℓ},δ) with transitions
δ(s0,b)=s0,δ(s0,a)=(s0∧x.sa)∨sℓ,
δ(sa,a)=(sa∧x<1)∨(x>1)=δ(sa,b), and
δ(sℓ,b)=sℓ,δ(sℓ,a)=⊥.
Consider the subset of L(A) consisting of timed words whose first
symbol occurs at a time >1. We write a SfrMTL formula that captures this subclass.
Let us consider the formula we obtain if we consider allowed behaviours from
s0 that begin in the region R1+; this is the subset of BDSet(s0) consisting of
BD(s0,R1+,R1+)=(⊤,⊤,⊤,[(a∧x.OBeh(sa))∨b]W(a∧OBeh(sℓ))). We look at the SfrMTL formula ψsa corresponding to
x.OBeh(sa), which is given by
RatR0Σ+→{RatR0(a+b)∗∧RatR1((a+b)∗+ϵ)∧RatR2ϵ∧RatR1+(a+b)∗}
∧
RatR0ϵ∧RatR1Σ+→{RatR0⊤∧RatR1(a+b)∗∧RatR2∅∧RatR1+(a+b)∗}
∧
RatR0ϵ∧RatR1ϵ∧RatR2ϵ∧RatR1+Σ+→RatR1+(a+b)∗
This formula ψa is plugged in place of x.OBeh(sa) in BD(s0,R1+,R1+). We now combine
BD(sℓ,R1+,R1+)∈BDSet(sℓ) with BD(s0,R1+,R1+)[R1+] to obtain the combined behaviour
of locations sℓ from the next point along with that of s0.
We know that BD(sℓ,R1+,R1+)=(⊤,⊤,⊤,bW⊥). Thus, we obtain
BD(s0,R1+,R1+) after combining with BD(sℓ,R1+,R1+) and
ψsa as (⊤,⊤,⊤,[(a∧ψsa)∨b]W(a∧(bW⊥))).
Translating this into an SfrMTL formula, we obtain the formula φR1+(s0)
RatR0ϵ∧RatR1ϵ∧RatR2ϵ∧RatR1+Σ+→RatR1+re([(a∧ψsa)∨b]W(a∧(bW⊥))).
φR1+(s0) is the formula which captures the subset of L(A) which consists of timed words
of the form (a1,t1)(a2,t2)…(an,tn) such that t1>1. We can also write the formulae
φR0(s0), φR1(s0), φR2(s0), which capture respectively, the subset of words
of L(A) which consists of timed words
of the form (a1,t1)(a2,t2)…(an,tn) where t1=0, 0<t1<1 and t1=1 respectively.
Thus, L(A) is the union of the languages
L(φR1+(s0)),L(φR0(s0)),L(φR2(s0)) and
L(φR1(s0)).