On Nonlinear Prices in Timed Automata

Priced timed automata provide a natural model for quantitative analysis of real-time systems and have been successfully applied in various scheduling and planning problems. The optimal reachability problem for linearly-priced timed automata is known to be PSPACE-complete. In this paper we investigate priced timed automata with more general prices and show that in the most general setting the optimal reachability problem is undecidable. We adapt and implement the construction of Audemard, Cimatti, Kornilowicz, and Sebastiani for non-linear priced timed automata using state-of-the-art theorem prover Z3 and present some preliminary results.

Introduction
Timed automata, introduced by Alur and Dill [3], extend finite state automata with continuous variablesreferred as clocks-that evolve with uniform rates. Time automata syntax permits comparing clocks with integers as guard on transitions and as well as invariants on locations (states), and also allows clock resets as a way to remember the time a transition was last fired. These features of time automata are general enough to permit modeling rich timing properties of real-time systems while providing a decidable verification framework. Timed automata have been quite successful in practice due to their appealing theoretical properties as well as the presence of mature verification tools such as UPPAAL.
Priced timed automata [9,8] are extensions of timed automata which permit us to model cost associated with staying at locations as well as taking discrete transitions. Priced timed automata are useful in modeling various decision-theoretic problem in the presence of strict timing constraints. The most natural problem studied on these models is the optimal reachability problem (shortest path problem) where the goal is to find the minimum (or maximum) cost to reach a given set of locations.
Linearly-priced timed automata [6] (LPTA), also known as weighted timed automata, are subclasses of priced timed automata where prices change linearly with respect to delay incurred at particular location. For LPTA the optimal reachability problem is known to be decidable and is shown to be PSPACEcomplete exploiting a clever extension of region graphs to so-called corner-point abstraction by Bouyer et al. [8]. Alur et al. [4] earlier gave an EXPTIME algorithm to solve the problem with an arbitrary initial state by giving a non-trivial extension of the region graph. Larsen et al. [6,9] gave a symbolic algorithm to solve the problem, although with some restrictions on the initial state (a corner state with all clocks set to zero). A recent result by Fearnley and Jurdzinksi [13] showed that the PSPACE-hardness results hold for timed automata with two clocks [13]. On the other hand, for timed automata with one clock, reachability-time and reachability-price problems are known to be NL-complete [19].
In practice, however, the requirement for nonlinear pricing models is quite common. As an example consider the optimal scheduling problem of battery usage in embedded systems studied by Jongerden et al. [16]. In this work authors modeled batteries using kinetic battery model (KiBaM). KiBaM itself is a nonlinear model, but Jongerden et al. [16] manually discretized it to required approximation to model the whole problem as optimization on LPTA. Similar scenarios can be cited from other application domains of priced timed automata such as scheduling [7], resource modeling and analysis [14], and optimal synthesis [15]. However, we believe that providing non-linear price modeling facilities directly in the language of timed automata will further their applicability in system design. Jurdzinski and Trivedi [18] introduced a non-linear subclass of priced timed automata, so-called concavely-priced timed automata, where prices in each location are certain concave prices of valuation and time delays. Exploiting the concave nature of the prices, they showed that the optimal price reachability problem for this class of automata has the same complexity as that of LPTA. Priced timed automata with exponential price functions were studied in a restricted context by Bouyer et al. [10] and Fahrenberg and Larsen [12].
In this paper we uniformly study various subclasses of (non-linear) priced timed automata, and study the boundary between decidable and undecidable variants of PTA. Towards this goal we first show the undecidability of the optimal reachability problem for unrestricted priced timed automata by showing a reduction from the halting problem for two-counter machines. For reasoning with decidable variants, we first introduce a key notion of price-preserving bisimilarity. We exploit this notion to formalize reduction for the optimal cost reachability problem for piecewise-linear priced timed automata to linearly priced timed automata. We also show the decidability of ε-optimal cost reachability for priced timed automata with Lipschitz-continuous prices. Finally, we adapt the construction of Audemard, Cimatti, Kornilowicz, and Sebastiani [5] for bounded model-checking of timed automata using SAT solvers to work for bounded reachability problem for non-linearly priced timed automata using SMT solver Z3 [11]. In conjunction with a decision procedure for the theory of the class of price functions (for instance polynomial prices [17,11]), our implementation can be used to compute bounded-step cost-optimal schedules for priced timed automata. We demonstrate the applicability of our approach using airplane landing problem [7]. This paper is organized as follows: we begin by defining syntax and semantics of generalized priced timed automata in the next section. We define various pricing models and their hierarchy. We prove key undecidability result in Section 3 and show decidability results in Section 4. Finally, in section 5 we present the details of our implementation and experimental results.

