Efficient On-the-Fly Algorithms for the Analysis of Timed Games. Cassez, F., David, A., Fleury, E., Larsen, K. G., & Lime, D. In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653, of Lecture Notes in Computer Science, pages 66–80, 2005. Springer.
Paper
Slides
Link doi abstract bibtex 1 download In this paper, we propose a first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. The algorithm we propose is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [15] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure. Various optimizations of the basic symbolic algorithm are proposed as well as methods for obtaining time-optimal winning strategies (for reachability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.
@inproceedings{DBLP:conf/concur/CassezDFLL05,
author = {Franck Cassez and
Alexandre David and
Emmanuel Fleury and
Kim Guldstrand Larsen and
Didier Lime},
title = {Efficient On-the-Fly Algorithms for the Analysis of Timed Games},
booktitle = {{CONCUR} 2005 - Concurrency Theory, 16th International Conference,
{CONCUR} 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings},
pages = {66--80},
year = {2005},
Type = {B - International Conferences},
series = {Lecture Notes in Computer Science},
volume = {3653},
publisher = {Springer},
urlpaper = {papers/efficient-control-concur05.pdf},
urlslides = {papers/efficient-control-concur05-slides.pdf},
url_link = {http://dx.doi.org/10.1007/11539452_9},
doi = {10.1007/11539452_9},
abstract = {In this paper, we propose a first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties.
The algorithm we propose is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [15] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure.
Various optimizations of the basic symbolic algorithm are proposed as well as methods for obtaining time-optimal winning strategies (for reachability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.},
keywords = {control, synthesis, timed games},
}
Downloads: 1
{"_id":"Y3qet65vyQicKmhyj","bibbaseid":"cassez-david-fleury-larsen-lime-efficientontheflyalgorithmsfortheanalysisoftimedgames-2005","author_short":["Cassez, F.","David, A.","Fleury, E.","Larsen, K. G.","Lime, D."],"bibdata":{"bibtype":"inproceedings","type":"B - International Conferences","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Alexandre"],"propositions":[],"lastnames":["David"],"suffixes":[]},{"firstnames":["Emmanuel"],"propositions":[],"lastnames":["Fleury"],"suffixes":[]},{"firstnames":["Kim","Guldstrand"],"propositions":[],"lastnames":["Larsen"],"suffixes":[]},{"firstnames":["Didier"],"propositions":[],"lastnames":["Lime"],"suffixes":[]}],"title":"Efficient On-the-Fly Algorithms for the Analysis of Timed Games","booktitle":"CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings","pages":"66–80","year":"2005","series":"Lecture Notes in Computer Science","volume":"3653","publisher":"Springer","urlpaper":"papers/efficient-control-concur05.pdf","urlslides":"papers/efficient-control-concur05-slides.pdf","url_link":"http://dx.doi.org/10.1007/11539452_9","doi":"10.1007/11539452_9","abstract":"In this paper, we propose a first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. The algorithm we propose is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [15] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure. Various optimizations of the basic symbolic algorithm are proposed as well as methods for obtaining time-optimal winning strategies (for reachability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.","keywords":"control, synthesis, timed games","bibtex":"@inproceedings{DBLP:conf/concur/CassezDFLL05,\n author = {Franck Cassez and\n Alexandre David and\n Emmanuel Fleury and\n Kim Guldstrand Larsen and\n Didier Lime},\n title = {Efficient On-the-Fly Algorithms for the Analysis of Timed Games},\n booktitle = {{CONCUR} 2005 - Concurrency Theory, 16th International Conference,\n {CONCUR} 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings},\n pages = {66--80},\n year = {2005},\n Type = {B - International Conferences},\n\n series = {Lecture Notes in Computer Science},\n volume = {3653},\n publisher = {Springer},\n urlpaper = {papers/efficient-control-concur05.pdf},\n urlslides = {papers/efficient-control-concur05-slides.pdf},\n url_link = {http://dx.doi.org/10.1007/11539452_9},\n doi = {10.1007/11539452_9},\n abstract = {In this paper, we propose a first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties.\nThe algorithm we propose is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [15] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure.\nVarious optimizations of the basic symbolic algorithm are proposed as well as methods for obtaining time-optimal winning strategies (for reachability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.},\n keywords = {control, synthesis, timed games},\n}\n\n","author_short":["Cassez, F.","David, A.","Fleury, E.","Larsen, K. G.","Lime, D."],"key":"DBLP:conf/concur/CassezDFLL05","id":"DBLP:conf/concur/CassezDFLL05","bibbaseid":"cassez-david-fleury-larsen-lime-efficientontheflyalgorithmsfortheanalysisoftimedgames-2005","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/efficient-control-concur05.pdf","Slides":"http://science.mq.edu.au/~fcassez/bib/papers/efficient-control-concur05-slides.pdf"," link":"http://dx.doi.org/10.1007/11539452_9"},"keyword":["control","synthesis","timed games"],"metadata":{"authorlinks":{}},"downloads":1},"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":["control","synthesis","timed games"],"search_terms":["efficient","fly","algorithms","analysis","timed","games","cassez","david","fleury","larsen","lime"],"title":"Efficient On-the-Fly Algorithms for the Analysis of Timed Games","year":2005,"downloads":1}