Theory Comput Syst (2011) 48: 648–679 DOI 10.1007/s00224-010-9253-z

Model Checking Weighted Integer Reset Timed Automata Lakshmi Manasa · Shankara Narayanan Krishna · Chinmay Jain

Published online: 2 March 2010 © Springer Science+Business Media, LLC 2010

Abstract Weighted timed automata (WTA), introduced in Alur et al. (Proceedings of HSCC’01, LNCS, vol. 2034, pp. 49–62, Springer, Berlin, 2001), Behrmann et al. (Proceedings of HSCC’01, LNCS, vol. 2034, pp. 147–161, Springer, Berlin, 2001) are an extension of Alur and Dill (Theor. Comput. Sci. 126(2):183–235, 1994) timed automata, a widely accepted formalism for the modelling and verification of real time systems. Weighted timed automata extend timed automata by allowing costs on the locations and edges. There has been a lot of interest Bouyer et al. (Inf. Process. Lett. 98(5):188–194, 2006), Bouyer et al. (Log. Methods Comput. Sci. 4(2):9, 2008), Brihaye et al. (Proceedings of FORMATS/FTRTFT’04, LNCS, vol. 3253, pp. 277–292, Springer, Berlin, 2004), Brihaye et al. (Inf. Comput. 204(3):408–433, 2006) in studying the model checking problem of weighted timed automata. The properties of interest are written using logic weighted CTL (WCTL), an extension of CTL with costs. It has been shown Bouyer et al. (Log. Methods Comput. Sci. 4(2):9, 2008) that the problem of model checking WTAs with a single clock using WCTL with no external cost variables is decidable, while 3 clocks render the problem undecidable Bouyer et al. (Inf. Process. Lett. 98(5):188–194, 2006). The question of 2 clocks is open. In this paper, we introduce a subclass of weighted timed automata called weighted integer reset timed automata (WIRTA) and study the model checking problem. We give a clock reduction technique for WIRTA. Given a WIRTA A with n ≥ 1 clocks, we show that a single clock WIRTA A preserving the paths and costs of A can be obtained. This gives us the decidability of model checking WIRTA with n ≥ 1 clocks and m ≥ 1 costs using WCTL with no external cost variables. We then show that L. Manasa () · S.N. Krishna · C. Jain Department of Computer Science & Engineering, IIT Bombay, Powai, Mumbai 76, India e-mail: [email protected] S.N. Krishna e-mail: [email protected] C. Jain e-mail: [email protected]

Theory Comput Syst (2011) 48: 648–679

649

for a restricted version of WCTL with external cost variables, the model checking problem is undecidable for WIRTA with 3 stopwatch costs and 1 clock. Finally, we show that model checking WTA with 2 clocks and 1 stopwatch cost against WCTL with no external cost variables is undecidable, thereby answering a question that has remained long open. Keywords Weighted timed automata · Weighted CTL · Model checking · Integer resets · Clock reduction

1 Introduction Timed automata [1] are a well-established model for real-time systems. One of the most important properties of timed automata is that reachability is decidable. This has paved the way for using timed automata in verification and many tools viz., UPPAAL [8], KRONOS [19] and HyTech [3] were built using this. Since their inception, several variants of timed automata have been considered: [12], wherein new operations on clock updates were considered, [10] where new kinds of guards were introduced, [20] where a set of clocks could be freezed, [11], where silent transitions were studied, and [23], where new kinds of updates along with additive and diagonal constraints were studied. However, timed automata are not closed under complementation, and their inclusion problem is not decidable [1]. Hence, the quest for finding a more attractive class of timed automata has been going on. Some of the interesting classes considered in the literature are: (i) [4] event clock automata, (ii) [21] open and closed automata, (iii) [6] perturbed timed automata, (iv) [18] timed automata with periodic constraints, (v) [26] one clock timed automata, (vi) timed automata with integer resets introduced in [25] and subsequently investigated in [27, 29] and [22]. To conclude the list of classes, [7] gives some conditions under which timed automata are determinizable. An extension of timed automata useful in applications like scheduling problems and controller synthesis is weighted timed automata (WTA) introduced in [5, 9]. In this, cost variables are attached to locations and edges. The costs are used only as observers, they cannot be compared or evaluated in the automata. The behaviour of the automata is not influenced by these costs. This has led to several decidability results for optimization problems like minimum cost reachability, cost optimal schedules and so on. A generalization of these questions is the model checking problem of WTAs using cost extended versions of linear as well as branching time logics. The logics WCTL and WMTL are considered as cost extensions of logics CTL and LTL (like TCTL, MTL which are timed extensions of CTL, LTL) and are interpreted over WTAs. While it is known [2] that TCTL model checking of timed automata is decidable, it has already been shown that WCTL model checking of WTAs is not decidable [14, 17]. Reference [17] shows that with 3 stopwatch costs and 1 clock, model checking WCTL with external cost variables is undecidable, while in the case of 2 clocks and 1 stopwatch cost or 2 stopwatch costs and 1 clock, it is possible to obtain an infinite bisimulation. Reference [14] has shown that if there are 3 clocks and 1 stopwatch cost, model checking WCTL with no external cost variables is undecidable. The case

650

Theory Comput Syst (2011) 48: 648–679

of model checking WTAs with 2 clocks and 1 stopwatch cost has remained an open problem. In this paper, we continue the study of this problem by first looking at the model checking question on a sub class of WTAs called weighted integer reset timed automata (WIRTA). These are extensions of IRTAs [25]. It has been shown [25, 27] (albeit with different complexities, non-primitive recursive [25] versus doubly exponential [27]) that if A is a timed automaton and if B is an IRTA, then the question L(A) ⊆ L(B)? is decidable. We show that it is possible to reduce the number of clocks in a given WIRTA to one. This, along with the decidability result [15] of model checking WCTL with no external cost variables on one clock WTAs gives us the result that model checking WCTL with no external cost variables is decidable for WIRTAs with n clocks and m costs, n, m ≥ 1. We then investigate model checking WCTL with external cost variables on WIRTAs. Here, we obtain an undecidability result with 3 stopwatch costs and 1 clock, on a restricted version of the logic (called WCTLr in [17]). Finally, we give a solution to the open question of model checking WTAs with 2 clocks and 1 stopwatch costs by showing undecidability in the case of WCTL with no external cost variables. The paper is organized as follows: Sect. 2 gives the prerequisites, introduces WTAs and gives the syntax, semantics as well as expressiveness of logic WCTL, Sect. 3 introduces WIRTA, Sect. 4 gives the clock reduction results, Sect. 5 talks about the undecidability results, and we conclude in Sect. 6.

2 Prerequisites For any set S, S ∗ denotes the set of all strings over S. We consider as time domain T the set Q+ or R+ of non-negative rationals or reals, and  a set of actions. A time sequence over T is a non-decreasing sequence τ = (ti )i≥1 ; for simplicity t0 is taken to be zero always. Let X be a set of clocks. A clock valuation over X is a mapping X X ν : X → R+ . We denote by RX + (or T ) the set of clock valuations over X. If ν ∈ T and τ ∈ T, then ν + τ is the clock valuation defined by (ν + τ )(x) = ν(x) + τ , for x ∈ X. A guard or constraint over X is a conjunction of expressions of the form x ∼ c where x ∈ X, c ∈ N and ∼∈ {<, ≤, >, ≥, =}. We denote by G(X) the set of guards over X. The satisfaction relation for guards over clock valuations is denoted as ν |= ϕ whenever valuation ν satisfies guard ϕ in the usual way. Clock constraints allow us to test the values of clocks. To change the value of a clock x we use clock resets. U0 (X) denotes the set of clock resets. A clock reset φ ∈ U0 (X) is defined by simply specifying the subset of clocks that get reset. Let ν be a valuation and φ be a clock reset. We use the notation ν  = ν[φ := 0] to denote ν  (z) = ν(z) for all z ∈ X\φ and ν  (y) = 0 for all y ∈ φ. 2.1 Timed Automata A timed automaton [1] is a tuple A = (L, L0 , , X, E, F ) where L is a set of locations; L0 ⊆ L is a set of initial locations;  is a set of symbols; X is a set of clocks; E ⊆ L × L ×  × G(X) × U0 (X) is the set of transitions and F ⊆ L is a set of final locations. G(X) and U0 (X) are the set of clock constraints and clock resets as

Theory Comput Syst (2011) 48: 648–679

651

described above. An edge e = (l, l  , a, ϕ, φ) represents a transition from l to l  on symbol a, with the valuation ν ∈ TX satisfying the guard ϕ, and then φ gives the resets of certain clocks. A path is a finite (infinite) sequence of consecutive transitions. The path is said to be accepting if it starts in an initial location (l0 ∈ L0 ) and ends in a final location. A run through a path from a valuation ν0 (with ν0 (x) = 0 for all x) is a se(σ1 ,ϕ1 ,φ1 )

t1

t2

(σ2 ,ϕ2 ,φ2 )

quence (l0 , ν0 ) −→ (l0 , ν1 ) −→ (l1 , ν1 ) −→ (l1 , ν2 ) −→ (l2 , ν2 ) · · · (ln , νn ). The timed word corresponding to the run is σ = (σ1 , t1 )(σ2 , t2 )(σ3 , t3 ) · · · (σn , tn ).  Note that νi = νi−1 + (ti − ti−1 ), νi |= ϕi , and that νi = νi [φi := 0], i ≥ 1. A timed word σ is accepted by A iff there exists an accepting run (through an accepting path) over A, the word corresponding to which is σ . The timed language L(A) accepted by A is defined as the set of all timed words accepted by A. 2.2 Region Automata Given a set X of clocks, let R be a partitioning of TX . Each partition contains a set (possibly infinite) of clock valuations. Given α ∈ R, the successors of α represented by Succ(α) are defined as α  ∈ Succ(α)

if ∃ν ∈ α, ∃t ∈ T such that ν + t ∈ α  .

The partition R is said to be a set of regions iff α  ∈ Succ(α)

⇐⇒

∀ν ∈ α, ∃t ∈ T such that ν + t ∈ α  .

A set of regions is consistent with time elapse if two valuations which are equivalent (within the same partition) stay equivalent with time elapse. A region α ∈ R is said to satisfy a clock constraint ϕ ∈ G(X) denoted as α |= ϕ, if ∀ ν ∈ α, ν |= ϕ. A clock reset φ ∈ U0 (X) maps a region α to a region α[φ := 0] = α  such that α  ∩ {ν[φ := 0]} = ∅ for ν ∈ α. A set of regions R is said to be compatible with a set of clock constraints G(X) iff ∀ϕ ∈ G(X) and ∀α ∈ R exactly one of the following holds (a) α |= ϕ or (b) α |= ¬ϕ. A set of regions R is said to be compatible with a set of clock resets U0 (X) iff α  = α[φ := 0] ⇒ ∀ν ∈ α, ∃ν  ∈ α  such that ν  = ν[φ := 0]. Given a timed automaton A, and a set of regions R compatible with G(X) and U0 (X), the region automaton R(A) = (Q, Q0 , , E  , F  ) is defined as follows: Q = L × R the set of locations; Q0 = L0 × α0 (α0 is the region where ν(x) = 0 for all x ∈ X), the set of initial locations; F  = F × R ⊆ Q the set of final locations; a E  ⊆ (Q ×  × Q) is the set of edges. (l, α) → (l  , α  ) if ∃α  ∈ R and a transition   (l, l , a, ϕ, φ) ∈ E such that (a) α ∈ Succ(α), (b) α  |= ϕ and (c) α  = α  [φ := 0]. Let σ = (σ1 , t1 )(σ2 , t2 )(σ3 , t3 ) · · · (σn , tn ) be a timed word. Define Untime(σ ) = σ1 σ2 · · · σn . Untime(L(A)) = {Untime(σ ) | σ ∈ L(A)}. The region automaton is an abstraction of the timed automaton accepting Untime(L(A)) [1]. Theorem 1 Let A be a timed automaton. Then the problem of checking emptiness of L(A) is decidable [1].