Priced Timed Automata
We denote sets of integers, rational numbers and real numbers as Z, Q and R respectively. Their respective non-negative subsets are denoted as Z + , Q + and R + .
Let X = {x 1 , x 2 , . . . , x n } be the finite set of clocks. A clock valuation is a map ν : X → R + . Thus, a given clock valuation ν maps clock x i to a value ν i . This fact is written as ν(x i ) = ν i . In n-tuple form, a clock valuation ν is denoted as (ν 1 , ν 2 , . . . , ν n ). Given a clock valuation ν and τ ∈ R + , ν + τ is the clock valuation defined by (ν 1 + τ, ν 2 + τ, . . . , ν n + τ). A guard is any finite conjunction of clauses of the form x i ∼ c, where clock x i ∈ X , constant c ∈ Z + and ∼ is one of the comparison operators in set {<, ≤, =, >, ≥}. Let G be the set of guards. Given a valuation ν and a guard g = j (x i ∼ c j ), ν g means expression j (ν(x i ) ∼ c j ) evaluates to true. For Y ⊆ X , ν[Y := 0] denotes clock valuation in which clocks in Y are reset to 0 while other clocks remain unchanged.
Timed Automata. A timed transition system T is a tuple (L, X , E) where (i) L is a finite set of locations, (ii) X is a finite set of clocks variables, and (iii) E is set of transitions. A configuration of T is a pair (ℓ, ν), where ℓ ∈ L is a location and ν in clock valuation over set X . Let Q T be the set of configurations for the timed transition system T . There are two types of transitions over Q T : We write E = E τ ∪ E e for the set of transitions of timed transition system T .
Definition A timed automaton A is a tuple (L, X , E, I) where (i) L is a finite set of locations (ii) X is a finite set of clocks (iii) E ⊆ L × G × 2 X × L is a finite set of edges (iv) I : L → G assigns an invariant to each location.
The semantics of timed automaton A is given as a timed transition system A run ρ = q 0 → q 1 → · · · → q m of the timed automaton A is a finite path in the induced timed transition system T A where every q i is configuration in T A and → is either delay or switch edge in E A . We use notation ρ = q 0 q m for a run from q 0 to q m . We write Runs(q, q ′ ) for the set of runs from the location q to q ′ . A run is said to be canonical if delay and switch transitions alternate.
Priced timed automata. A priced timed automaton (PTA) is a timed automaton A = (L, X , E, I, π, ψ) augmented with a price functions π : Q A × R + → R + and ψ : E → Z + which assign prices (costs) for waiting at locations and taking edges, where Q A is the set of the configurations of timed automaton A . Let A be a PTA and Then the cost C(ρ) of the run ρ is equal to C d (ρ)+C s (ρ) where C d (ρ) = ∑ m k=1 π(q ′ k−1 , τ k ) and C s (ρ) = ∑ m k=1 ψ(e k ) are the duration and switching costs of ρ respectively.
A priced timed transition system T is a tuple (L, X , E) where (i) L is a set of locations (ii) X is a finite set of clocks (iii) E is a set of transitions. A configuration is a tuple (ℓ, ν, u), where ℓ ∈ L is a location, ν is a clock valuation over set X and u ∈ R is current accumulated price. Let Q T be the set of configurations for timed transition system T . There are two types of transitions defined over Q T : We write E = E τ ∪ E e for the set of transitions of timed transition system T . A priced timed transition system is said to be canonical if for its every run, delay transitions and switch transitions occur in the strict alternation. Observe that two consecutive delay transitions like (ℓ 1 , ν 1 , u 1 ) because for non-linear price functions such clubbing may not yield valid transitions. Similarly, there cannot be consecutive switch transitions without zero delay transition between them.
Let A = (L, X , E, I, π, ψ) be a priced timed automaton. The semantics of A are given by a canonical priced timed transition system A run of the transition system T A starts with some configuration (ℓ, ν, u 0 ) where ℓ ∈ L, ν ∈ (R + ) X and u 0 ∈ R. We do not explicitly specify initial configuration in our definition of priced timed automaton.
Cost-optimal reachability problem Let A be a priced timed automaton. Given two locations ℓ, ℓ ′ of A, the optimal cost OptCost(ℓ, ℓ ′ ), of reaching ℓ ′ from ℓ is defined as Given priced timed automaton A , locations ℓ, ℓ ′ , and a budget B ∈ R the cost-optimal reachability problem is to decide whether OptCost(ℓ, ℓ ′ ) ≤ B.
Summary of Our Results. Our first result (Section 3) is that the optimal cost reachability problem for general priced timed automata is undecidable.

