Lecture 10: Discretizing Dense Time A. PnueliDiscretizing Dense TimeSince there are only finitely many regions, it is possible to find a rational point withsmall denominator as a representative of each region. If there arek clocks, weneed at leastk + 1 different fractional numbers, so we can take δ =1k+1to be theunit of discretization.The main question is whether we can follow any dense computation by discreterepresentatives whose clocks assume values of the formnδ for some natural n.Consider the following computation of a system with three clocks:ht1: 1.2 , t2: 1.4 , t3: 1.6itick(0.7)−→ ht1: 1.9 , t2: 2.1 , t3: 2.3ireset(t3)−→ht1: 1.9 , t2: 2.1 , t3: 0.0iIf we record the effect of this computation on the ordering of the fractional partsof the clocks, it can be written as0 < f1< f2< f3tick(0.7)−→ 0 < f2< f3< f1reset(t3)−→0 = f3< f2< f1Attempting to emulate this behavior with clocks ranging overn4, we start with ht1:1.25 , t2: 1.50 , t3: 1.75i, and immediately see that there is no time increment∆ =n4which will lead to a state satisfying 0 < fr(1.50 + ∆) < fr(1.75 + ∆) <fr(1.25 + ∆).Timed and Hybrid Systems, NYU, Spring, 2007 178Lecture 10: Discretizing Dense Time A. PnueliThe ProblemSimply increasing the resolution of δ will not solve the problem.Claim 16. There exists a CTS D3with 3 clocks such that, for every discretizationunitδ, there exists a computation of D3which cannot be emulated by acomputation over the time domain{nδ|n ≥ 0}.By using combinations oftick steps and resets, the pathologic computation of D3switches back and forth between states satisfying 0 < f1< f2< f3and statessatisfying0 < f1< f3< f2, where the difference f2− f1is preserved in thetransition from0 < f1< f2< f3to 0 < f1< f3< f2and the difference f3− f1ispreserved in the transition from0 < f1< f3< f2to 0 < f1< f2< f3. Obviously,these differences get smaller and smaller and, at the end, must become smallerthanδ which is impossible in a δ-discrete computation.Timed and Hybrid Systems, NYU, Spring, 2007 179Lecture 10: Discretizing Dense Time A. PnueliSystems with Weak InequalitiesConsider a restricted class of CTS’s in which all inequalities are of the formsxi≤ Uior xj≥ Lj. For this class, we can use a significantly more compactdiscretization.Claim 17. Letϕbe an assertion using only weak inequalities over the clocks,and letD be a weak-inequalities CTS. Then a state satisfyingϕis D-reachableunder the dense time model iff it isD-reachable under integer time.This claim states thatinteger-time provides a faithful simulation of dense time.Clearly, if aϕ-state is reachable under integer time, it is also reachable underdense time. It remains to show that any dense-time computation can be simulatedby an appropriate integer-time computation.Letσ : s0, s1, . . . , smbe a dense-time computation leading to the state smsuchthatsm|=ϕ. Let t0= 0, t1, . . . , tmbe the values of the clocks at the statess0, . . . , sm, respectively. In particular, let T0, . . . , Tmbe the values of the masterclock at these states. For eachi < m, let γi(t) be the condition on the clockswhich allowed the computation to move fromsito si+1. We also take γm=ϕ.Timed and Hybrid Systems, NYU, Spring, 2007 180Lecture 10: Discretizing Dense Time A. PnueliProof ContinuedObviously, for every i < m and every clock tj∈ C, the value tijcan be expressedas a differencetij= Ti− Tkwhere skis the state on whose entry clock tjwaslast reset. In casetjwas not reset before state i, Tk= T0= 0. Thus, wecan translate eachγi(t) into a boolean combination of constraints stating weakupper and lower bounds on differences of the formTi− Tk. Satisfying all of theseconditions will yield a sequence of valuesT0, . . . , Tmwhich correspond to entrytimes of a feasible computation leading tosm.The fact thatσ : s0, s1, . . . , smis a dense computation shows that the resultingset of inequalities has a rational solution. We will proceed to show that if a setof weak inequalities of the formLki≤ Ti− Tk≤ Ukihas any solution, it alsohas aninteger solution. This will establish the existence of an integer sequenceT0≤ T1≤ · · · ≤ Tmfrom which we can construct an integer computation leadingto a stateesmwhich satisfies γm(tm) =ϕ(tm).Timed and Hybrid Systems, NYU, Spring, 2007 181Lecture 10: Discretizing Dense Time A. PnueliA Lemma and Its ProofLemma 1. LetS(T0, . . . , Tm): {0 ≤ Lki≤ Ti− Tk≤ Uki| k ≤ i ≤ m}be a set of inequalities. Then, S has a solution iff it has an integer solution.Assume that we constructed the graph representationG of the system S. Withoutloss of generality, assume thatT0= 0 and every other variable Tifor 0 < i ≤ mhas the constraint 0 ≤ Ti. Note that since all inequalities are weak, all edges willbe dashed.Apply the process oftightening to the graph G. We claim that since the systemS is consistent (has a solution) the process of tightening must terminate. Assumeto the contrary, that the process does not terminate. Observe that, wheneverwe replace a label of an edgeeijby a bigger label cij, this implies that we haveidentified apath from node Tito node Tjsuch that the sum of its (original) labelsequalscij. Note also that this update implies that the constraint Tj− Ti≥ cijis aconsequence of the original constraints.Assume that the tightening process fails to terminate, because the label ofeijhas been updated infinitely many times. Let π1, π2, . . . be an infinite enumerationTimed and Hybrid Systems, NYU, Spring, 2007 182Lecture 10: Discretizing Dense Time A. Pnueliof all the paths leading from Tito Tjsorted by increasing length. If we comparethe accumulated weights of these paths, we find that infinitely often we identifya path which has a bigger weight than all of its predecessors. In particular, thisimplies that there exist two pathsπmand πn, with m < n and w(πn) > w(πm),such thatπncontains a cycle whose removal would reproduce πm. It follows thatthe removed cycle has a positive weight, implying thatS can have no solution.Since we know thatS has a (rational) solution, this is impossible.We therefore conclude that the tightening process terminates. When itterminates, we have thatcik≥ cij+ cjkholds for every i, j, and k. Furthermore, ifthe original constraints were of the formTi− Tk≥ Lki, then the final values of ckisatisfies Lki≤ cki.We are now ready to identify the solution. We takeT0= 0 and, for everyi > 0, Ti= c0i. We will show that these values for Tisatisfy