652

Theory Comput Syst (2011) 48: 648–679

2.3 Weighted Timed Automata Let AP be a set of atomic propositions. We recall the definition of WTAs [16]. A weighted timed automaton is a tuple A = (L, L0 , X, Z, E, θ, η, C) where L is a set of locations, L0 ⊆ L is a set of initial locations, X is a set of clocks, Z is a finite set of costs (let |Z| = m), E ⊆ L × G(X) × U0 (X) × L is the set of transitions. A transition e = (l, ϕ, φ, l  ) ∈ E is a transition from l to l  with valuation ν ∈ TX satisfying the guard ϕ, and φ gives the set of clocks to be reset. θ : L → 2AP is the labelling function which associates with each location a subset of AP . η : L → G(X) defines the invariants of each location. C : L ∪ E → Nm is the cost function which gives the rate of growth of each cost. Note that the costs are called stopwatches if C : L ∪ E → {0, 1}m . From the nature of the costs and stopwatches, it is clear that stopwatches are restricted costs. Hence, WTA with stopwatches form a subclass of WTA with costs. The semantics of a WTA A = (L, L0 , X, Z, E, θ, η, C) is given by a labelled timed transition system TA = (S, →) where S = L×TX ×TZ . We refer to an element l ∈ L of a WTA A as a location while we refer to an element (l, ν, μ) ∈ S of TA as a state. The terms transition and edge are used interchangeably. → is composed of transitions – Time elapse t in l: A state (l, ν, μ) after time elapse t evolves to (l  , ν  , μ ), where l  = l, ν  = ν + t, μ = μ + C(l) ∗ t and for all 0 ≤ t  ≤ t, ν + t  |= η(l). (ϕ,φ)

– Location switch: (l, ν, μ) −→ (l  , ν  , μ ) if there exists e = (l, ϕ, φ, l  ) ∈ E, such that ν |= ϕ, ν  = ν[φ := 0] and μ = μ + C(e). Here, ν |= η(l), ν  |= η(l  ). A path is a sequence of consecutive transitions in the transition system TA . t1

(ϕ1 ,φ1 )

A path ρ starting at (l0 , ν0 , μ0 ) is denoted as ρ = (l0 , ν0 , μ0 ) −→ (l0 , ν1 , μ1 ) −→ t2

(ϕ2 ,φ2 )

 (l1 , ν1 , μ1 ) −→ (l1 , ν2 , μ2 ) −→ (l2 , ν2 , μ2 ) · · · (ln , νn , μn ). Note that νi = νi−1 +   (ti − ti−1 ), νi |= ϕi , νi = νi [φ := 0] and μi = μi−1 + C(li−1 ) ∗ (ti − ti−1 ), μi = μi + C(li−1 , ϕi , φi , li ). The ith state of the path is denoted as ρ[i].

2.4 Weighted Computational Tree Logic (WCTL) The logic weighted CTL (WCTL) extends CTL with constraints over costs. Let Z be a set of costs. We now give the syntax of WCTL with external cost variables as in [17]. Let AP be the set of atomic propositions. ψ ::= true | σ |π | z.ψ | ¬ψ | ψ ∨ ψ | E(ψUψ) | A(ψUψ) where z ∈ Z, σ ∈ AP , and π is a cost constraint of the form zi ∼ c or zi − zj ∼ c for costs zi , zj ∈ Z and c ∈ N. If the cost constraints π are restricted to be only of the form zi ∼ c, then the logic is denoted by WCTLr . The freeze quantifiers z. allows us to reset costs, while the cost constraints z ∼ c allows us to test them. The formulae are evaluated on a WTA. The sets AP , Z are the same for the formula as well as for the WTA. Given a WTA A, its transition system TA and a WCTL formula ψ , the satisfaction relation A,(l, ν, μ) |= ψ is defined as follows:

Theory Comput Syst (2011) 48: 648–679

653

A,(l, ν, μ) |= σ iff σ ∈ θ (l) A,(l, ν, μ) |= π iff μ |= π A,(l, ν, μ) |= ¬ψ iff A,(l, ν, μ) |= ψ A,(l, ν, μ) |= ψ1 ∨ ψ2 iff A,(l, ν, μ) |= ψ1 or A,(l, ν, μ) |= ψ2 . A,(l, ν, μ) |= z.ψ iff A,(l, ν, μ[z := 0]) |= ψ where μ[z := 0] stands for μ with z reset to zero. – A,(l, ν, μ) |= Eψ1 Uψ2 iff there exists a run ρ in the transition system TA starting at (l, ν, μ), such that there exists a position i in ρ for which ρ[i] = (li , νi , μi ) |= ψ2 and for all j < i, ρ[j ] |= ψ1 . – A, (l, ν, μ) |= Aψ1 Uψ2 iff for any run ρ in the transition system TA starting at (l, ν, μ), there exists a position i in ρ such that ρ[i] = (li , νi , μi ) |= ψ2 and for all j < i, ρ[j ] |= ψ1 .

– – – – –

Next, we define logic WCTL with no external cost variables [15]. ψ ::= true | σ | ¬ψ | ψ1 ∨ ψ2 | Eψ1 Uz∼c ψ2 | Aψ1 Uz∼c ψ2 with z ∈ Z, c ∈ N, σ ∈ AP . Given a WTA A, its transition system TA , the semantics of Eψ1 Uz∼c ψ2 and Aψ1 Uz∼c ψ2 are given below. The semantics of the other formulae are the same as described above. – A,(l, ν, μ) |= Eψ1 Uz∼c ψ2 iff there exists a run ρ in the transition system TA starting at (l, ν, μ), such that for a position i in ρ, ρ[i] = (li , νi , μi ) |= ψ2 and for all j < i, ρ[j ] |= ψ1 , with μi (z) − μ(z) ∼ c. – A,(l, ν, μ) |= Aψ1 Uz∼c ψ2 iff for any run ρ in the transition system TA starting at (l, ν, μ), there exists a position i in ρ, such that ρ[i] = (li , νi , μi ) |= ψ2 and for all j < i, ρ[j ] |= ψ1 , with μi (z) − μ(z) ∼ c. As usual, we use the abbreviations EFφ ≡ E(trueUφ), AFφ ≡ A(trueUφ) EGφ ≡ ¬AF¬φ and AGφ ≡ ¬EF¬φ. Let us denote logic WCTL with no external variables [15] by WCTL1 , and WCTL with external cost variables [17] by WCTL2 . The restriction of WCTL2 where cost constraints zi − zj ∼ c are not allowed is denoted by WCTL2r (this was called WCTLr in [17]). We now compare the expressive power of the logics WCTL1 , WCTL2r . Lemma 1 WCTL2r is more expressive than WCTL1 . Proof We only give a proof sketch. Consider the WCTL2r formula ψ = z.EF([a ∧z ≤ 1] ∧ EG[z ≤ 1 ⇒ ¬b]), where a, b ∈ AP . It can proved that there is no WCTL1 formula equivalent to ψ using an argument similar to the one used for showing that TPTL is more expressive than MTL [13]. 

3 Weighted Integer Reset Timed Automata (WIRTA) In this section, we introduce a subclass of WTA called weighted integer reset timed automata along the lines of IRTA introduced in [25]. In this subclass of automata, the reset of clocks are restricted to happen only at integer time points. An integer reset

654

Theory Comput Syst (2011) 48: 648–679

Fig. 1 An IRTA A

timed automaton (IRTA) is a timed automaton in which every edge e = (l, l  , a, ϕ, φ) is such that φ is nonempty only if ϕ contains at least one atomic constraint of the form x = c c ∈ N, for some clock x. Definition 1 A Weighted Integer Reset Timed Automaton (WIRTA) is a WTA A = (L, L0 , X, Z, E, θ, η, C) with the restriction that for all e = (l, ϕ, φ, l  ) ∈ E if φ = ∅ then ϕ consists of at least one atomic clock constraint x = c for some x ∈ X, c ∈ N. The restriction on the resets ensure that the fractional parts of all clocks remain the same at all points of time. For a clock valuation ν(x), let frac(ν(x)) denote the fractional part of ν(x) and int(ν(x)) denote the integral part. For example, if ν(x) = 7.02, then int(ν(x)) = 7 and frac(ν(x)) = 0.02. Example 1 The automaton A in Fig. 1 is an IRTA. Lemma 2 Let A = (L, L0 , , X, E, F ) be an IRTA and ν be a clock valuation in any given run in A. Then ∀x, y ∈ X, frac(ν(x)) = frac(ν(y)) [27]. 3.1 IRTA Regions In this section, we look at the regions R of an IRTA. Given a set X of clocks, let R be a finite partitioning of TX . The notions successor of a region, compatibility with guards and compatibility with resets are the same as mentioned in Sect. 2.2. Let cm ∈ N be the maximum constant occurring in the guards G(X) of the IRTA A. For every clock x ∈ X, define a set of intervals I, as I = {[c]|0 ≤ c ≤ cm } ∪ {(c, c + 1)|0 ≤ c < cm } ∪ {(cm , ∞)}. Let α be a tuple ((Ix )x∈X , ≺) where 1. Ix ∈ I and 2. ≺ is a total preorder on X0 = {x ∈ X | Ix is of the form (c, c + 1)}. The region associated with α is the set of valuations ν ∈ TX such that for all x ∈ X, ν(x) ∈ Ix and for all x, y ∈ X0 , x ≺ y iff frac(ν(x)) ≤ frac(ν(y)). By Lemma 2, for all x, y ∈ X, x ≺ y and y ≺ x. Thus we can safely consider α to be ((Ix )x∈X ). The set of all such tuples α partitions TX and this is the set we consider to be R. Definition 2 (Integral, Non-integral, Saturated region) Let α = ((Ix )x∈X ) ∈ R and let Xm ⊆ X be such that ∀x ∈ Xm , Ix = (cm , ∞). – α is said to be saturated if Xm = X – α is said to be integral if ∀x ∈ X \ Xm , with Xm ⊂ X, Ix is of the form [c], c ≤ cm

Theory Comput Syst (2011) 48: 648–679

655