Theorem 2.1 Cost-optimal reachability problem for nonlinearly priced timed automata is undecidable.
Given this negative result it is justifiable to look for various restricted subclasses of price functions in order to recover decidable variants. The first subclass that we consider is piece-wise linear price functions. A piecewise linear price function f : R + →R can be represented as tuple . . , p n is an increasing sequence of n-points in time. First point p 1 is always at time value zero. Thus, p 1 (= 0) < p 2 < . . . < p n holds.
• Y ℓ P = y p 1 , y p 2 , . . . , y p n is a sequence of prices such that is a sequence of n tuples. Time intervals formed by points in P ℓ are I 1 def = (p 1 , p 2 ), · · · , I n def = (p n , +∞). Again let I = I 1 , . . . , I n be the sequence of intervals. Value of piecewise linear price function f ℓ in the interval I k is given by We call tuple (P ℓ ,Y ℓ P ,Y ℓ I ) as structure of function f . We call a timed automaton is piecewise linearly priced if for all configuration (ℓ, ν) we have that π((ℓ, ν), , is a piecewise linear function defined over interval [0, +∞) and all the constants appearing in its structure are integers. Observe that the standard definition of linearly priced timed automata can be casted as a special case of piecewise linearly priced timed automata such that f ℓ = (P ℓ ,Y ℓ P ,Y ℓ I ), where P ℓ = 0 , Y ℓ P = 0 , and Y ℓ I = (k ℓ , 0) such that k ℓ is rate of change of price at location ℓ. For LPTA the cost-optimal reachability problem is known to be PSPACE-complete [8]. In Section 4 we show the following key result of piecewise linearly priced timed automata.

Theorem 2.2 The cost-optimal reachability problem for piecewise linearly priced timed automaton is PSPACE-complete.
This result can easily be extended to piecewise-concave priced timed automata [18].
We also study more general Lipschitz continuously priced timed automata. We say that a function

timed automaton is then called
Lipschitz continuous priced if price functions π((ℓ, ν), τ) = f ℓ (τ), are Lipschitz continuous for every location ℓ and there exists a constant T such that all the clock valuations are bounded from above by T . For this class of functions the optimal reachability problem may not be computable due to optimal occurring at non-rational points. For this reason we study the following approximate optimal problem. ε-Cost-optimal reachability problem Let A be a priced timed automaton. Given ε > 0 and two locations ℓ, ℓ ′ of A , a budget B ∈ R + , the ε-optimal cost problem is to decide whether OptCost(ℓ, ℓ ′ ) ≤ B + ε.
We show in Section 4 the following result for Lipschitz-continuous priced timed automata.

Theorem 2.3
The ε-Cost-optimal reachability is decidable for Lipschitz-continuous priced timed automata.
Finally, in Section 5 we give details of our implementation to solve step-bounded cost-optimal reachability problem for general priced timed automata.

Undecidability
This section is devoted to the proof of Theorem 2.1. We prove this result by reducing the halting problem for two counter machines to the cost-optimal reachability problem for priced timed automata. A two-counter machine M is a tuple (L,C) where L = {ℓ 0 , ℓ 1 , . . . , ℓ n } is the set of instructions including a distinguished terminal instruction ℓ n called HALT, and the set C = {c 1 , c 2 } of two counters. The instructions L are of the type: A configuration of a two-counter machine is a tuple (ℓ, c, d) where ℓ ∈ L is an instruction, and c, d ∈ N is the value of counters c 1 and c 2 , resp. A run of a two-counter machine is a (finite or infinite) sequence of configurations k 0 , k 1 , . . . where k 0 = (ℓ 0 , 0, 0) and the relation between subsequent configurations is governed by transitions between respective instructions. The halting problem for a two-counter machine asks whether its unique run ends at the terminal instruction ℓ n . The halting problem for two-counter machines is known [20] to be undecidable.
Proof of Theorem 2. 1 We reduce the reachability problem of two counter machines to an instance of the cost-optimal reachability problem OptCost(q, q ′ ) for priced timed automata A such that desired configuration of two counter machine is reachable from its initial configuration iff there is a run in the automaton A from q to q ′ of cost exactly zero.
Let M be the instance of the two counter machine having counters c and d. We construct a PTA A from M using suitable encoding. Valid runs of M are mapped to valid runs of A such that their cost is exactly zero. Figure 1 and 2 describes the module simulating counter decrement instruction of M . PTA A is constructed by composing the various modules. A uses four clocks -x, y, w and z, out of which x and y encode counters c and d as x = 1 − 1 2 c and y = 1 − 1 2 d . Let enc(·) denote this encoding function. Testing whether c is zero amounts to testing x is zero in the guards of A . Figure 1 describes decrement operation on counter c. It shows clock valuations before entering the module and after exiting the module when simulation is correct. Let t be the amount of time spent in location l 0 during simulation. Let (x, y, z, w) = (1 − 1 2 c , 1 − 1 2 d , 0, 0) be the configuration on entering l 0 . We want to ensure that the time spent at l 0 is t = 1 2 c−1 . The self loop at l 0 ensures that the value of y never crosses 1. If so, the new values of x, y, z, w respectively are 0, Observe that after every increment or decrement operation, the value of clock x moves to clock w. Hence, in order to composing A from individual modules we need to swap the roles of clocks x and w in every alternate modules. Let c 1 , d 1 be initial configuration and c 2 , d 2 be target configuration of M . They map to clock valuation ν 1 = (enc(c 1 ), enc(d 1 ), 0, 0) and ν 2 = (enc(c 2 ), enc(d 2 ), 0, 0) respectively. To make ν 1 and ν 2 separate locations, we can scale all constants ν 1 , ν 2 and A so as to make clock values in ν 1 and ν 2 integers. The construction is now complete.

Decidable Subclasses
Priced Timed Bisimulations. Let A and B be timed automata with their timed transition systems S A and S B . Let Q A and Q B respective sets of configurations. A binary symmetric relation R over Q A × Q B is a strong timed bisimulation relation iff for all a ∈ (R + ∪ 2 X ) • if q 1 a − → q ′ 1 and q 1 Rq 2 then there exists transition q 2 a − → q ′ 2 such that q ′ 1 Rq ′ 2 • conversely, if q 2 a − → q ′ 2 and q 1 Rq 2 then there exists transition q 1 a − → q ′ 1 such that q ′ 1 Rq ′ 2 , where q 1 , q ′ 1 ∈ Q A and q 2 , q ′ 2 ∈ Q B . The relation R is strong timed bisimilarity or strong timed bisimulation equivalence if it is the largest strong timed bisimulation relation such that R ⊆ Q A × Q B . Timed automata A and B are strong timed bisimilar if there exists such R.
Let A and B be priced timed automata with their priced timed transition systems T A and T B . Let P A and P B be respective sets of priced configurations. A strong timed bisimilarity ∼ is said to price preserving if for every a ∈ (R + ∪ 2 X ) As the choice of initial credit is arbitrary and the cost of a run does not depend on the value of initial credit, we claim following lemma.

Lemma 4.2 Let
A and B be two priced timed automata with price preserving timed bisimilarity ∼. Then following statements are true.

Proof of Theorem 2.2 Lemma 4.3 For every piecewise linearly priced timed automaton (PwLPTA), there exists linearly priced timed automaton with price preserving strong bisimulation between them.
Proof We prove this lemma by constructing LPTA explicitly from a given PwLPTA. Rest of this section explains construction and lemma 4.4 proves its correctness.

Construction of LPTA Let
from PwLPTA A as follows: • Let ℓ ∈ L A be some location of A . Delay price function for location ℓ, π A (ℓ, τ) = f ℓ (τ), is piecewise linear with respect to τ. f ℓ is given by integer restricted structure (P ℓ ,Y ℓ P ,Y ℓ I ), where -P ℓ = p 1 = 0, p 2 , . . . , p n -Y ℓ P = y p 1 , y p 2 , . . . , y p n -Y ℓ I = (m 1 , c 1 ), (m 2 , c 2 ), . . . , (m n , c n ) with the following interval sequence We associate each p i ∈ P ℓ and each I j ∈ I with locations of L B . This association is captured by mapping α ℓ such that α ℓ (p i ) = ℓ p i and α ℓ (I j ) = ℓ (p j , p j+1 ) . Here, ℓ p i and ℓ (p j , p j+1 ) are the names of locations of B. We define another mapping β ℓ (I j ) which returns j th entry in the sequence Y ℓ I . This mapping is useful for retrieving parameters of delay cost function in the interval I j .
• We add one extra clock named x to B. Thus, X B := X A ∪ {x}. This clock measures time spent at every location of A . Whenever a run enters any location of A , x is reset to zero.
• An edge e = (l, ϕ, λ , l ′ ) ∈ E B iff there is an edge e ′ = (ℓ, χ, ξ , ℓ ′ ) ∈ E A such that Let ℓ and m be locations of A and B respectively. We define following relation between ℓ and m,

Lemma 4.4 ϒ is price preserving timed bisimilarity.
Proof Let A = (L A , X A , E A , I A , π A , ψ A ) be a PwLPTA and B = (L B , X B , E B , I B , π B , ψ B ) be LPTA constructed from A using above construction.
If part: Let t be delay and λ be set of clocks to be reset in A . Now consider following transition . Now we try to find simulating transition in B under relation ϒ. We claim its (l 2 , ν 1 : 0, u 1 ) To hold this claim, we choose l 2 ∈ L B such that delay t matches with expected interval of l 2 . If t = p i for some i then l 2 = α l 1 (p i ). Otherwise t will match with some interval I j . So l 2 = α l 1 (I j ). Thus, (l 1 , l 2 ) ∈ ϒ holds. To place edge in B, construction mandates (l ′ 1 , l ′ 2 ) ∈ ϒ. Also the clocks in X A change identically. Now, let's verify that prices are preserved. For the case where t = p i , (u ′ 1 − u 1 ) = y p i + ψ A ((l 1 , l 2 )). Verify that from construction yields same price difference. For the case where t = I j , location price matters. Verify that rates at l ′ 1 and l ′ 2 are the same in the construction. Price change (u ′ 1 − u 1 ) = m j · t + c j + ψ A ((l 1 , l 2 )). Price offset c j is added to edge cost in the construction. Thus prices are preserved.
Proof of Theorem 2.2 PSPACE-hardness follows from the fact that LPTA are nothing but PwLPTA with single piece and their cost-optimal reachability is PSPACE-complete. We now explain a PSPACE algorithm for solving cost-optimal reachability for PwLPTA. We construct LPTA B for given piecewise linearly priced timed automaton A and solve cost-optimal reachability on B. Construction yields priced timed bisimilarity ϒ. Using

Proof of Theorem 2.3
Before we sketch a proof of Theorem 2.3, we introduce the concept of iterative approximation for nonlinear price functions.

Lemma 4.5 OptCost
Now we are in position to sketch the proof of Theorem 2.3. . Figure 3 shows calculation of these bounds for a Lipschitz continuous function. More precisely, for every t ∈ [x, y], Assume that f is a rational function. We will first prove decidability of ε-optimal cost reachability problem using this assumption. Later we will drop this assumption. We now construct two piecewise linear price functions f l and f u such that f l (t) ≤ f (t) ≤ f u (t) holds for 0 ≤ t ≤ T . Let T ∈ R + is a constant such that all clock valuations are bounded above by T .
Let δ ∈ Q + , 0 < δ ≤ T be the sampling period. Choice for the value of δ is explained at the end of the proof. We sample f at periodic intervals of δ in the interval 0 ≤ t ≤ T . We define a piecewise linear functions Let A be priced timed automaton with Lipschitz continuous price functions at all locations. We construct automata A l and A u by replacing price function at every location while keeping everything else unchanged. Specifically, if price function at location ℓ in A is π (ℓ) = f , then in A l , price at location ℓ is π (ℓ) l = f l . Likewise we assign price π (ℓ) u = f u to location ℓ of A u . Observe that A l and A u are replicas of A except the difference in location price functions. Since, π (ℓ) follows. Now, for any single delay transition, sup{ π (ℓ) graph, then sup{ OptCost A l (ℓ, ℓ ′ ) − OptCost A u (ℓ, ℓ ′ ) } = ε ≤ DKδ . This gives us the bound on ε. We choose δ = DK ε . In the above construction f is evaluated only at sampling points. We can safely drop the rationality restriction of f by approximating it by rational function f ′ such that f − f ′ ≤ DKδ 2 .

Step-Bounded Cost-Optimal Reachability Problem
In this section we look into the following step-bounded cost-optimal reachability problem for priced timed automata.
Step-Bounded Cost-optimal reachability problem Let A be a priced timed automaton. Given two locations ℓ, ℓ ′ of A, step bound N ∈ N, the step-bounded optimal cost OptCost N (ℓ, ℓ ′ ), is defined as where Runs N (ℓ, ℓ ′ ) are the set of canonical runs between ℓ and ℓ ′ of length less than or equal to N. Given priced timed automaton A , locations ℓ, ℓ ′ , and a budget B ∈ R + the step-bounded cost-optimal reachability problem is to decide whether OptCost N (ℓ, ℓ ′ ) ≤ B.
In this section we extend the encoding of Audemard, Cimatti, Kornilowicz, and Sebastiani [5] to solve step-bounded optimal-cost reachability problem for priced timed automata. After generating the encoding, we can feed it to SMT solver that support the theory corresponding to the price functions to solve the step-bounded cost-optimal reachability problem.

Audemard-Cimatti-Kornilowicz-Sebastiani Encoding for PTA
Let A 1 , A 2 , . . . A n be the priced timed automata which are composed into network of automata A . These automata communicate using channels. Let η be the set of channels used in A . If c is a channel, then c! is send operation on the channel c and c? is the blocking receive operation on the channel c.
Original Encoding for Timed Automata. We generate SMT formula for each automata using encoding from Audemard et. al. [5]. As per their scheme, we create one real variable for every clock and create separate one for an extra variable named z, which keeps the track of global time. We add a variable named s of type bitvector at every step which denotes current location. Notation s ℓ denotes assertion that current location is ℓ. We also create two binary variables for each channel per automaton -one for send and one for receive. For example, if automaton A 2 sends over channel c in current step, we set variable named A 2 .c!. This notation helps us to identify automaton which uses that channel in the current step and the type (send or receive) of an operation performed on that channel. We permit to use global clocks. While generating formula for A, it may happen that some of the automata share clock names or location names. For example, automata A 1 and A 2 may both have local clocks named y. But we must distinguish between variables that were created to hold value of y in A 1 and value of y in A 2 . We qualify all variables with name of automaton they are the part of. Here, we create real variables named A 1 .y and A 2 .y. All of these variables are created for every step of a run in a standard bounded-model-checking fashion. Assertions in Fig. 5.1 describe encoding at current and next step in the formula. We represent next step variables in primed version. For further details refer to [5]. Extension for Priced Timed Automata. Let A = (L, X , E, I, π, ψ) be priced timed automaton. To keep our encoding as general as possible, we describe our SMT formula generation for general priced timed automata. Observe that this class of automata subsume LPTA, concavely-priced PTA, piecewise-linear PTA, and Lipschitz-continuous priced PTA. For each automaton, we represent current accumulated price using real variable named price. We introduce variables price k at each step. Initially price 0 is set to zero as in 5. When switch transition occurs, we update the price using equation 6. The function ψ(T ) denotes edge price for the transition T . Equation 7 is used to specify prices for each delay transition. Quantity (z − z ′ ) is the delay incurred at current step and x is vector of current clock valuations. As price functions are location dependent, we add clause s ℓ to check whether current location is ℓ and then update price accordingly. For null transitions, prices at current and previous step are identical. To decide whether accumulated price at step n satisfies the condition price (n) ⋊ ⋉ k, where ⋊ ⋉ ∈ {<, ≤, >, ≥, =, =}, we add an assertion as per Eq. 9.

Experimental Results
We implemented the encoding discussed in the previous subsection as a vtool [1] for analyzing stepbounded optimal-cost for PTA. Out tool invokes state-of-the-art theorem prover Z3 [11] from Microsoft Research. It supports linear and non-linear arithmetic, bit-vectors, arrays, data-types, and quantifiers. For our purpose, Z3 can be used to solve price functions that are given as a polynomial of time-delay and the current valuation. Other non-linear price functions such as log, sin, cos, and exp can be accommodated in this framework using corresponding Taylor series approximations. In order to show experimental results, we concentrate the standard Airport Landing Scheduling Problem (ALP) from [7]. In order to give comparison with an existing tool we keep the price function linear and compare our tool with state-of-the-art optimal-cost reachability tool Uppaal-Cora [2]. Airport Landing Scheduling Problem. Given number of airplanes each with attributes like type of airplane, landing time window and number of runways, assign a landing time and runways to each airplane such that all airplanes land within their specific landing time window and also comply with safety regulations like mandatory wake turbulence separation delay. There are two possible sources of costs. If airplane travels faster than its designated speed, it lands earlier but consumes more fuel. If airplane landing is delayed, it suffers fuel costs for circling over the airport.
ALP is known to suffer exponential blowup with increasing runways [7]. We used the instances of ALP problem which are distributed with Uppaal CORA demo version. We asked whether there is a schedule such that all airplanes land and total cost is bounded from above by a fixed budget (800). Table 1 shows the results of our experiments. We ran all our experiments on 64-bit Intel R Xeon R CPU E5-2660 v2 running at 2.20GHz with 64 GB RAM. We fixed time limit to 30 minutes for each problem and used single threaded Z3 SMT solver (v 4.3.2).


SHARING ON WEB 3D MODELS OF ANCIENT THEATRES. A METHODOLOGICAL WORKFLOW

In the last few years, the need to share on the Web the knowledge of Cultural Heritage (CH) through navigable 3D models has increased. This need requires the availability of Web-based virtual reality systems and 3D WEBGIS. In order to make the information available to all stakeholders, these instruments should be powerful and at the same time very user-friendly. However, research and experiments carried out so far show that a standardized methodology doesn’t exist. All this is due both to complexity and dimensions of geometric models to be published, on the one hand, and to excessive costs of hardware and software tools, on the other. In light of this background, the paper describes a methodological approach for creating 3D models of CH, freely exportable on the Web, based on HTML5 and free and open source software. HTML5, supporting the WebGL standard, allows the exploration of 3D spatial models using most used Web browsers like Chrome, Firefox, Safari, Internet Explorer. The methodological workflow here described has been tested for the construction of a multimedia geo-spatial platform developed for three-dimensional exploration and documentation of the ancient theatres of Segesta and of Carthage, and the surrounding landscapes. The experimental application has allowed us to explore the potential and limitations of sharing on the Web of 3D CH models based on WebGL standard. Sharing capabilities could be extended defining suitable geospatial Web-services based on capabilities of HTML5 and WebGL technology.

INTRODUCTION
The definition of detailed 3D models and the development of Web-based virtual reality systems represent a significant value added for protection and promotion of Cultural Heritage (CH). In this context, recent advances within Information and Communication Technology (ICT) sector have allowed the development of new methods and technologies for sharing and browsing via the Web of 3D models of CH (Guarnieri et al., 2010;Gruen, 2013;Herrmann and Pastorelli, 2014). Particularly, new methods, procedures and technologies have been proposed for the construction of Web-based applications for interactive exploration of three-dimensional models, through the integration of geometrical and semantic information into an interface (Manferdini and Remondino, 2010). Principal aim is to provide users of a new exploration experience of 3D multimedia model of CH. In this perspective, the Web represents the ideal mean for accessing information, managing documentation and dissemination of CH values (Di Benedetto et al, 2014). All this is supported by the developments in visual computing that have opened new possibilities about documenting CH through the integration of geospatial data, graphical representations, multimedia contents and semantic metadata (Meyer et al., 2002;Noh et al., 2009;Remondino and Rizzi, 2010;Scianna and Sciortino, 2013;Gomes et al. 2014;Siotto et al., 2014). Beside the possibility of creating high-detailed models, the central question that arises is how to make these threedimensional models accessible and usable by the community (Di Benedetto et al., 2014). This last one is extensive as different types of multidisciplinary users with reduced (tourists) or high (scholars and researchers) technical knowledge are interested in CH. Indeed, the experience so far carried out highlights the difficulties involved into the identification of a proper methodological process. Today, on the base of technology available for Web, the definition of a more suitable method to publish detailed 3D models is possible with a reduction of costs of hardware and software tools. For this reason, more and more frequent are experimentations of CH interactive 3D models on the Web using open source tools and free software (Guarnieri et al., 2010). In light of these premises, the paper illustrates an experimental framework defined to produce 3D CH information systems, shareable on the Web. In this case, in order to allow access to multimedia representation on the Web and high-quality visualization, a WebGL-based application has been realized. It is compliant with features of most recent Web standards and technologies also running on mobile platforms, WebGL is an emerging standard from Khronos Group for accelerated 3D graphics rendering for the Web that complements HTML5 standards (Marrin, 2011). This application allows to access directly to full 3D vector models, without the need to install plugins or other kinds of extensions on the clients. In order to test the validity of the method, a platform hosting the ancient theatres of Segesta (Italy) and Carthage (Tunisia), and their neighbouring landscapes has been built (webgis.gislab.unipa.it/Hologramme). The development of these study cases has highlighted capabilities and limitations of the proposed method for Web sharing of 3D vector heritage models. Emerging aspects are (I) synchronic and diachronic representation possibilities, (II) relationships between Level of Detail (LoD) of the model vs access speed to geospatial 3D information, (III) multi-resolution data integration. The remainder of this paper is organized as follows. Section II analyses issues and advances in sharing on Web CH 3D models. Section III presents the ancient theatres system and, particularly, describes the principal characteristics of Segesta and Carthage Theatres, on which the platform has been experimented. The methodological workflow is then presented in section IV. Finally, section V shows the results achieved and section VI draws the conclusions and open scenarios.

SHARING OF CULTURAL HERITAGE ON WEB
Publishing on the Web the knowledge acquired or available for CH is an effective way to promote it. To stimulate the interest of users, this knowledge could be structured in the form of multimedia contents (texts, drawings, maps, movies, 2D or 3D models), necessary also to correctly document the life cycle and features of CH. In this perspective, one of the best and very impressive ways to transfer knowledge on CH is to share on the Web navigable 3D models, integrated by semantic data and other multimedia contents. Usually, this operation requires accessing to a great amount of data, whose management could be very complex and transmission through the NET very slow. Until today, 3D models have been published on the Web using non-native Web technologies, like VRML ( Fig.1 -option a) or PDF3D ( Fig.1 -option c) and plugins running on Web Browsers. Beside, in the past, a method for sharing of 3D urban models based on 3D geospatial Web-services (3D WFS) ( Fig.1 -option b) has been studied. This method could be applied also for sharing on the Web 3D geometrical and semantic data of CH (Scianna, 2013a). It requires the existence of a proper Webserver, able to deploy 3D WFS (Web Feature Service) and WMS (Web Map Service). Besides, accessing of geospatial information through a browser requires installing on it a JAVA applet/plugin that convert 3D GML data made available by the 3D WFS running as java servlet on the server, in a format compliant with features of the browser and loaded applet/plugins. The benefit deriving from an infrastructure based on Web services, is the possibility to grant everyone the open access to data. This requires that the interface of the Web services is well defined and documented and guaranties that everyone can write an applet/plugin in order to transform information coming from Web services allowing visualization on internet browser. Besides, writing the models inside the geospatial database requires the availability of a dedicated graphic editor (i.e. Blender software and some scripts) that should allow storing the 3D model inside the geospatial database, according to predefined conceptual model (Scianna, 2013b). If for the built environment there exist different kinds of conceptual models like CityGML, GIANT, on the other side the proposition of a global conceptual model for the description and the building of CH has not been fully defined; this last aspect is a complex issue, especially considering archaeological remains. These ones are characterized by a very fragmented structure, hard to be described both on geometric and semantic point to view, so that the definition of a standard conceptual model always applicable is a complex task. This difficulty is also due to the necessary coexistence of representations characterized by very different scales, inside the same model and the same visualization. The complexity of the structure of CH models and their size can also represent a problem bordering to the big data sector. To date, doesn't exists a global standardized model applicable to all kinds of cultural goods like BIM for new constructions (Scianna et al., 2014), even if in the last few years some authors have been proposed extensions of BIM applicable to CH (Dore and Murphy, 2012). On the basis of what said before, the proposition of simple and more suitable ways to publish on the web 3D models is a relevant aspect; it is necessary to study both the building structure of CH and the most appropriate Web compliant method for sharing geospatial 3D information, in relationship with the specific CH to describe (Fig. 1). We think that a possible solution should take in account capabilities of HTML5 and related WebGL technology in order to build user-friendly, scalable and adaptable platforms ( Fig.1 option d). Indeed, the proposition of a model for sharing of CH 3D models should necessary take in account the best balance between the levels of structuring of the model, quality of visualization and access speed on the Web. For these reasons, the correct definition of different LoDs (connected with the discretization of each model in subcomponents) is fundamental. Besides, the Web sharing of CH models requires a careful study about the system usability, regarding the ways of access, the navigation speed, the characteristics of the interface and the quality of contents.

THE ANCIENT THEATRES OF SEGESTA AND CARTHAGE
Within the experimental framework here described, the possibilities for implementing 3D CH information system applied to Mediterranean ancient theatres system (Segesta (Italy) and Carthage (Tunisia)) and shareable on the Web has been explored, valuing also its capabilities and limitations ( see Fig. 2). The Theatre of Segesta ( Fig. 3) dates back to the middle of the Fourth or the Second Century BC and it is one of the most successful examples of theatrical architecture placed in the transition from type Greek to the Roman. Although the theatre was located in an Elima city 1 , it is hypothesized that it has assumed roles and functions typical of the theatres of the Greek cities. The Theatre of Segesta, partially excavated at the beginning of the last century and recently restored, is now part of the archaeological park of Segesta and today is regularly used for theatrical performances (Tusa, 1991). The roman theatre of Carthage ( Fig. 4), built in the Second Century BC in the north-east of the city, is an intermediate type between the Greek theatre, dug into the ground, and Roman, generally realized on an open ground. During the Fifth Century, the theatre was completely destroyed by Vandals and remained unused until the end of the Nineteenth Century. The architectural and cultural-historical importance of the Roman theatre of Carthage is related to its massive size, making it able to accommodate more than 10,000 spectators, and its peculiarities that make a real masterpiece of Roman architecture. Since 1964 the Roman theatre of Carthage welcomes the International Festival of Carthage thanks to which assumes a significant touristic, cultural, artistic and folkloristic value, of national and international level (Ros, 1996). In both two theatres, in the last period of their life, a multistorey scena was built closing the orchestra.

THE WORKFLOW
The application presented here allows the observation of the CH (the theatres) in its original configuration and in the present. Obviously, it is possible to present CH also in other intermediate stages of life. The methodological workflow for sharing on Web 3D models of ancient theatres is described in Figure 5. Survey is the first phase. Inside it, the collection of requirements represents a step of primary importance. Requirements attain to the content of the platform, the interface and the method of exploration, formulated according to expert and visitor needs. Another important step is the acquisition of bibliographical and archival documentation required to diachronic and synchronic description of Theatres of Segesta and Carthage, as emerged from the analysis of the user's needs. Activities carried out in subsequent phases can be synthetized in as follows: -definition of a conceptual scheme aimed to subdivide the building into categories -land surveys and restitutions -3D modelling -construction of WebGL visualization system -user interface construction -browsing on internet are detailed in the following subparagraphs. The global workflow, here applied to theatres, can be extended to other archaeological or historical objects. Besides WebGL technology could be applied in every other applications for sharing knowledge regarding CH and/or the environment. The acquisition of historical data is necessary not only to produce information to show users but also to define correct reconstructive hypotheses to be simulated with 3D models. This The International Archives of the Photogrammetry, Remote Sensing and Spatial Information Sciences, Volume XLI-B2, 2016 XXIII ISPRS Congress, 12-19 July 2016, Prague, Czech Republic phase usually requires the help of historical experts or archaeologists.
During knowledge acquisition, a global survey of the area is carried out, it is useful to acquire a rough geometric knowledge of the interested area. After the definition of conceptual schema, a detailed survey step is carried out. Survey operations must be calibrated respecting the LoDs required for construction of 3D models; generally, acquiring of data with different type of instruments is necessary, observing CH from different points of view and different distances. In order to guarantee the completeness of 3D models, during 3D reconstruction phase, the integration of data coming from different type of instruments is always necessary.
The definition of conceptual model depends on specific cultural object to be described. If an object or an artefact must be described without differentiating various components, the conceptual model is less important. In this case the object is structured as a geometric complex to be eventually connected to a description (linked to one external database record).
In our case, we refer to more complex models in which every object (building or monument) is composed by different parts according to a predefined level of detail requested.

Definition of the conceptual model
In our case, the definition of a conceptual model is mandatory and the model must fit the specific object. The conceptual model, described at chapter 4.1, has been defined for ancient theatres and their complementary parts. It (Fig. 6) allows to describe not only the theatre but also some simple services buildings like the scena. The section of the conceptual model describing the scena could be used for structuring other buildings present in an archaeological site. The architecture of the scena resembles that of a temple but with a different shape and a limited number of columns and lacking of other elements typical of temples. 3D modelling requires the discretization of buildings and surrounding environments (far and near landscape) into parts that represent architectural objects according to the requested LoD. Each building part can be connected to a block of semantic data (attributes) and must be stored inside the HTML file defining the WebGL environment. For the definition of the conceptual model, a decomposition hypothesis of ancient theatres into its traditional functional areas (scena, cavea, analemma, etc.) has been formulated. This decomposition is necessary to cope with the complexity of geometric models and to define semantic and geometric hierarchies. Elements composing theatres are grouped into "classes" differentiating each other by function. The decomposition is defined also according to Italian Central Institute for Cataloguing and Documentation (ICCD) standard, in order to make 3D models suitable for connection to standardized semantic information system (Fig. 6). Models of the two theatres consist of elements that are at different scales, often represented within the same scene with a different LoDs in relation with the aims of the visualization (Fig. 7) (for example, the statue of Apollo, the Theatre Carthage, and the surrounding landscape) (Fig. 8).
The different LoD of the objects depends on the central element of each single view or scene. The virtual immersive exploration requires the representation both of the theatre and of the surrounding landscape in order to allow users to explore the relationships between these two elements (buildings and landscape) but also to analyse changes over space and time. These aspects are particularly important in the case of the Greek cities, positioned for urban and defensive reasons, in panoramic points (Fig. 9).

Survey and data acquisition
The detailed survey phase represents a fundamental moment in the methodological workflow. The construction of a multiscale model, in which theatres and surrounding areas are represented at different LoDs, requires the execution of surveys based on a combined use of different instruments (laser scanners, cameras, GPS receivers, and drones/UAVs flying at different heights). The acquisition of data with different instruments allows building of a geometric and semantics databases, where each display mode requires specific representation scales for each different objects (Fig.  10). In this perspective, the application of the most appropriate method depends on the nature of objects, as well as the purpose of their acquisition (Guarnieri et al., 2004;Pavlidis et al., 2007;Gomes et al., 2014).

3D Modelling
In the test platform of this research, project attributes are stored inside a javascript module that encapsulates WebGL models. Functions necessary to extract data (the attributes of each building part) from a database like PostgreSQL are to be developed.

WebGL visualization
Main software components of HTML5/WebGL visualization system are Apache server, Three.js libraries and HTML files (inside which are contained all Javascripts). Three.js library is a comprehensive and powerful Javascript library for creating simple 3D environments as well as interactive 3D games. Three.js library represents the core of the WebGL system, which is realized in Javascript and that allows visualizing 3D environments, calling and setting many functions like controls, camera, scene, loader, etc. (Fig. 11). Actually, Three.min.js library has been used. It has same functionalities of Three.js library, but the .min library has all unnecessary characters removed in order to make the file size smaller so to preserve band width. Into the HTML file is possible to insert directly the far landscape and the 3D model. The far landscape consists in a big sphere that incorporates the 3D loaded model, and the lights of the environment. On the inner surface of the sphere is projected a 360° panoramic image of the site, in order to create an effective and at the same time an impressing representation of the far landscape (Fig. 12).

Figure 12. Structure of 3D environment
The 3D model, imported from Blender software, represents the main part of the environment. Particularly, the 3D model is composed by the theatre and the terrain close to it.

User interface construction
The introductory page of the platform contains a map of the Mediterranean area. In this map, there are links to the pages regarding ancient theatres of Sicily and Tunisia. Clicking on each geographic link, the system shows the main page of the corresponding theatre. In this page is possible to acquire knowledge about the history of the theatre and its architectural features, as well as to start interactive navigation of 3D models, today and in the past (Fig. 13). The interface of the interactive navigation system is created in order to give users the possibility of different kinds of navigation, using different interfaces, in order to make the experience as interesting as possible.
For every type of interface, there is a command description, in order to make the model more user-friendly. Moreover, the command controls for movement are very simple (Fig. 14).
The navigation inside the model takes place using mouse buttons or arrow keys of the keyboard.

RESULTS
The research work above described represents one of first examples of sharing on Web 3D geospatial data of archaeological Mediterranean theatres. It has been demonstrated that it is possible sharing on Web complex CH 3D models using simplified methods compliant with present Web visualization HTML5 and WebGL technologies and tools. Particularly, the experimentation here presented has allowed (I) to produce and test an environment for networking CH geospatial information that can be shared without use of additional plug-ins or applets, and in toto based on free and open source solutions; (II) to share, view and browse interactively ancient theatre 3D models; (III) to realize ancient theatres 3D models contextualized in their environment and surrounding landscape; (IV) to handle fully 3D multi-resolution datasets; (V) to start reflections about the right balance between LoD of the model and speed access to geospatial 3D information. This latter aspect is strictly linked to the typology of CH objects to model, to environmental context within they are inserted and to representation scale. The downloading time of .obj models depends on their size; the size of the texture has less influence on downloading time, while has great importance for the visualization of models on mobile devices. In this regard we can say that the system here presented has a good level of scalability. The navigation can be performed with different kinds of devices like desktop PCs, Tablets and smartphones.
Hardware limitations regard only ram of mobile devices (requiring a minimum of 2GB) and compatibility with WebGL implementation (that derives from the availability of OpenGL supported hardware). On the software side, almost all web browsers are HTML5 and WebGL compliant and 3D models are navigable using all operative systems like Windows, Linux, Mac and Android. Besides, a reduction of textures' resolution (related to the reduction of screen resolution) is necessary to extend the platform from desktop to mobile devices. In addition, the research work presented here is useful as experimental model for future developments related to the networking of 3D models of CH via Web services.

CONCLUSIONS AND OPEN SCENARIOS
browser as a function of visualization scale; (III) the division of textures of the model in quad in such a way that furthest elements prove less defined, and then with a lighter level of description; (IV) the definition of a specific format that allows further compression of data.