@article{bouyer-jlli-2011,
  author    = {Patricia Bouyer and
               Franck Cassez and
               Fran{\c{c}}ois Laroussinie},
  title     = {Timed Modal Logics for Real-Time Systems - Specification, Verification
               and Control},
  journal   = {Journal of Logic, Language and Information},
  volume    = {20},
  number    = {2},
  pages     = {169--203},
  year      = {2011},
  Type = {A - Journal},
  url       = {http://dx.doi.org/10.1007/s10849-010-9127-4},
  doi       = {10.1007/s10849-010-9127-4},
  timestamp = {Tue, 12 Apr 2011 09:14:59 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jolli/BouyerCL11},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  urlpaper = {papers/jlli-2011.pdf},
  category= {games},
  mywebpage = {timed},
  show = {},
  keywords = {logics, real-time, timed automata, timed games},
  abstract = {
  In this paper, a timed modal logic Lc is presented for the specification
and verification of real-time systems. Several important results for Lc are discussed.
First we address the model checking problem and we show that it is an EXPTIME-complete problem.
Secondly we consider expressiveness and we explain how to
express strong timed bisimilarity and how to build characteristic formulas for timed
automata. We also propose a compositional algorithm for Lc model checking. Finally
we consider several control problems for which Lc can be used to check controllability.
  }
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 2010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

{"_id":"iFD2mDmhrRuSdbHtX","bibbaseid":"bouyer-cassez-laroussinie-timedmodallogicsforrealtimesystemsspecificationverificationandcontrol-2011","author_short":["Bouyer, P.","Cassez, F.","Laroussinie, F."],"bibdata":{"bibtype":"article","type":"A - Journal","author":[{"firstnames":["Patricia"],"propositions":[],"lastnames":["Bouyer"],"suffixes":[]},{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["François"],"propositions":[],"lastnames":["Laroussinie"],"suffixes":[]}],"title":"Timed Modal Logics for Real-Time Systems - Specification, Verification and Control","journal":"Journal of Logic, Language and Information","volume":"20","number":"2","pages":"169–203","year":"2011","url":"http://dx.doi.org/10.1007/s10849-010-9127-4","doi":"10.1007/s10849-010-9127-4","timestamp":"Tue, 12 Apr 2011 09:14:59 +0200","biburl":"http://dblp.uni-trier.de/rec/bib/journals/jolli/BouyerCL11","bibsource":"dblp computer science bibliography, http://dblp.org","urlpaper":"papers/jlli-2011.pdf","category":"games","mywebpage":"timed","show":"","keywords":"logics, real-time, timed automata, timed games","abstract":"In this paper, a timed modal logic Lc is presented for the specification and verification of real-time systems. Several important results for Lc are discussed. First we address the model checking problem and we show that it is an EXPTIME-complete problem. Secondly we consider expressiveness and we explain how to express strong timed bisimilarity and how to build characteristic formulas for timed automata. We also propose a compositional algorithm for Lc model checking. Finally we consider several control problems for which Lc can be used to check controllability. ","bibtex":"@article{bouyer-jlli-2011,\n author = {Patricia Bouyer and\n Franck Cassez and\n Fran{\\c{c}}ois Laroussinie},\n title = {Timed Modal Logics for Real-Time Systems - Specification, Verification\n and Control},\n journal = {Journal of Logic, Language and Information},\n volume = {20},\n number = {2},\n pages = {169--203},\n year = {2011},\n Type = {A - Journal},\n url = {http://dx.doi.org/10.1007/s10849-010-9127-4},\n doi = {10.1007/s10849-010-9127-4},\n timestamp = {Tue, 12 Apr 2011 09:14:59 +0200},\n biburl = {http://dblp.uni-trier.de/rec/bib/journals/jolli/BouyerCL11},\n bibsource = {dblp computer science bibliography, http://dblp.org},\n urlpaper = {papers/jlli-2011.pdf},\n category= {games},\n mywebpage = {timed},\n show = {},\n keywords = {logics, real-time, timed automata, timed games},\n abstract = {\n In this paper, a timed modal logic Lc is presented for the specification\nand verification of real-time systems. Several important results for Lc are discussed.\nFirst we address the model checking problem and we show that it is an EXPTIME-complete problem.\nSecondly we consider expressiveness and we explain how to\nexpress strong timed bisimilarity and how to build characteristic formulas for timed\nautomata. We also propose a compositional algorithm for Lc model checking. Finally\nwe consider several control problems for which Lc can be used to check controllability.\n }\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2010\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n","author_short":["Bouyer, P.","Cassez, F.","Laroussinie, F."],"key":"bouyer-jlli-2011","id":"bouyer-jlli-2011","bibbaseid":"bouyer-cassez-laroussinie-timedmodallogicsforrealtimesystemsspecificationverificationandcontrol-2011","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/jlli-2011.pdf"},"keyword":["logics","real-time","timed automata","timed games"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"article","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":["logics","real-time","timed automata","timed games"],"search_terms":["timed","modal","logics","real","time","systems","specification","verification","control","bouyer","cassez","laroussinie"],"title":"Timed Modal Logics for Real-Time Systems - Specification, Verification and Control","year":2011}