@inproceedings{DBLP:conf/concur/BouyerCL05,
  author    = {Patricia Bouyer and
               Franck Cassez and
               Fran{\c{c}}ois Laroussinie},
  title     = {Modal Logics for Timed Control},
  booktitle = {{CONCUR} 2005 - Concurrency Theory, 16th International Conference,
               {CONCUR} 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings},
  pages     = {81--94},
  year      = {2005},
  crossref  = {DBLP:conf/concur/2005},
          Type = {B - International Conferences},

  urlpaper = {papers/modal-control-concur05.pdf},
  urlslides = {papers/slides-concur-05.pdf},
    url_link       = {http://dx.doi.org/10.1007/11539452_10},
  series    = {Lecture Notes in Computer Science},
  volume    = {3653},
  publisher = {Springer},
  doi       = {10.1007/11539452_10},
  abstract = {
Abstract. In this paper we use the timed modal logic Lnu to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (Lcont) of the logic Lnu with a new modality.
More precisely we define a fragment of Lnu, namely Ldet, such that any
control objective of Lnudet can be translated into a Lcont formula that
holds for the plant if and only if there is a controller that can enforce
the control objective.
We also show that the new modality of Lcont strictly increases the expressive power of Lnu
while model-checking of Lcont remains EXPTIME-complete.},
  keywords = {control, synthesis, logics},
}

{"_id":"AsPnPxQC8DfuYhg8K","bibbaseid":"bouyer-cassez-laroussinie-modallogicsfortimedcontrol-2005","author_short":["Bouyer, P.","Cassez, F.","Laroussinie, F."],"bibdata":{"bibtype":"inproceedings","type":"B - International Conferences","author":[{"firstnames":["Patricia"],"propositions":[],"lastnames":["Bouyer"],"suffixes":[]},{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["François"],"propositions":[],"lastnames":["Laroussinie"],"suffixes":[]}],"title":"Modal Logics for Timed Control","booktitle":"CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings","pages":"81–94","year":"2005","crossref":"DBLP:conf/concur/2005","urlpaper":"papers/modal-control-concur05.pdf","urlslides":"papers/slides-concur-05.pdf","url_link":"http://dx.doi.org/10.1007/11539452_10","series":"Lecture Notes in Computer Science","volume":"3653","publisher":"Springer","doi":"10.1007/11539452_10","abstract":"Abstract. In this paper we use the timed modal logic Lnu to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (Lcont) of the logic Lnu with a new modality. More precisely we define a fragment of Lnu, namely Ldet, such that any control objective of Lnudet can be translated into a Lcont formula that holds for the plant if and only if there is a controller that can enforce the control objective. We also show that the new modality of Lcont strictly increases the expressive power of Lnu while model-checking of Lcont remains EXPTIME-complete.","keywords":"control, synthesis, logics","bibtex":"@inproceedings{DBLP:conf/concur/BouyerCL05,\n author = {Patricia Bouyer and\n Franck Cassez and\n Fran{\\c{c}}ois Laroussinie},\n title = {Modal Logics for Timed Control},\n booktitle = {{CONCUR} 2005 - Concurrency Theory, 16th International Conference,\n {CONCUR} 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings},\n pages = {81--94},\n year = {2005},\n crossref = {DBLP:conf/concur/2005},\n Type = {B - International Conferences},\n\n urlpaper = {papers/modal-control-concur05.pdf},\n urlslides = {papers/slides-concur-05.pdf},\n url_link = {http://dx.doi.org/10.1007/11539452_10},\n series = {Lecture Notes in Computer Science},\n volume = {3653},\n publisher = {Springer},\n doi = {10.1007/11539452_10},\n abstract = {\nAbstract. In this paper we use the timed modal logic Lnu to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (Lcont) of the logic Lnu with a new modality.\nMore precisely we define a fragment of Lnu, namely Ldet, such that any\ncontrol objective of Lnudet can be translated into a Lcont formula that\nholds for the plant if and only if there is a controller that can enforce\nthe control objective.\nWe also show that the new modality of Lcont strictly increases the expressive power of Lnu\nwhile model-checking of Lcont remains EXPTIME-complete.},\n keywords = {control, synthesis, logics},\n}\n\n","author_short":["Bouyer, P.","Cassez, F.","Laroussinie, F."],"key":"DBLP:conf/concur/BouyerCL05","id":"DBLP:conf/concur/BouyerCL05","bibbaseid":"bouyer-cassez-laroussinie-modallogicsfortimedcontrol-2005","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/modal-control-concur05.pdf","Slides":"http://science.mq.edu.au/~fcassez/bib/papers/slides-concur-05.pdf"," link":"http://dx.doi.org/10.1007/11539452_10"},"keyword":["control","synthesis","logics"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":["control","synthesis","logics"],"search_terms":["modal","logics","timed","control","bouyer","cassez","laroussinie"],"title":"Modal Logics for Timed Control","year":2005}