– α is said to be non-integral if ∀x ∈ X \ Xm , with Xm ⊂ X, Ix is of the form (c, c + 1), c < cm . Definition 3 (Immediate Successor) For every clock region α ∈ R, its immediate successor α i is defined as ∀ν ∈ α, ∀t ∈ T if ν + t ∈ α then ∃t  ≤ t such that ν + t  ∈ α i . Lemma 3 Every clock region α ∈ R has a unique immediate successor α i ∈ R. Note that the immediate successor of a non-integral clock region is an integral clock region and that of an integral region is either a non-integral region or a saturated region. The following lemma proves that R is indeed a set of regions and that it is compatible with the set of clock constraints and resets. The proof is as in [12]. Lemma 4 Set R forms a set of regions; R is compatible with the clock constraints G(X) and clock resets U0 (X).

4 Clock Reduction and Decidability In this section, we give a technique for reducing the number of clocks in a WIRTA to one. The clock reduction is due to Lemma 2. This simplifies the region partitioning to give regions which can be called integral, non-integral and saturated. For simplicity, we consider WIRTAs where all the location invariants are true. The component η which assigns true to all locations will be omitted from the description of WIRTAs. All the results obtained can be extended to the case of having general location invariants. Definition 4 Let τ ∈ R+ , and let int(τ ) = k. Define  (δ)k if τ is integral, dt(τ )  k (δ) δ if τ is non-integral. Let τ1 ≤ τ2 be two real numbers. dte(τ2 , τ1 ) is the δ-pattern that is to be concatenated to the right of dt(τ1 ) to get dt(τ2 ). For example, if τ1 = 1.3 and τ2 = 2.9, then dt(τ1 ) = δδ while dt(τ2 ) = δδδ. Therefore, dte(τ2 , τ1 ) = δ. In the following, we assume that all runs begin from time 0, and that time progresses in a weakly monotonic sense. Definition 5 Let A be a WTA and let l0 ∈ L0 . Consider two paths ρ and ρ  visiting the sequence l0 l1 l2 · · · ln of locations such that li is visited at time ti in ρ and at time ti in ρ  . Define f (ρ) to be l0 dte(t1 , t0 ) l1 dte(t2 , t1 ) l2 · · · ln−1 dte(tn , tn−1 ) ln (f (ρ  ) is  ) ln ). Then, ρ and ρ  are said to be l0 dte(t1 , t0 ) l1 dte(t2 , t1 ) l2 · · · ln−1 dte(tn , tn−1   f -equivalent (ρ ∼ = ρ ) iff f (ρ) = f (ρ ).

656

Theory Comput Syst (2011) 48: 648–679

Proposition 1 Let A be a WIRTA. Let ρ ∼ = ρ  . Then ρ(ρ  ) is a path in TA taking the  sequence e1 , . . . , en of edges iff ρ (ρ) is. Proof The proof is easy to see since all constraints in the WTA compare clock values only to integer constants—since ρ ∼ = ρ  , ρ  can take the exact sequence of edges as ρ.  Let [ρ] = {ρ  | ρ ∼ = ρ  } and define f ([ρ]) = {f (ρ  ) | ρ ∼ = ρ  }. Clearly, f ([ρ]) is a f singleton, we henceforth denote it by f (ρ). Let TA denote the set of all equivalence classes [ρ]. Note that if A is not a WIRTA, then Proposition 1 need not hold good as given by Corollary 1 below. Corollary 1 Proposition 1 need not be true if A is a WTA but not a WIRTA. Proof Consider the following WTA.

y:=0

0.3

1.2

Consider paths ρ = (l, 0, 0) −→ (l, 0.3, 0.3) −→ (m, 0, 0.3) −→ (m, 0.9, y<1?

0.3

y:=0

1.5

1.2) −→ (n, 0.9, 1.2) and ρ  = (l, 0, 0) −→ (l, 0.3, 0.3) −→ (m, 0, 0.3) −→ (m, 1.2, 1.5) −→ (n, 1.2, 1.5). f (ρ) = f (ρ  ) = lδmδn, hence, ρ ∼ = ρ  . However, ρ is a path   in the automaton while ρ is not. 4.1 Marked Automaton MA As a first step in obtaining a one clock WIRTA from a given WIRTA A, we obtain from A, a marked automaton MA . The passage of time between integral and nonintegral regions in A is marked using symbols δ,  in MA . MA has a single clock cMA , the locations of MA are of the form (l, α) where l is a location of L, and α is a region over clocks X ∪ {n}, where n is a new clock that is reset only when a clock reset happens in A. t A time elapse transition in A of the form (l, ν) −→ (l, ν +t) where ν(x) is integral and ν(x) + t is non-integral for x ∈ X is represented in MA as a discrete transition δ

(l, α) −→ (l, α i ) where α i is the immediate successor of α. Similarly, a time elapse t transition in A of the form (l, ν) −→ (l, ν +t) where ν(x) is non-integral and ν(x)+t 

is integral for x ∈ X is represented in MA as a discrete transition (l, α) −→ (l, α i ). The clock cMA keeps track of the progress of time between integral and non-integral regions. A guard cMA ∈ (0, 1) should be satisfied on a δ transition, while a guard cMA = 1 should be satisfied on a  transition. cMA is reset to zero everytime it attains the value of 1 on the  transition. A path from (l, α) to (l, αk ) on δ,  transitions in MA corresponds to time elapse in the location l in A and has as many s as the number of time units elapsed. This is also indicated by the difference between the intervals α(x) and αk (x) for any clock x ∈ X ∪ {n}. A discrete transition (l, ϕ, φ, l  ) of A is represented by marked discrete

Theory Comput Syst (2011) 48: 648–679

657

transitions from (l, α) to (l  , α  ) on the symbol  such that α |= ϕ, cMA = 0 if α is integral, and cMA ∈ (0, 1) if α is non-integral, and α  is obtained from α by resetting the clocks in φ (if any) and n. If φ = ∅, then α  = α. Definition 6 Given a WIRTA A = (L, L0 , X, Z, E, θ, C), we construct a marked weighted timed automaton MA corresponding to A as MA = (Q, Q0 , {cMA }, Z, Em , θm , Cm ) where – – – –

Q = L × R where R is the set of regions defined for X ∪ {n} where n ∈ X, Q0 = L0 × {α0 } such that α0 = {ν0 }, ν0 (x) = 0 for all x ∈ X ∪ {n}, Z is the set of costs as in A, Em ⊆ Q × {δ, , } × G({cMA }) × U0 ({cMA }) × Q is the set of edges. For q = (l, α) and q  = (l  , α  ), an edge em = (q, a, ϕm , φm , q  ) ∈ Em is such that 1. if α(x) = (cm , ∞) for all x ∈ X ∪ {n}, then q = q  , a ∈ {δ, }, ϕm :: true and φm = ∅, 2. if l = l  , α is integral and α  = α i , then a = δ, ϕm :: 0 < cMA < 1 and φm = ∅, 3. if l = l  , α  is integral and α  = α i , then a = , ϕm :: cMA = 1 and φm = {cMA }, 4. For a discrete transition (l, ϕ, φ, l  ) ∈ E, there exists a transition((l, α), , ϕm , ∅, (l  , α  )) ∈ Em such that (1) α |= ϕ, (2) α  = α[φ ∪ {n} := 0] if φ = ∅, else α  = α, and (3) ϕm :: cMA = 0 if α is integral, else ϕm :: 0 < cMA < 1,

– θm : Q → 2AP such that θm (q) = θ (l) for q = (l, α), – Cm : Q ∪ Em → N|Z| such that 1. Cm (q) = C(l) if q = (l, α), 2. Cm (em ) = C(e) if em = (q, , ϕm , ∅, q  ), e = (l, ϕ, φ, l  ), q = (l, α) and q  = (l  , α  ), 3. Cm (em ) = 0 if em = (q, δ, ϕm , ∅, q  ) or em = (q, , ϕm , φm , q  ) where q = (l, α) and q  = (l, α  ). The semantics of MA = (Q, Q0 , {cMA }, Z, Em , θm , Cm ) is given by a labelled timed transition system TM just as in the case of A. Note It should be noted that due to the loop consisting of both δ and  over locations with regions α such that α(x) = (cm , ∞) for all x, the paths might contain arbitrary sequences of δ, . A time elapse between a δ transition and a subsequent  transition is possible. However, due to the constraint 0 < cMA < 1? accompanying both δ and , and due to the nature of the cost function, it is possible to delay the δ transition to ensure that the  is taken after δ with no time elapse in between. In the following, we restrict TM to only those paths in which δ and  strictly alternate and such that any  which follows a δ() has the same time stamp as its immediate predecessor (δ or ). Let ρm be a path in TM . A sequence of transitions between locations (l, α), (l, αk+1 ) in ρm indicates time elapse in the corresponding location l of A. Let w ∈ {δ, }∗ be a word obtained by concatenating the δ’s and ’s appearing on the edges

658

Theory Comput Syst (2011) 48: 648–679

between (l, α), (l, αk+1 ). Note that there are no  transitions between (l, α), (l, αk+1 ). Define h(ρm ) = l0 w1 l1 w2 · · · ln−1 wn ln where wi+1 is the word over {δ, } between  (li , α) and (li , αki +1 ). There is a transition (li , αki +1 ) −→ (li+1 , αk i +1 ) in MA for all i ≥ 0 corresponding to the discrete transition between li and li+1 in TA .  are h-equivalent (ρ ≡ ρ  ) iff h(ρ ) = h(ρ  ). Let We say that the paths ρm , ρm m m m m   [ρm ] = {ρm | ρm ≡ ρm }, and let TM h denote the set of equivalence classes [ρm ]. Let h([ρm ]) = {h(ρ) | ρ ≡ ρm }. h([ρm ]) is a singleton, and we denote h([ρm ]) by h(ρm ). Proposition 2 Let MA be the marked automaton obtained from a WIRTA A. Let  . Then ρ (ρ  ) is a path in M taking the sequence e , . . . , e of edges iff ρm ≡ ρm m m 1 n A  ρm (ρm ) is. Proof The proof is similar to that of Proposition 1.



Lemma 5 Let A = (L, L0 X, Z, E, θ, C) be a WIRTA and let MA = (Q, Q0 , {cMA }, Z, Em , θm , Cm ) be its marked automaton. 1. For every path ρ of TA , there exists a cost preserving path ρm of TM such that f (ρ) = h(ρm ). 2. For every path ρm of TM where the δ,  strictly alternate, there exists a cost preserving path ρ of TA such that f (ρ) = h(ρm ). 3. There exists a bijection g : TA f → TM h such that f ([ρ]) = h(g([ρ])) and h([ρm ]) = f (g −1 ([ρm ])). For every ρ ∈ [ρ], there exists a cost preserving path ρm ∈ g([ρ]), and vice versa. Proof We give a proof sketch, the details of which can be easily worked out. t1

(ϕ1 ,φ1 )

(ϕn ,φn )

1. Let ρ = (l0 , ν0 , μ0 ) −→ (l0 , ν1 , μ1 ) −→ (l1 , ν1 , μ1 ) · · · (ln−1 , νn , μn ) −→ (ln , νn , μn ) be a path in TA . From the definition of MA we know the following.

– Corresponding to every state (li , νi+1 , μi+1 ) [or (li , νi , μi )] of A, by definition of Q, there exists (li , αi+1 ) [or (li , αi )] ∈ Q such that νi+1 ∈ αi+1 [or νi ∈ αi ] restricted to X. ti+1 – From the δ,  transitions of Em , we know that forall i, if (li , νi , μi ) −→ (li , νi+1 , μi+1 ), then there exists a path over word wi+1 from (li , αi ) to (li , αi+1 ). The number of s in wi+1 is the number of time units elapsed and is indicated by the difference between the intervals αi (x) and αi+1 (x) for any clock x. As νi+1 (x) − νi (x) = ti+1 − ti , νi ∈ αi , νi+1 (x) ∈ αi+1 , and there is a path from αi to αi+1 over wi+1 , we have dte(ti+1 , ti ) = dte(νi+1 (x), νi (x)) = wi+1 . (ϕi ,φi )

– From the  transitions of Em , we know that forall i, if (li−1 , νi , μi ) −→  (li , νi , μi ), then there exists (li−1 , αi ) −→ (li , αi ) such that αi |= ϕi and αi = αi [φ ∪ {n} := 0] (with appropriate constraint on cMA ).

We can construct a path ρm using the above information such that for every discrete transition in ρ there is a corresponding  transition, while for time elapse ti+1 − ti there is a path labeled with dte(ti+1 , ti ). Hence f (ρ) = l0 dte(t1 , t0 ) l1

Theory Comput Syst (2011) 48: 648–679

659

· · · dte(tn , tn−1 ) ln and h(ρm ) = l0 w1 l1 · · · wn ln are the same. Additionally, due to the cost function C of MA we can prove that the cost valuations in ρ before and after time elapse and discrete transitions are maintained in ρm . 2. Similar to 1. 3. From 1, we have for every path ρ ∈ TA , a path ρm in TM such that f (ρ) = h(ρm ). From 2, we have the reverse implication. By Proposition 1, any two paths ρ, ρ  in A such that ρ ∼ = ρ  follow the same sequence of edges; likewise by Proposition 2,  such that ρ ≡ ρ  in M follow the same sequence of any two paths ρm , ρm m A m edges. The proof follows from the observation that from 1, 2 above, we can find  for every ρ ∈ [ρ] in A, a path ρm ∈ [ρm ] in MA and vice-versa. Corollary 2 In the case of a WTA which is not a WIRTA, the 3rd property listed in the above theorem need not hold due to Corollary 1. Note Our construction does not extend to WTAs, because from Corollary 1 we know that no partitioning of the form TA f exists for a WTA. 4.2 One Clock WIRTA In this section, we give a construction to obtain a single clock WIRTA A from MA such that for every path ρ  ∈ TA , there exists a cost preserving path ρ ∈ TA . Definition 7 (δ −  sequence) Let (l, α) be a location in MA . A δ −  sequence starting at (l, α) is a sequence of locations lα = (l, α0 )(l, α1 ) · · · (l, αk+1 ) with lα [i] = (l, αi ) is the ith location in the sequence. Here α0 = α and ∀j ≥ 0, αj +1 = αji (immediate successor of αj ), and any path in TM consisting of only these locat1,1

t1,2

a

tions is of the form ((l, α0 ), γ0 , χ0 ) −→ ((l, α0 ), γ1 , χ1 ) −→ ((l, α1 ), γ1 , χ1 ) −→ a

t1,k+1

δ

((l, α1 ), γ2 , χ2 ) −→ ((l, α2 ), γ2 , χ2 ) · · · −→ ((l, αk ), γk+1 , χk+1 ) −→ ((l, αk+1 ), γk+1 , χk+1 ) where 1. a, a  ∈ {δ, }, 2. The δ,  moves strictly alternate, 3. The location (l, αk+1 ) has a self loop on δ,  in MA . Let L = {lα | (l, α) ∈ L × R} be the set of δ −  sequences in MA . The one clock WIRTA is built by considering L as the set of locations. Recall that the locations of MA are of the form (l, α) where α is a region for X ∪ {n}. α(n) is made zero after an  transition only whenever some clock x ∈ X is reset in A. Thus, clock n records the time elapsed between two resets in the transitions of A. The one clock WIRTA A constructed uses n as its only clock. The initial location of A is sα0 , where s ∈ L0 and α0 is the region (0, 0, . . . , 0). Treating a sequence lα as a location, we enable transitions from lα whenever there is a transition from lα [i] = (l, αi ), i ≥ 0 in MA . The guard to be satisfied on such a transition is that value of n which agrees with αi (n). The discrete transitions in A are defined as follows: a transition is taken from a location lα to a location lα  with guard ϕ defined as n ∈ αi (n) whenever there is an

660

Theory Comput Syst (2011) 48: 648–679

Fig. 2 WIRTA A

Fig. 3 Marked Weighted Automaton M corresponding to the WIRTA of Fig. 2. Locations of M are of the form (l, α), r Where l is a location in A, α = (Ix , Iy , In ) ∈ R the set of regions for the set X ∪ {n} and r ∈ N|Z| is the cost of the location. Intervals of α are represented as follows: c for [c], c+ , c < cm + for (c, c + 1) (here cm = 2) and cm for (cm , ∞). For readability, some of the states have been replicated and the resets, guards of cMA associated with δ and  edges are not shown. Each row here is a δ −  sequence. For instance, the row marked s(0,0,0) consists of all locations in the δ −  sequence starting at location (s, (0, 0, 0))

 transition in MA from lα [i] to lα  [j ]. The transition does not reset n if αj (n) = 0, while n is reset if αj (n) = 0.

Theory Comput Syst (2011) 48: 648–679

661

Formally, the definition of the one clock WIRTA is given below. Definition 8 Let MA = (Q, Q0 , {cMA }, Z, Em , θm , Cm ) be the marked automaton corresponding to a WIRTA A. Construct the one clock WIRTA A = (L , L0 , {n}, Z, E  , θ  , C  ) as follows: L = {lα | (l, α) ∈ Q}, L0 = {sα | (s, α) ∈ Q0 }, Z = the set of costs as in MA , E  ⊆ L × G({n}) × U0 ({n}) × L consists of transitions e = (lα , ϕ, φ, lα  ) ∈ E  iff there exists em = (lα [i], , lα  [j ]) ∈ Em , i, j ≥ 0. ϕ defined as n ∈ αi (n) and φ = {n} iff αj (n) = 0, (recall that lα [i] = (l, αi ) and lα  [j ] = (l  , αj )), – θ  : L → 2AP is given as θ (lα ) = θm (l, α), where (l, α) ∈ Q, – C  : L ∪ E  → N|Z| is defined as C  (lα ) = Cm (l, α) where (l, α) ∈ Q, C  (e) = Cm (em ) where e ∈ E  is the edge defined above corresponding to an edge em of Em .

– – – –

The semantics of A are given by the labelled timed transition system TA in the usual way. A path ρ in TA is a sequence of consecutive transitions of the t1

(ϕ1 ,φ1 )

(ϕn ,φn )

form (lα0 , ν0 , μ0 ) −→ (lα0 , ν1 , μ1 ) −→ (lα1  , ν2 , μ2 ) · · · −→ (lβn , νm , μm ). Recall that f (ρ) = lα0 dte(t1 , t0 ) lα1  · · · dte(tn−1 , tn ) lβn . Define ρ ≈ ρ  for two paths ρ, ρ  in A iff f (ρ) = f (ρ  ). [ρ] = {ρ  | ρ ≈ ρ  } and let TA f denote the set of equivalence classes [ρ]. As earlier, we denote f ([ρ]) by f (ρ). The following lemma can be proved similar to Lemma 5. Lemma 6 Let MA = (Q, Q0 , {cMA }, Z, Em , θm , Cm ) be the marked automaton obtained from a WIRTA A and let A = (L , L0 , {n}, Z, E  , θ  , C  ) be its one clock WIRTA. 1. For every path ρm of TM where the δ,  strictly alternate, there exists a cost preserving path ρ of TA such that f (ρ) = h(ρm ). 2. For every path ρ of TA , there exists a cost preserving path ρm of TM such that f (ρ) = h(ρm ). 3. There exists a bijection g : TM h → TA f such that h([ρm ]) = f (g([ρm ])) and f ([ρ]) = h(g −1 ([ρ])). For every ρm ∈ [ρm ], there exists a cost preserving path ρ ∈ g([ρm ]), and vice versa. Theorem 2 Let A be a WIRTA and let A be the one clock WIRTA obtained from MA . Then for every path ρ ∈ TA , there is a path ρ  in TA such that ρ ∼ = ρ  . Further,  the accumulated costs in the corresponding locations of ρ, ρ are identical. Proof The proof follows from Lemmas 5 and 6.



Complexity Let cm be the highest constant used in the guards of a WIRTA A = (L, L0 , X, Z, E, θ, C). Then the number of intervals I is 2 ∗ (cm + 1) and the number of regions

662

Theory Comput Syst (2011) 48: 648–679

Fig. 4 Single clock WIRTA A corresponding to MWA M of Fig. 3

of A is (2 ∗ (cm + 1))|X| . The number of locations in the marked automaton MA = (Q, Q0 , {cMA }, Xm , Z, Em , θm , Cm ) is |Q| = |L| × (2 ∗ cm + 2)|X|+1 . Each δ −  sequence lα is a location in A . The number of δ −  sequences is |L | ≤ |L| × (2 ∗ cm + 2)|X|+1 . Thus, starting from a WIRTA A with |L| locations, we can obtain a one clock path preserving, cost preserving single clock WIRTA A with at most |L| × (2 ∗ cm + 2)|X|+1 locations. Related Work The technique described above can be used in the case of IRTA [25] to obtain a deterministic one clock IRTA A starting from an IRTA A. We will then start with A, obtain MA , determinize MA and then proceed to obtain A . Determinizing MA would give rise to one exponent—this would make A doubly exponential in size. This is an improvement over the following earlier results: – The result in [28], where a deterministic one clock IRTA A is obtained starting from an IRTA A—however, A is triply exponential in size with respect A. – The result in [29], where a deterministic one clock IRTA A is obtained starting from an IRTA A—even though A is doubly exponential in size with respect to A, A introduces -moves when A has none. – The result in [7], where a deterministic IRTA A is obtained starting from an IRTA A—even though A is doubly exponential in size with respect to A, it needs cm + 1 clocks, where cm is the maximum constant used in the guards of A. To conclude, we mention the result of [22], where the δ −  theory is replaced by an extremely simple theory, and obtains the same result viz., a one clock deterministic IRTA A from an IRTA A with the blow up in the size of A being atmost doubly exponential. [22] also shows that this upper bound is tight. Theorem 3 Model checking WCTL1 on WIRTA is decidable. Proof Combine the proof of Theorem 2 with the decidability of model checking WCTL1 on WTAs [15]. 

Theory Comput Syst (2011) 48: 648–679

663

5 Undecidability Results In this section, we describe two undecidability results: (1) for showing that WCTL2r model checking is undecidable on WIRTAs with 3 stopwatch costs and 1 clock—this improves the result of [17], and (2) for showing the undecidability of WCTL1 model checking on WTAs with 2 clocks and 1 stopwatch cost—this solves a long standing open question [14, 15]. The proof technique we use for undecidability is by reducing the problem to that of the halting problem for 2 counter machines. Deterministic Two Counter Machine A 2-counter machine M with counters c1 and c2 can be described by a program formed by five basic instructions: – – – – –

lk : goto ln ; lk : if ci = 0 then goto lk1 else goto lk2 ; (check for zero) lk : ci = ci + 1; (increment counter ci ) lk : ci = ci − 1; (decrement counter ci preceded by check for zero) lk : HALT;

Without loss of generality, assume that the instructions are labelled l1 , . . . , ln where ln = HALT (a special instruction) and that in the initial configuration, both counters have value zero. The behavior of the machine is described by a possibly infinite sequence of configurations l1 , 0, 0, l1 , C11 , C21 , . . . , lk , C1k , C2k , . . . where C1k and C2k are the respective counter values and lk is the label of the kth instruction. The halting problem of such a machine is known to be undecidable [24]. In the following, a state (l, −, (a1 , a2 , a3 )) represents that the current location is l, with stopwatches zi having value ai , and we do not care about the value of clock x. Similarly, a state (l, −, (a1 , −, a3 )) represents that the current location is l, with stopwatches z1 , z3 having value a1 , a3 , and we do not care about the value of clock x and stopwatch z3 . A “−” in a component should be understood as a dont care value. Lemma 7 Model checking WCTL2 on WIRTA with 1 clock and 3 stopwatch costs is undecidable. Proof Reference [17] has shown that WCTL2 model checking on WTAs with 3 stopwatch costs and 1 clock is undecidable. This proof, with minimal modifications as given in the next line, can be used to show the result for WIRTAs. Replace all occurrences of constraint x = 1? with x = 1?, x := 0, and add x = 0? as a constraint over all the other edges.  5.1 Model Checking WCTL2r on WIRTAs with 1 Clock and 3 Stopwatch Costs We construct a WIRTA A and a WCTL2r formula Ψ such that for q0 , the initial location of A, the counter machine halts if, and only if, (q0 , 0, (0, 0, 0))  Ψ . Let x be the clock used, and let Z = {z1 , z2 , z3 } be the stopwatch cost variables. The counters c1 and c2 of the counter machine are represented as c1 = n1 − n2 and c2 = n3 − n4 , where ni ∈ N, 1 ≤ i ≤ 4. The values of counters c1 , c2 are encoded as μ(z1 ) = 1 − 2n113n2 and μ(z2 ) = 1 − 2n313n4 . The normal form for the clock and

664

Theory Comput Syst (2011) 48: 648–679

Fig. 5 Module for instruction li :: goto lk

Fig. 6 Module Ai and ψI1 :: I1 ⇒ E[I1 U (k1 ∧ z3 = 0 ∧ ψC )] to increment c1 . Module C is given in Fig. 7 and location k1 is in module C

stopwatches is ν(x) = 0, μ(z1 ) = 1 − 2n113n2 , μ(z2 ) = 1 − 2n313n4 and μ(z3 ) = 0 where ν (μ) is the clock (cost) valuation. For each instruction li of M, there is a location labelled li in A. There is a location labeled HALT corresponding to the instruction HALT. The values of the clock and stopwatches are in the normal form at locations labeled li . We have separate modules for each instruction and the final WIRTA is obtained by connecting these appropriately. The final formula is given by Ψ :: z1 .z2 .z3 .[E (ψall U (HALT ∧ z3 = 0))], where ψall will be given at the end of this section. The module for instruction li :: goto lk is given in Fig. 5. The instructions of M are simulated as follows. 1 to z1 = 1 − 2n113n2 . 2n1 +1 3n2 Decrement c1 : Increment n2 by adding 23 . 2n113n2 to z1 = 1 − 2n113n2 . Checking if c1 is zero : c1 = 0 iff n1 = n2 . This is achieved by multiplying the value 2n113n2 by 6 an integral number of times till it becomes 1. Multiplying 2n113n2 once by 6 decrements both n1 and n2 .

1. Increment c1 : Increment n1 by adding 2. 3.

4. Identical operations can be performed with respect to counter c2 by reversing the roles of z1 and z2 in all the modules pertaining to c1 . Increment c1 The module to increment c1 is given in Fig. 6. The formula ψI1 :: I1 ⇒ E I1 U (¬I1 ∧ z3 = 0 ∧ ψC ) ensures that the amount of time spent in the location j1 is 12 .(1 − z1 ). The correctness of the module incrementing c1 is given by Lemma 12. Lemma 8 In the module getx2 in Fig. 7, there exists a path from (k1 , t, (−, 0, 0)) to (k2 , t  , (−, 1, t  )) iff t  = t. Lemma 9 In the module Addi in Fig. 7, there exists a path from (a1 , −, (δ1 , δ2 , 0)) to (A, ta , (δ1 , δ2 + ta , 0)) witnessing ψAi iff ta = δ1 . Lemma 10 If a run enters module check in Fig. 7, with initial values z1 = 1 − α + t, z2 = t  and z3 = t then ψC2 holds iff t  = α.

Theory Comput Syst (2011) 48: 648–679

665

Fig. 7 Module Add and formula ψAi :: (Ai ∧ z3 = 0) ⇒ E[¬AiF U (AiF ∧ z1 = 1 ∧ z3 = 0)] ensure that time spent in location a2 is the same as the value of z1 . Module check is associated with the formula ψC2 :: C2 ⇒ E[¬C2F U (C2F ∧ z2 = 1 ∧ z1 = 2 ∧ z3 = 2)]. Module C is associated with the formula ψC :: z2 .z3 . E¬C1 U[C1 ∧ z2 = 1 ∧ z2 . E¬C2 U{C2 ∧ ψC2 ∧ z3 . E(¬CF ∧ ψA1 ∧ ψA2 )U(CF ∧ z2 = 2 ∧ z3 = 0)}]

Lemma 11 If a run enters module C in Fig. 7, with values z1 = 1 − α + t and x = t, then ψC holds iff t = α2 . (Note that 0 < α, t ≤ 1.) Proof In the module C, along a path from location k1 to CF , the value of z2 is α before entering the Add1 module (from Lemmas 8 and 10). Due to Lemma 9, the value of z2 is α + 1 − α + t + 1 − α + t on reaching CF . Such a path is a witness of ψC iff z2 = α + 1 − α + t + 1 − α + t = 2 ⇐⇒ t = α2 .  Lemma 12 In the module Ai given in Fig. 6, there exists a path from (li , 0, (1 − 1 1 1 1 2n1 3n2 , 1 − 2n3 3n4 , 0)) to (li+1 , 0, (1 − 2n1 3n2 + t, 1 − 2n3 3n4 , 0)) witnessing ψI1 iff 1 t = n1 +1 n2 . (Due to the final formula Ψ , z3 = 0 in li+1 .) 2

3

This lemma follows from Lemma 11. Note that in module C of Fig. 7, the value of x does not go beyond 1 (or 2) before the reset x = 1?x := 0 (correspondingly x = 2?x := 0) even though it is not accounted for in the calculations. From Fig. 6, it is clear that when the module C is entered, 0 < x ≤ 1. Thus the total time elapsed in locations k2 and k3 is at most 2. Similar argument holds in all the resets in other modules too.

666

Theory Comput Syst (2011) 48: 648–679

Fig. 8 Module Az and formula ψZ1 check if counter c1 is zero. ψZ1 :: [l11 ⇒ E l11 U (M0 ∧ψE )]∧ [l12 ⇒ E l12 U (M0 ∧ ψE )]. Module E is given in Fig. 9 and location M0 is in module E

Decrement c1 The module to increment n2 is similar to that in Fig. 6 with I1 replaced by D1 ; C is replaced by another module C  (to check if value of x is t = 23 ∗ α with z1 being 1 − α + t). This module is obtained from C by an additional Add3 before location CF . The formula ψC  would compare z2 to 3 instead of 2 as in ψC . As a consequence of this modification, z2 = α + 1 − α + t + 1 − α + t + 1 − α + t = 3 when CF is reached, which in turn ensures that t = 23 ∗ α. Thus, the formula to decrement counter c1 is ψD1 :: D1 ⇒ E[D1 U (¬D1 ∧ z3 = 0 ∧ ψC  )]. Check for c1 to be Zero The module Az given in Fig. 8 and the formula ψZ1 together ensure that c1 is zero iff location li1 is reached (else li2 is reached and c1 is non-zero). From the representation of c1 as n1 − n2 , it follows that c1 = 0 iff n1 = n2 . One way of checking whether n1 = n2 is to decrement n1 and n2 every step and check if both of them become zero at the same time. As c1 is encoded by the stopwatch z1 = 1 − 2n113n2 , simultaneous decrement of n1 and n2 is achieved follows: store α = 2n113n2 into stopwatch z2 , double the value of z2 (making value of z2 = 2 ∗ α), and then add 2 ∗ z2 to the current value of z2 (making z2 = 6 ∗ α). This makes the value of z2 6 times 2n113n2 . This is done until z2 = 1. If z2 attains the value of 1 after i iterations, then 6i . 2n113n2 = 1, indicating that n1 = n2 . The module E in Fig. 9 does the above calculation. Lemma 19 proves this. Lemma 13 If a run enters module M in Fig. 9 with values z1 = 1 − α, z2 = t and z3 = 0 then ψM1 holds iff t = α. Lemma 14 If a run enters module F1 in Fig. 9 with values z2 = α + t and x = t (0 < t < 1), then ψF1 holds iff t = α. Lemma 15 If a run enters module G in Fig. 10 with values z2 = β + t, z3 = t and z1 = t2 , then ψG holds iff t2 = β.

Theory Comput Syst (2011) 48: 648–679

667

Fig. 9 Module E checks if n1 = n2 with the help of the formula ψE :: z2 .z3 . E (¬MF ∧ ψM1 ∧ ψDn ∧ψDn )U(MF ∧z3 = 0∧z2 = 1). Here ψM1 :: M1 ⇒ E ¬M1F U(M1F ∧z2 = 1∧z3 = 1∧z1 = 1) 1 2 pertains to the module M while ψF1 :: z1 .z3 . E ¬B3 U [B3 ∧ z1 = 1 ∧ z1 . E¬BF U (BF ∧ z1 = 1 ∧ z2 = 1 ∧ z3 = 1)] is for the module F1 . The formulae ψDn :: Dn1 ⇒ E Dn1 U(¬Dn1 ∧ z3 = 0 ∧ ψF1 ) and 1 ψDn :: Dn2 ⇒ E Dn2 U(¬Dn2 ∧ z3 = 0 ∧ ψF2 ) ensure that n1 and n2 are decremented respectively. 2 Module F2 and formula ψF2 are given in Fig. 10

Lemma 16 If a run enters module H in Fig. 10 with values z1 = t2 , z2 = 0 and x = t4 , then ψH holds iff t2 = t4 . Lemma 17 If a run enters module F2 in Fig. 10 with values z2 = β + t and x = t (0 < t < 1), then ψF2 holds iff t = 2 ∗ β. This lemma follows from Lemmas 15 and 16. The module F2 and formula ψF2 ensure that z2 = 3 ∗ β, decrementing n2 in module Dec_n2 of Fig. 9. Lemma 18 Consider the modules Dec_n1 and Dec_n2 in Fig. 9. 1. There exists a path from (d11 , −, (−, α, 0)) to (Dn1 , td1 , (−, α + td1 , 0)) witnessing ψDn1 iff td1 = α. 2. There exists a path from (d21 , −, (−, β, 0)) to (Dn2 , td2 , (−, β + td2 , 0)) witnessing ψDn2 iff td2 = 2 ∗ β. Follows from Lemmas 14 and 17.

668

Theory Comput Syst (2011) 48: 648–679

Fig. 10 Module F2 and formula ψF2 ensure that t = 2 ∗ β given the values x = t and z2 = β + t . The formula is ψF2 :: z1 .z3 . E ¬H1 U [H1 ∧ z1 = 1 ∧ z1 . E ¬H4 U {H4 ∧ ψG ∧ z2 . E(¬HF ∧ ψH ) U (HF ∧ z1 = 1 ∧ z2 = 1 ∧ z3 = 1)}]. Here ψG :: H4 ⇒ E ¬H4F U (H4F ∧ z1 = 1 ∧ z2 = 1 ∧ z3 = 1) and ψH :: (H5 ∧ z2 = 0) ⇒ E H5 U (H5F ∧ z1 = 1 ∧ z2 = 0)

Lemma 19 If a run enters module E in Fig. 9, with values z1 = 1 − holds iff n1 = n2 (that is iff c1 = 0).

1 2n1 3n2

then ψE

Proof Let α = 2n113n2 . Consider a path from location M0 to MF . This path is a witness of ψE iff upon reaching MF , the value accumulated in stopwatch z2 is 1. From Lemma 13, the value in z2 is α upon reaching M1 . The path can then reach MF from M1 either directly or after i loops through modules Dec_n1 and Dec_n2 . If MF is reached directly and z2 = 1, then α = 1. This implies n1 = n2 = 0. From Lemma 18, it follows that the value accumulated in z2 after one loop is 6α = 6. 2n113n2 = n1 −11 n2 −1 . Thus, one loop through the modules Dec_n1 and Dec_n2 2 3 has the effect of decrementing n1 and n2 . If the path reaches MF after i loops, then the accumulated cost is z2 = 6i α. The path is a witness iff z2 = 6i α = 1. Hence,  n1 = n2 . Now, we shall describe the final formula which will ensure that all the modules are associated with their respective formulae. Ψ :: z1 .z2 .z3 .E ψall U (HALT ∧ z3 = 0)

Theory Comput Syst (2011) 48: 648–679

669

 where ψall :: i=1,2 ψIi ∧ ψDi ∧ ψZi . A is obtained by adjoining all modules such that the target state lk of a module coincides with the start state lk of another module. Theorem 4 A, (l1 , 0, (0, 0, 0)) |= Ψ iff M halts. Proof We show that if A, (l1 , 0, (0, 0, 0)) |= Ψ , then M halts by building the halting x=0?

computation of M. Let ρ be the path witnessing Ψ . Then ρ = (l1 , 0, (0, 0, 0)) −→ x=0?

· · · −→ (HALT, −, (−, −, 0)) such that ψall holds in all the states. From the construction, we know that the module starting at (li , 0, (−, −, 0)) simulates the instruction li in M. Let s be a state occurring in ρ. – If s = (li , 0, (−, −, 0)) or s = (l j , −, (−, −, 0)) then it trivially satisfies ψall . – If s = (I1 , t, (1 − 2n113n2 + t, −, 0)) then it satisfies ψall iff it satisfies ψI1 . From Lemma 12, we know that if s |= ψI1 then t = 12 . 2n113n2 incrementing n1 . Thus 1 1 s = (I1 , 2n1 +1 , (1 − 2n1 +1 , −, 0)). 3n2 3n2

– Similarly if s = (D1 , t, (1 − 2n113n2 + t, −, 0)) or s = (I2 , t, (−, 1 − 2n313n4 + t, 0)) or s = (D2 , t, (−, 1 − 2n313n4 + t, 0)), then n2 or n3 or n4 have been incremented respectively. – If s = (l11 , 0, (1 − 2n113n2 , −, 0)) then s |= ψZ1 and thus satisfies ψE . From Lemma 19, it follows that n1 = n2 . Similarly if s = (l12 , 0, (1 − 2n113n2 , −, 0)), then n1 = n2 .

It is clear from A and Ψ that no time elapses in locations li , Ij , Dj , lj1 and lj2 , ∀i and j ∈ {1, 2}. Consider the case where s = (I1 , t, (1 − 2n113n2 + t, −, 0)) is a state in ρ. As no time elapses in I1 , there is a single instance of I1 between two consecutive occurrences of li and li+1 and s |= ψI1 . Hence the state 1 1 (li+1 , 2n1 +1 , (1 − 2n1 +1 , −, 0)) is reached after s. This ensures that the values 3n2 3n2 of stopwatches updated by the module Ai+1 are indeed the result of simulating instruction li . Thus A and Ψ simulate M. Associate a tuple (li , (ni1 − ni2 ), (ni3 − ni4 )) with each state (li , 0, (1 − ni1 ni , 1 − 1 ni ni 2 33 4

2 13

2

, 0)) in ρ. Now the path ρ gives a sequence of tuples (l1 , 0, 0)(l2 , −, −)

· · · (HALT, −, −). This sequence represents the halting computation of M. To show that if M halts, then A, (l1 , (0, 0, 0)) |= Ψ we construct a path ρ  witnessing Ψ using the halting computation of M. Without loss of generality, let (l1 , 0, 0)(l2 , 1, −) · · · (li , c1i , c2i ) · · · (HALT, −, −) be the halting computation of M. Construct another sequence of tuples (l1 , (0 − 0), (0 − 0))(l2 , (1 − 0), (0 − 0)) · · · (li , (ni1 − ni2 ), (ni3 − ni4 )) · · · (HALT, −, −) where is nij or nij + 1 such that ∀i, ni1 − ni2 = c1i ni3 − ni4 = c2i . Now ∀i, j, ni+1 j construct a path ρ  in A such that ρ  = (l1 , 0, (0, 0, 0))  (I1 , 12 , ( 12 , 0, 0))  (l2 , 0, ( 12 , 0, 0)) · · · (li , 0, (1 − ni1 ni , 1 − ni1 ni , 0)) · · · (HALT, −, (−, −, 0)). Ad2 13

2

2 33

4

ditionally, if the instruction li corresponds to checking if c1 = 0 then select state (l11 , 0, (−, −, −)) after (li , 0, (−, −, −)) if c1i = ni1 − ni2 = 0; else choose (l12 , 0, (−, −, −)).

670

Theory Comput Syst (2011) 48: 648–679

It is clear from ρ  that no time elapses in locations li , Ij , Dj , lj1 and lj2 , ∀i and 1 1 j ∈ {1, 2}. From Lemma 12, it follows that for all i, (I1 , ni +1 , (1 − ni +1 , ni ni 2

1

3

2

2

1

3

2

−, 0)) |= ψI1 . Similar argument holds for locations I2 , D1 , D2 . From Lemma 19, if c1i = 0, then (l11 , 0, (−, −, −)) |= ψZ1 ; else (l12 , 0, (−, −, −)) |= ¬ψZ1 . Thus ρ  is a witness of Ψ as ψall holds in all states in ρ  . Hence, A, (l1 , 0, (0, 0, 0)) |= Ψ iff M halts.  Theorem 5 The WCTL2r model checking problem on WIRTAs with 1 clock and 3 stopwatch costs is undecidable. The proof follows from the construction of A, formula Ψ and Theorem 4. 6 Model Checking WCTL1 over WTAs with 2 Clocks and 1 Stopwatch In this section, we show that the question of model checking WTA with 2 clocks and 1 stopwatch is undecidable using the logic WCTL1 . The decidability question of model checking WTAs with 2 clocks and one stopwatch has been open for a long time [14–17] with respect to both WCTL1 and WCTL2r . Theorem 6 The WCTL1 model checking problem on WTAs with 2 clocks and 1 stopwatch cost is undecidable. Proof We construct a WTA A and a WCTL1 formula Φ such that for q0 , the initial location of A, the counter machine halts if, and only if, (q0 , (0, 0), 0)  Φ. The counters c1 and c2 of the counter machine are encoded as follows: 1 , 5c1 · 7c2 1 ν(x2 ) − ν(x1 ) = 1 − c 5 1 · 7c2 ν(x1 ) − ν(x2 ) =

where, x1 and x2 are clocks and ν(x1 ), ν(x2 ) are the valuations of the clocks. We say that the encoding is in normal form when ν(x2 ) = 0. At the beginning and end of every main module (increment, decrement and check for zero), the clocks will be in the normal form. The cost function assigns cost 0 and 1 only to the locations. The set L of the automaton states contains a location labelled lk for each program label lk of the counter machine. The initial location q0 is labelled by l0 . We now encode the instructions of the counter machine M. Instruction lk : goto lk  ; can be encoded by making an edge (with no cost) from the location labeled lk to the location labeled lk  and the edge going out of lk has the constraint x2 = 0?. The instruction lk : HALT; is represented by a location labeled HALT. In the following sections, we shall describe how the rest of the instructions, namely, increment, decrement and checking for zero are encoded. The modules for each of these and the corresponding WCTL1 formula for each type of instruction will be provided. The individual modules are connected to form the final WTA A.

Theory Comput Syst (2011) 48: 648–679

671

Decrement c1 According to the encoding of counters done by clock values we deduce that, in order to decrement the value of counter ci we need to multiply ν(x1 ) − ν(x2 ) by 5 or 7. Figure 11 shows the decrement of counter c1 . Lets examine Fig. 11. At entry, x1 = xold , x2 = 0, so that the initial value of x1 − x2 while entering lk is xold . The value of x1 is reset to 0 on the transition to G, thereby giving x1 = 0, x2 = 1 − xold . At G , we have x1 = xold , x2 = 0. A non-deterministic amount of time is spent at G . Let this time be k. Now, x1 = xold + k, x2 = k. Lets denote xold + k as xnew . Therefore, x1 = xnew , x2 = xnew − xold on leaving G . Now we shall use a WCTL1 formula to force the value xnew to be 5 times xold . The formula dec, is as follows: dec ≡ C ⇒ E(CU=0 (E[¬CU=1 C  ])) dec says that there exists a path from location C to location C  such that time elapsed at C is 0 and the total cost to reach C  is 1. x1 = xnew , x2 = xnew − xold on entry into C, where no time can elapse (the final formula Φ we construct will demand that the there is a path to a location labeled HALT with cost 0). The cost accumulated at H is 1 − xnew . Then, x1 = 0, x2 = 1 − xold on exiting H . To satisfy the constraint on exiting from P0 , a time xold must be spent, making the accumulated cost to be 1 − xnew + 5 × xold which must be 1 for dec to hold. That is, 1 − xnew + 5 × xold = 1 which gives us xnew = 5 × xold . Thus, the new value xnew of x1 is 5 times the old value xold of x1 − x2 . dec checks the value of x1 at C and the value of x2 is reset as soon as we leave C. The case for decrementing counter c2 can be handled by replacing cost 5 with 7. Note that the location P0 in Fig. 11 with cost 5 can be replaced by a sequence of locations as shown in the Fig. 12 such that they use only stopwatch costs. Similar short hand notation shall be used henceforth but it can always be redrawn with just stopwatch costs.

Fig. 11 Decrement counter c1

Fig. 12 Part of Fig. 11 redrawn with only stopwatch costs

672

Theory Comput Syst (2011) 48: 648–679

Fig. 13 lk : if c2 = 0 goto lk1 else goto lk2

Fig. 14 Check c2 zero

Lemma 20 If a run enters location lk in Fig. 11 with x1 = 5i17j , x2 = 0, i > 0, and enters location lk+1 some time units later, then x1 = 5i−11 7j , x2 = 0. Check Counter c2 for Zero For the instruction lk : if ci = 0 goto lk1 else goto lk2 , we need to check whether the value of counter ci is 0 or not. According to the encoding we will have to check if the value of x1 − x2 is only a power of 15 or a power of 17 . Figure 13 gives the module for checking if the value of counter c2 is zero. The WCTL1 formula chk2 used is the following: ψ ≡B

⇒

E(BU=0 (E¬BU=1 D)),

chk2 ≡ A

⇒

E(AU(E(¬A ∧ ψ)U=0 Y )).

Entry into lk happens with x1 = xold , x2 = 0. chk2 holds good in the module only if there exists a path which will finally reach Y with cost 0. ψ is satisfied at B only if every time we go through B the value of x1 is multiplied with 5. Thus, for every movement around the loop, the value of the encoding becomes five times its last value. Thus, there exists a path from A to Y only if the original value of the counter was just a multiple of 15 ; otherwise the value can never become 1 unless we multiply it by 7. If the value of clock becomes greater than 15 then the condition at B can no longer be satisfied. Thus, this checks if the value of counter c2 is 0. Similarly, to check if counter c2 is non-zero, we construct a module that looks exactly same as Fig. 14, but by replacing labels l with l  . The formula ¬chk2 is checked on this module. ψ  ≡ B

⇒

E(B  U=0 (E¬B  U=1 D  )),

Theory Comput Syst (2011) 48: 648–679

673

Fig. 15 Incrementing ci

chk2 ≡ A

⇒

E(A U(E(¬A ∧ ψ  )U=0 Y  )).

For checking whether counter c1 is 0 or not, we have modules which are the same as Fig. 14 replacing cost 5 with 7. The corresponding WCTL1 formula remains the same. Lemma 21 If a run enters location lk of Fig. 13 with x1 = 5i17j , x2 = 0, i > 0, then it will enter location B of Fig. 14 for the first time with x1 = 5i−11 7j , x2 = 1 − 5i17j + 1 . Such a run enters location Y only if j = 0. 5i−1 7j Increment c1 The counter machine instruction to be encoded is lk : increment ci , go to lk+1 . We need to divide the value of the encoding by 5 or 7. The module in Fig. 15 depicts the increment of counter ci . The time spent at the location J must be such that x1 − x2 gets divided by 5 or 7. Let xold be the old value of x1 − x2 when entering at location lk . Since x2 is reset to zero at the end of every module, we have x1 = xold , x2 = 0 at lk . At location J , the values are x1 = 0, x2 = 1 − xold . Let xnew be the amount of time spent at location J . Then the values while entering location I are x1 = xnew , x2 = 1 − xold + xnew . The constraint x2 < 1? forces xnew < xold . At location I , we want to verify points P1, P2 given below. No time will be spent at I (this will be enforced by the final formula Φ). P1 xnew is of the form 5i17j , and P2 xold − xnew is of the form 5i47j in the case of incrementing c1 and is of the form 6 in the case of incrementing counter c2 . 5i 7j We then use the points P1, P2 to show that if xold = 5i17j , then xnew = 5i+11 7j in the case of incrementing c1 and xnew = 5i 71j +1 in the case of incrementing c2 . We have submodules Fig. 16 for P1 and Fig. 17 for P2. Check P1 Now, we look at the module in Fig. 16 that checks P1. The purpose of this module and the corresponding WCTL1 formula is to check if the current value of the encoding (value of x1 − x2 ) is of the type 5i17j . Recall that while entering this module, x2 = 0, x1 = xnew . The WCTL1 formula inc_chk_1 to check on this module is f1 ≡ F ⇒ E(F U=0 (E(¬F )U=1 F  )),

674

Theory Comput Syst (2011) 48: 648–679

Fig. 16 Checking xnew is of the form i1 j 57

f2 ≡ S ⇒ E(SU=0 (E(¬S)U=1 S  )), inc_chk_1 ≡ E(f1 ∧ f2 )U=0 V where, formulae f1 , f2 ensure that movement along a loop multiplies the value of the encoding by 5 or 7 according to the loop taken. The formula inc_chk_1 holds in the module only if the value of the encoding is of the form 5i17j , since, only in that case will the final value of the encoding become equal to 1—this is the only way to reach V . We shall now explain with respect to Fig. 16 how P1 is checked. On entry, we have x1 = xnew , x2 = 0. These values are preserved while entering X. A non-deterministic amount of time (k ≤ 1) is spent at X. Lets examine the case when the control enters location S from X. The values of the clocks are x1 = xnew + k, x2 = k while entering S. Let k  = k + xnew so that x1 = k  , x2 = k  − xnew . No time is spent at S (the formula f2 ensures this). At L , 1 − k  time is spent, incurring a cost 1 − k  , and x1 = 0, x2 = 1 − xnew . At K0 , xnew amount of time is spent, accumulating the cost to 1 − k  + 7xnew , and x1 = xnew , x2 = 0 on exiting K0 . The formula f2 demands that the total cost between S and S  is 1, therefore, k  = 7xnew . Thus, on leaving X, x1 = 7xnew . The initial value xnew of x1 (or x1 − x2 ) is multiplied by 7. If we had entered F instead of S, f1 would check that the x1 − x2 gets multiplied by 5. The control can switch to T from S, F each time a multiplication is done, and at the very end, reaching V is possible only if the value of xnew we started out with (recall that we started out with x1 = xnew , x2 = 0) is of the form 5i17j . Lemma 22 If a run enters location U in Fig. 16 with x1 = α ∈ (0, 1] and x2 = 0, then α is of the form 5i17j for i, j ≥ 0. Check P2 Next, we look at the module (in Fig. 17) which checks P2 : if xold − xnew is of the form 5i47j . On entry, we have x1 = 0, x2 = 1 − xold + xnew . This module has some extra checks as compared to the previous one. The formula to be checked on this module is inc_chk_2 ≡ E(f1 ∧ f2 ∧ f3 )U=0 V

Theory Comput Syst (2011) 48: 648–679

Fig. 17 Checking xold − xnew is of the form

675

4 5i 7j

where f1 , f2 are as defined before and f3 defined as f3 ≡ N

⇒

E(N U=0 E(¬N U=1 Q)).

These ensure that xold − xnew is of the form

4 5i 7j

.

Lemma 23 If a run enters location W with x1 = 0 and x2 = 1 − α + β, α, β ∈ [0, 1), then α − β is of the form 5i47j . We now describe checking P2 with respect to Fig. 17. On entry, x1 = 0, x2 = 1 − xold + xnew . We simply explain how f3 is checked as f1 , f2 are the same as in P1. Now, if we take the path down, no time is spent at T , and we reach O with the same values. At O, a non-deterministic amount of time k2 gets spent, and x1 = k1 + k2 , x2 = k2 . Let k3 denote k1 + k2 . Thus, x1 = k3 , x2 = k3 − k1 at N . No time is spent at N (as required by formula f3 ) and a time of 1 − (k3 − k1 ) = 1 − k2 is spent at R, with cost 1 − k2 . This makes x1 = 1 + k1 , x2 = 0 at Z. A time elapse of 1 − k1 from Z takes us to Z  , with x1 = 0, x2 = 1 − k1 with no extra cost. At Z  , a time k1 is elapsed, giving x1 = k1 , x2 = 0. At M, a time of 1 − k1 is elapsed, making the total cost (1 − k2 ) + 5(1 − k1 ) which must be 1 for f3 to hold. Therefore, k2 = 5(1 − k1 ). Note that to satisfy the guard x2 = 1 from N to V , k2 = 1 Thus, k1 = 45 . Recall that k1 = 5i 7j (xold − xnew ). This proves the claim that (xold − xnew ) is of the form 5i47j . Combining the formulae inc_chk_1 and inc_chk_2, we obtain a formula to check that at location I , so that points P1 and P2 hold. The formula inc is defined as follows: ψ1 ≡ (inc_chk_1 ∧ (AG¬I )), ψ2 ≡ (inc_chk_2 ∧ (AG¬I )), inc ≡ I

⇒

E(I U=0 ψ1 ) ∧ E(I U=0 ψ2 ).

676

Theory Comput Syst (2011) 48: 648–679

In a similar manner, we can construct modules for incrementing counter c2 by replacing cost 5 with cost 7 in the path from N to Q. We now need to prove that points P1, P2 can simultaneously hold iff xnew = 5i+11 7j while incrementing counter c1 whenever xold = 5i17j , and that xnew = 5i 71j +1 while incrementing counter c2 whenever xold = 5i17j . Lemma 24 For i, j, i1 , j1 , n ∈ N ∪ {0}. 5i − 7j = (−1)n 4 · 5i1 · 7j1

iff i = 1 and j, i1 , j1 = 0 and n = even,

(1)

5i − 7j = (−1)n 6 · 5i1 · 7j1

iff j = 1 and i, i1 , j1 = 0 and n = odd,

(2)

5 i · 7 j − 1 = 4 · 5 i 1 · 7 j1

iff i = 1 and j, i1 , j1 = 0,

(3)

5 i · 7 j − 1 = 6 · 5 i 1 · 7 j1

iff j = 1 and i, i1 , j1 = 0.

(4)

Proof For the proof we shall use the equalities listed below: For n ∈ N, (a) 74n mod 10 = 1, 74n+1 mod 10 = 7, 74n+2 mod 10 = 9 and 74n+3 mod 10 = 3 (b) 5n mod 10 = 5, 5n mod 4 = 1, 5n mod 6 = 1 iff n = 2k and, for n > 1, 5n mod 100 = 25. We shall prove that it is not possible for i, j, i1 , j1 , n to take any other value. This shall be done as follows: Case 1 For (1) and (2), suppose i1 = 0 and i = 0. For (1), we have 4 · 5i1 mod 5 = 0 while we can easily see that (5i − 7j )mod 5 = 0. We have similar situation for (2). Also, we can prove that it is not possible to have j1 = 0 and j = 0 which can be done by taking mod 7 on both sides. The RHS would turn out to be 0 while the LHS would be non-zero. Case 2 For (3) and (4), suppose i1 = 0 and i = 0. For (3), we have 4 · 5i1 mod 5 = 0, while we can easily see that (5i · 7j − 1)mod 5 = 0. We have a similar situation for (4). Also, we can prove that it is not possible to have j1 = 0 and j = 0 which can be done by taking mod 7 on both sides. The RHS would turn out to be 0 and LHS will be non-zero. Thus, at least one of i and i1 and at least one of j and j1 must be zero because neither can i and i1 be non-zero simultaneously nor j and j1 . Taking this into account, we proceed further. Case 3 Suppose 5i − 1 = 4 · 7j1 with i = 1 and j1 = 0. Take mod 10 both sides. As (5i − 1)mod 10 = 4 we have, 4 · 7j1 = 4(mod 10). Thus, 7j1 = 1(mod 10) ⇒ j1 = 4k. So, it reduces to 5i − 1 = 4 · 2401k . Taking mod 100 on both sides, 4 · (2401)k mod 100 = 4 × 1 = 4 but (5i − 1)mod 100 = 25 − 1 = 24 (for i > 1) and (5i − 1)mod 100 = 0 for i = 0. Thus, contradiction. Case 4 Suppose 7j − 1 = 6 · 5i1 with j = 1 and i1 = 0. Take mod 10 on both sides. As 6 × 5 = 30, we have 7j mod 10 = 1. Thus, i1 is of the form 4n. But, (74k − 1)mod 8 = (7k − 1)(7k + 1)(72k + 1)mod 8 = 0 which is not true for the RHS as it only has a single factor of 2. Similarly, we can handle the case of 7j − 1 = 4 · 5i1 where the RHS has a factor of 4 but not 8.

Theory Comput Syst (2011) 48: 648–679

677

Case 5 Suppose 5i −1 = 6·7j1 . Take mod 4 on both sides. Then, (5i −1)mod 4 = 0. For the RHS, (6 · 7i )mod 4 = 0. Thus, contradiction. Case 6 Suppose 7j − 5i = 4. Then, 7j − 4 = 5i . Taking mod10 both sides, we have 7j mod 10 = 9 making j = 4k1 + 2 = 2k. Thus, we have 72k − 4 = (7k − 2)(7k + 2) = 5i . As we know none of (7k − 2) or (7k + 2) can be 1, we have for i1 , i2 = 0, 7k − 2 = 5i 1 ,

(5)

7k + 2 = 5i 2 .

(6)

Subtracting (5) from (6), we have 4 = 5i1 − 5i2 , which is not possible unless i2 = 0. Thus, contradiction. Case 7 Suppose 7j − 5i = 6 with j = 1 and i = 0. Clearly, j = 0 is not possible. So, let j > 1. Taking mod 10 on both sides we get j = 4k. So, the equation becomes 2401k − 5i = 6. Take mod 6 on both sides. This gives 5i mod 6 = 1 which implies i = 2m. Thus, we have 74k − 52m = (72k − 5m )(72k + 5m ) which is greater then 6 for k, m = 0. Thus, contradiction. Case 8 Suppose 5i − 7j = 6. Taking mod10 both sides we get j = 4k + 2. Now, take mod 4 on both sides. We have, (5i − 49 × 2401k )mod 4 = 1 − 1 × 1 = 0, while 6 mod 4 = 2. Thus, contradiction. Case 9 Suppose 5i − 7j = 4 with i = 1 and j = 0. Clearly, i = 0 is not possible. Taking mod 10 both sides we get j = 4k. Now, take mod 100 on both sides. We have (5i − 2401k ) mod 100 = 25 − 1 = 24, while 4 mod 100 = 4. Thus, contradiction. Case 10 Suppose 5i · 7j − 1 = 4 with i = 1 and j = 0. This is not possible as the least value of LHS is 6. Similarly, 5i · 7j − 1 = 6 with i = 0 and j = 1 is also not possible as the two least values are 4 and 24, rest all being greater than 24. Thus, we have negated the possibility of any other case. This proves that we 6 can have xold − xnew of type 5i 4·7j iff xnew = xold 5 and xold − xnew of type 5i ·7j xold iff xnew = 7 . This proves our assertion. Hence, checking the form of xnew and xold − xnew suffices to check if xnew is the required one. This takes care of encoding the incrementing step of the counter machine.  Summing Up We have seen modules and corresponding WCTL1 formula which take care of each instruction of the counter machine M. The automaton A will be formed by joining the modules in the order in which instructions appear in the linear program of the counter machine. We define ψ as the conjunction of all the WCTL1 formulae restricting the run through the automaton. ψ ≡ inc ∧ dec ∧ chk1 ∧ ¬chk1 ∧ chk2 ∧ ¬chk2 .

678

Theory Comput Syst (2011) 48: 648–679

The WCTL1 formula Φ that needs to be checked by A in order to encode the working of counter machine M is: Φ ≡ E(ψU=0 HALT). HALT is the label of the location representing the HALT instruction of the counter machine. The HALT location has to be reached with cost 0 which enforces that during the path one can not wait on locations with cost greater than 0. If the counter machine halts, then the path which models the WCTL1 formula is the one which follows the instruction set of the counter machine. If there is a path that models the WCTL1 formula Φ, then an instruction set corresponding to the run must exist which definitely halts and reaches the HALT instruction. Therefore, (l0 , (0, 0), 0) |= Φ iff the counter machine M halts. 

7 Concluding Remarks In this paper, we have continued the study of the WCTL model checking problem on WTAs. We have identified a subclass of WTAs on which WCTL1 model checking is decidable, irrespective of the number of clocks and costs. The question for WCTL2r is undecidable with WIRTAs having 3 stopwatch costs and 1 clock. We have also given a solution for the decidability question of WCTL1 model checking for WTAs with 2 clocks and 1 stopwatch cost. Some interesting questions that need to be answered are (i) The decidability question for model checking WCTL2 , WCTL2r on WIRTA with 2 stopwatch costs, (ii) Model checking WCTL1 , WCTL2 on WIRTA with multiconstrained modalities.

References 1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994) 2. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real time. Inf. Comput. 104(1), 2–34 (1993) 3. Alur, R., Henzinger, T.A., Ho, P.-H.: Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22(3), 181–201 (1996) 4. Alur, R., Fix, L., Henzinger, T.: Event-clock automata, a determinizable class of timed automata. Theor. Comput. Sci. 211, 253–273 (1999) 5. Alur, R., La Torre, S., Pappas, G.: Optimal paths in weighted timed automata. In: Proceedings of HSCC’01. LNCS, vol. 2034, pp. 49–62. Springer, Berlin (2001) 6. Alur, R., La Torre, S., Madhusudan, P.: Perturbed timed automata. In: Proceedings of HSCC’05. LNCS, vol. 3414, pp. 70–85. Springer, Berlin (2005) 7. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T.: When are timed automata determinizable? In: Proceedings of ICALP’09(2). LNCS, vol. 5556, pp. 43–54. Springer, Berlin (2009) 8. Behrmann, G., David, A., Larsen, K.G., Möller, O., Pettersson, P., Yi, W.: Uppaal—present and future. In: Proceedings of the 40th IEEE Conference on Decision and Control’01. IEEE Computer Society Press, Los Alamitos (2001) 9. Behrmann, G., Fehnkar, A., Hune, T., Larsen, K.G., Petterson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Proceedings of HSCC’01. LNCS, vol. 2034, pp. 147–161. Springer, Berlin (2001) 10. Bérard, B., Duford, C.: Timed automata and additive clock constraints. Inf. Process. Lett. 75(1–2), 1–7 (2000)

