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

• Autorzy: Woźna-Szcześniak B. , Zbrzezny A.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

SAT; timed automata; air traffic control problem; reachability problem

PL

SAT; automat czasowy; problem kontroli ruchu lotniczego; problem osiągalności

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2010
• Tom: Vol. 15
• Strony: 163--176
• Opis fizyczny: Bibliogr. 16 poz., rys., tab.

Twórcy

autor

Woźna-Szcześniak B.

• Institute of Mathematics and Computer Science Jan Długosz University of Częstochowa al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

autor

Zbrzezny A.

• Institute of Mathematics and Computer Science Jan Długosz University of Częstochowa al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• [1] R. Alur, C. Courcoubetis, T. Henzinger. Computing accumulated delays in real-time systems. Formal Methods in System Design, 11 (2), 137-155, 1997.
• [2] R. Alur, D. Dill. A theory of Timed Automata. Theoretical Computer Science, 126 (2), 183-235, 1994.
• [3] R. Alur, S. La Torre, G. J. Pappas. Optimal paths in weighted timed automata. Theoretical Computer Science, 318 (3), 297-322, 2004.
• [4] E. Asarin, O. Maler. As soon as possible: Time optimal control for timed automata. In: Proc. 2nd Int. Workshop on Hybrid Systems: Computation and Control,vol. 1569 of LNCS, pp. 19-30. Springer, 1999.
• [5] G. Behrmann, A. Fehnker, T.S. Hune, K. G. Larsen, P. Pettersson, J. M. T. Romijn, F.W. Vaandrager, F. W. Va, G. Behrmann, A. Fehnker, T. Hune, K. Larsen, P.Pettersson, J. Romijn. Minimum-cost reachability for priced timed automata. In: Proc. HSCC'01,vol. 2034 of LNCS, pp. 147-161. Springer, 2001.
• [6] A. Biere, A. Cimatti, E. Clarke, O. Strichman, Y. Zhu. Bounded model checking. In: Highly Dependable Software,vol. 58 of Advances in Computers. Academic Press, 2003. Pre-print.
• [7] P. Bouyer, T. Brihaye, V. Bruyère, J. Raskin. On the optimal reachability problem of weighted timed automata. Formal Methods System Design, 31 (2), 135-175, 2007.
• [8] P. Bouyer, E. Brinksma, K. G. Larsen. Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design, 32 (1), 3-23, 2008.
• [9] C. Courcoubetis, M. Yannakakis. Minimum and maximum delay problems in real-time systems. Formal Methods in System Design, 1 (4), 385-415, 1992.
• [10] Y. Kesten, A. Pnueli, J. Sifakis, S. Yovine. Decidable integration graphs. Information and Computation, 150 (2), 209-243, 1999.
• [11] K. G. Larsen, J. I. Rasmussen. Optimal reachability for multi-priced timed automata. Theoretical Computer Science, 390, 197-213, 2008.
• [12] P. Niebert, S. Tripakis, S. Yovine. Minimum-time reachability for Timed Automata. In: Proc. 8th IEEE Mediterranean Conf. on Control and Automation (MED'2000),Patros, Greece, July 2000.
• [13] W. Penczek, B. Woźna, A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fund. Informaticae, 51 (1-2), 135-156, 2002.
• [14] B. Woźna, A. Zbrzezny, W. Penczek. Checking reachability properties for Timed Automata via SAT. Fund. Informaticae, 55, 223-241, 2003.
• [15] A. Zbrzezny. SAT-based reachabilitychecking for timed automata with diagonal constraints. Fund. Informaticae, 67 (1-3), 303-322, 2005.
• [16] A. Zbrzezny. A boolean encoding of arithmetic operations. In: Proc. Int. Workshop on Concurrency, Specification and Programming, vol. 170 of Informatik-Berichte, pp. 536-547. Humboldt University, 2008.