Synthesis of Optimal Strategies Using HyTech. Bouyer, P., Cassez, F., Fleury, E., & Larsen, K. G. Electr. Notes Theor. Comput. Sci. (Proceedings of GDV), 119(1):11–31, 2004.
Paper
Slides doi abstract bibtex Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. The problem of synthesizing an optimal winning strategy for a priced timed game under some hypotheses has been shown decidable in [P. Bouyer, F. Cassez, E. Fleury, and K.G. Larsen. Optimal strategies in priced timed game automata. Research Report BRICS RS-04-4, Denmark, Feb. 2004. Available at http://www.brics.dk/RS/04/4/]. In this paper, we present an algorithm for computing the optimal cost and for synthesizing an optimal strategy in case there exists one. We also describe the implementation of this algorithm with the tool HyTech and present an example.
@article{DBLP:journals/entcs/BouyerCFL05,
author = {Patricia Bouyer and
Franck Cassez and
Emmanuel Fleury and
Kim Guldstrand Larsen},
title = {Synthesis of Optimal Strategies Using HyTech},
journal = {Electr. Notes Theor. Comput. Sci. (Proceedings of GDV)},
volume = {119},
Type = {B - International Conferences},
number = {1},
pages = {11--31},
year = {2004},
url = {http://dx.doi.org/10.1016/j.entcs.2004.07.006},
urlslides = {papers/slides-gdv-04.pdf},
doi = {10.1016/j.entcs.2004.07.006},
abstract = {Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. The problem of synthesizing an optimal winning strategy for a priced timed game under some hypotheses has been shown decidable in [P. Bouyer, F. Cassez, E. Fleury, and K.G. Larsen. Optimal strategies in priced timed game automata. Research Report BRICS RS-04-4, Denmark, Feb. 2004. Available at http://www.brics.dk/RS/04/4/]. In this paper, we present an algorithm for computing the optimal cost and for synthesizing an optimal strategy in case there exists one. We also describe the implementation of this algorithm with the tool HyTech and present an example.},
keywords = {control, synthesis, priced timed games, optimal},
}