Theory Comput Syst (2011) 48: 648–679

679

11. Bérard, B., Gastin, P., Petit, A.: On the power of non observable actions in timed automata. In: Proceedings of STACS’96. LNCS, vol. 1046, pp. 257–268. Springer, Berlin (1996) 12. Bouyer, P., Duford, C., Fleury, E., Petit, A.: Updatable timed automata. Theor. Comput. Sci. 321(2–3), 291–345 (2004) 13. Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. In: Proceedings of FST&TCS’05. LNCS, vol. 3821, pp. 432–443. Springer, Berlin (2005) 14. Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Inf. Process. Lett. 98(5), 188–194 (2006) 15. Bouyer, P., Larsen, K.G., Markey, N.: Model checking one-clock priced timed automata, Log. Methods Comput. Sci. 4(2), 9 (2008) 16. Brihaye, T., Bruyère, V., Raskin, J.: Model-checking for weighted timed automata. In: Proceedings of FORMATS/FTRTFT’04. LNCS, vol. 3253, pp. 277–292. Springer, Berlin (2004) 17. Brihaye, T., Bruyère, V., Raskin, J.: On model-checking timed automata with stopwatch observers. Inf. Comput. 204(3), 408–433 (2006) 18. Choffrut, C., Goldwur, M.: Timed automata with periodic clock constraints. J. Autom. Lang. Comb. 5(4), 371–404 (2000) 19. Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool KRONOS. In: Proceedings of Hybrid Systems’95. LNCS, vol. 1066, pp. 208–219. Springer, Berlin (1995) 20. Demichelis, F., Zielonka, W.: Controlled timed automata. In: Proceedings of CONCUR’98. LNCS, vol. 1466, pp. 455–469. Springer, Berlin (1998) 21. Henzinger, T., Manna, Z., Pnueli, A.: What good are digital clocks? In: Proceedings of ICALP’92. LNCS, vol. 623, pp. 545–558. Springer, Berlin (1992) 22. Manasa, L., Krishna, S.N.: Integer reset timed automata—clock reduction and determinizability. CoRR/abs/1001.1215 (2010). Available at http://arxiv.org/abs/1001.1215v1/ 23. Manasa, L., Krishna, S.N., Nagaraj, K.: Updatable timed automata with additive and diagonal constraints. In: Proceedings of CiE’08. LNCS, vol. 5028, pp. 407–416. Springer, Berlin (2008) 24. Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, New York (1967) 25. Nagaraj, K.: Topics in timed automata. Master’s Thesis. Department of Computer Science & Engineering, Indian Institute of Technology, Bombay, July 2006 26. Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: closing a decidability gap. In: Proceedings of LICS’04, pp. 54–63. IEEE Computer Society, Los Alamitos (2004) 27. Suman, P.V., Pandya, P.K., Krishna, S.N., Manasa, L.: Timed automata with integer resets: language inclusion and expressiveness. In: Proceedings of FORMATS’08. LNCS, vol. 5215, pp. 78–92. Springer, Berlin (2008) 28. Suman, P.V., Pandya, P.K., Krishna, S.N., Manasa, L.: Timed automata with integer resets: language inclusion and expressiveness. Research report TIFR-SPKG-GM-2008/1, Tata Institute of Fundamental Research, Bombay 2008. Available at http://www.tcs.tifr.res.in/~vsuman/TechReps/ IrtaLangInclTechRep.pdf 29. Suman, P.V., Pandya, P.K.: Determinization and expressiveness of integer reset timed automata with silent transitions. In: Proceedings of LATA’09. LNCS, vol. 5457, pp. 728–739. Springer, Berlin (2008)