SAT-based searching for k-quasi-optimal runs in weighted timed automata

In the paper we are concerned with an optimal cost reachability problem for weighted timed automata, and we use a translation to SAT to solve the problem. In particular, we show how to find a run of length k ∈ IN that starts at the initial state and terminates at a state containing a target location, its total cost belongs to the interval [c,c+1), for some natural number c ∈ IN, and the cost of each other run of length k, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of runs is called k-quasi-optimal. We exemplify the use of our solution to the mentioned problem by means of the air traffic control problem, and we provide some preliminary experimental results.