Affiliations: IMCS, Jan Długosz University in Częstochowa, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland. {b.wozna,agnieszka.zbrzezny,a.zbrzezny}@ajd.czest.pl
Correspondence:
[†]
Address for correspondence: IMCS, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland.
Note: [*] Partly supported by National Science Centre under the grant No. 2014/15/N/ST6/05079.
Abstract: We investigate a quasi-optimal cost reachability problem for weighted timed automata. We use a translation to the satisfiability modulo theories (SMT) problem 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 the 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 run is called k-quasi-optimal. We exemplify the use of our solution to the investigated problem by means of the weighted timed generic pipeline protocol and the weighted job shop scheduling problem, and we provide some preliminary experimental results.
