var bibbase_data = {"data":"<img src=\"//bibbase.org/img/ajax-loader.gif\" id=\"spinner\"\n  style=\"display: none;\" alt=\"Loading..\" />\n\n<div id=\"bibbase\">\n\n  <script type=\"text/javascript\">\n    var bibbase = {\n      params: {\"bib\":\"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib\",\"jsonp\":\"1\",\"filter\":\"mywebpage:timed\",\"css\":\"true\",\"host\":\"bibbase.org\"},\n      data: [{\"bibtype\":\"article\",\"type\":\"A - Journal\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Benattar\"],\"firstnames\":[\"Gilles\"],\"suffixes\":[]},{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Lime\"],\"firstnames\":[\"Didier\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Roux\"],\"firstnames\":[\"Olivier\",\"H.\"],\"suffixes\":[]}],\"title\":\"Control and Synthesis of Non-Interferent Timed Systems\",\"journal\":\"International Journal of Control\",\"volume\":\"88\",\"number\":\"2\",\"pages\":\"217–236\",\"year\":\"2015\",\"doi\":\"10.1080/00207179.2014.944356\",\"mywebpage\":\"timed\",\"urlpaper\":\"papers/ijc-2014.pdf\",\"ee\":\"http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full\",\"keywords\":\"security, non-interference\",\"category\":\"Non-interference\",\"abstract\":\"We focus on the control and the synthesis of secure timed systems which are modelled as timed automata. The security property that the system must satisfy is a non-interference property. Intuitively, non-interference ensures the absence of any causal dependency from a high-level domain to a lower level domain. Various notions of non-interference have been defined in the literature, and in this paper, we focus on strong non- deterministic non-interference (SNNI) and two (bi)simulation-based variants thereof (cosimulation-based SNNI and bisimulation-based SNNI). These properties and their extensions have been mostly studied in the context of discrete event systems, while it is now well-known that time is an important attack vector against secure systems. At the same time, there is an obvious interest in going beyond simple verification to control problems: to be able to automatically make systems secure. We consider non-interference properties in the challenging setting of control of dense-time systems specified by timed automata and we study the two following problems: (1) check whether it is possible to find a sub-system so that it is non- interferent; if yes, (2) compute a (largest) sub- system which is non- interferent. We exhibit decidable sub-classes for these problems, assess their theoretical complexities and provide effective algorithms based on the classical framework of timed games.\",\"bibtex\":\"@article{ijc-14,\\nauthor = {Benattar, Gilles and Franck Cassez and Lime, Didier\\nand Roux, Olivier H.},\\ntitle = {Control and Synthesis of Non-Interferent Timed\\nSystems},\\nType = {A - Journal},\\njournal = {International Journal of Control}, volume = {88}, number =\\n{2},\\npages = {217--236},\\nyear = {2015},\\ndoi = {10.1080/00207179.2014.944356},\\nmywebpage = {timed},\\nurlpaper = {papers/ijc-2014.pdf},\\nee = {http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full},\\nkeywords = {security, non-interference},\\ncategory = {Non-interference},\\nabstract = {We focus on the control and the\\nsynthesis of secure timed systems which are modelled as timed automata. The\\nsecurity property that the system must satisfy is a non-interference property.\\nIntuitively, non-interference ensures the absence of any causal dependency from\\na high-level domain to a lower level domain. Various notions of non-interference\\nhave been defined in the literature, and in this paper, we focus on strong non-\\ndeterministic non-interference (SNNI) and two (bi)simulation-based variants\\nthereof (cosimulation-based SNNI and bisimulation-based SNNI). These properties\\nand their extensions have been mostly studied in the context of discrete event\\nsystems, while it is now well-known that time is an important attack vector\\nagainst secure systems. At the same time, there is an obvious interest in going\\nbeyond simple verification to control problems: to be able to automatically make\\nsystems secure. We consider non-interference properties in the challenging\\nsetting of control of dense-time systems specified by timed automata and we\\nstudy the two following problems: (1) check whether it is possible to find a\\nsub-system so that it is non- interferent; if yes, (2) compute a (largest) sub-\\nsystem which is non- interferent. We exhibit decidable sub-classes for these\\nproblems, assess their theoretical complexities and provide effective algorithms\\nbased on the classical framework of timed games.}\\n}\\n\\n\\n\",\"author_short\":[\"Benattar, G.\",\"Cassez, F.\",\"Lime, D.\",\"Roux, O. H.\"],\"key\":\"ijc-14\",\"id\":\"ijc-14\",\"bibbaseid\":\"benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2015\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/ijc-2014.pdf\",\"Link\":\"http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full\"},\"keyword\":[\"security\",\"non-interference\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/timed-games.html\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Romain\"],\"propositions\":[],\"lastnames\":[\"Brenguier\"],\"suffixes\":[]},{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Jean-François\"],\"propositions\":[],\"lastnames\":[\"Raskin\"],\"suffixes\":[]}],\"title\":\"Energy and mean-payoff timed games\",\"booktitle\":\"17th International Conference on Hybrid Systems: Computation and Control, HSCC'14\",\"year\":\"2014\",\"pages\":\"283-292\",\"urlpaper\":\"papers/hscc-2014.pdf\",\"url_link\":\"http://doi.acm.org/10.1145/2562059.2562116\",\"mywebpage\":\"timed\",\"show\":\"\",\"keywords\":\"hybrid, timed automata, games\",\"abstract\":\"In this paper, we study energy and mean-payoff timed games. The decision problems that consist in determining the existence of winning strategies in those games are undecidable, and we thus provide semi-algorithms for solving these strategy synthesis problems. We then identify a large class of timed games for which our semi-algorithms terminate and are thus complete. We also study in detail the relation between mean-payoff and energy timed games. Finally, we provide a symbolic algorithm to solve energy timed games and demonstrate its use on small examples using HyTech.\",\"bibtex\":\"@inproceedings{hscc-14,\\n  author    = {Romain Brenguier and\\n               Franck Cassez and\\n               Jean-François Raskin},\\n  title     = {Energy and mean-payoff timed games},\\n  booktitle = {17th International Conference on Hybrid Systems: Computation\\n               and Control, HSCC'14},\\n  year      = {2014},\\n  pages     = {283-292},\\n  urlpaper = {papers/hscc-2014.pdf},\\n  url_link     = {http://doi.acm.org/10.1145/2562059.2562116},\\n  mywebpage = {timed},\\n  show = {},\\n  keywords = {hybrid, timed automata, games},\\n  abstract = {In this paper, we study energy and mean-payoff timed games.\\n  The decision problems that consist in determining the existence of winning strategies in those games are undecidable,\\n  and we thus provide semi-algorithms for solving these strategy synthesis problems.\\n  We then identify a large class of timed games for which our semi-algorithms terminate and are thus complete.\\n  We also study in detail the relation between mean-payoff and energy timed games. Finally,\\n  we provide a symbolic algorithm to solve energy timed games and demonstrate its use on small examples using HyTech.},\\n  Type = {B - International Conferences},\\n\\n}\\n\\n\",\"author_short\":[\"Brenguier, R.\",\"Cassez, F.\",\"Raskin, J.\"],\"key\":\"hscc-14\",\"id\":\"hscc-14\",\"bibbaseid\":\"brenguier-cassez-raskin-energyandmeanpayofftimedgames-2014\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/hscc-2014.pdf\",\" link\":\"http://doi.acm.org/10.1145/2562059.2562116\"},\"keyword\":[\"hybrid\",\"timed automata\",\"games\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/timed-games.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"A - Journal\",\"author\":[{\"firstnames\":[\"Béatrice\"],\"propositions\":[],\"lastnames\":[\"Bérard\"],\"suffixes\":[]},{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Serge\"],\"propositions\":[],\"lastnames\":[\"Haddad\"],\"suffixes\":[]},{\"firstnames\":[\"Didier\"],\"propositions\":[],\"lastnames\":[\"Lime\"],\"suffixes\":[]},{\"firstnames\":[\"Olivier\",\"H.\"],\"propositions\":[],\"lastnames\":[\"Roux\"],\"suffixes\":[]}],\"title\":\"The expressive power of time Petri nets\",\"journal\":\"Theoretical Computer Science\",\"volume\":\"474\",\"year\":\"2013\",\"pages\":\"1-20\",\"doi\":\"http://dx.doi.org/10.1016/j.tcs.2012.12.005\",\"bibsource\":\"DBLP, http://dblp.uni-trier.de\",\"category\":\"Timed Petri nets\",\"mywebpage\":\"timed\",\"keywords\":\"time petri nets, timed automata\",\"urlpaper\":\"papers/tcs-2013.pdf\",\"abstract\":\"We investigate expressiveness questions for time Petri nets (TPNs) and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs) as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs. We give a syntactical translation from bounded GTPNs to timed automata (TA) that generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly l ess expressive than TA w.r.t. weak timed bisimilarity. We prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance. Finally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs \\\"á la Merlin\\\" w.r.t. weak timed bisimilarity. These results provide a unified comparison of the expressiveness of many variants of timed models often used in practice. It leads to new important results for TPNs. Among them are: 1-safe TPNs and bounded-TPNs are equally expressive; $ε$-transitions strictly increase the expressive power of TPNs; self modifying nets as well as read, inhibitor and reset arcs do not add expressiveness to bounded TPNs. \",\"bibtex\":\"@article{tpn-13,\\n  author    = {Béatrice Bérard and\\n               Franck Cassez and\\n               Serge Haddad and\\n               Didier Lime and\\n               Olivier H. Roux},\\n  title     = {The expressive power of time {Petri} nets},\\n  journal   =  {Theoretical Computer Science},\\n  Type = {A - Journal},\\n  volume    = {474},\\n  year      = {2013},\\n  pages     = {1-20},\\n  doi        = {http://dx.doi.org/10.1016/j.tcs.2012.12.005},\\n  bibsource = {DBLP, http://dblp.uni-trier.de},\\n  category= {Timed Petri nets},\\n  mywebpage = {timed},\\n  keywords = {time petri nets, timed automata},\\n  urlpaper = {papers/tcs-2013.pdf},\\n  abstract = {We investigate expressiveness questions for time Petri nets (TPNs)\\n  and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs)\\n  as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs.\\nWe give a syntactical translation from bounded GTPNs to timed automata (TA)\\nthat generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly l\\ness expressive than TA w.r.t. weak timed bisimilarity.\\nWe prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance.\\nFinally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs \\\"á la Merlin\\\" w.r.t.\\nweak timed bisimilarity. These results provide a unified comparison of the expressiveness of\\nmany variants of timed models often used in practice. It leads to new important results for TPNs.\\nAmong them are: 1-safe TPNs and bounded-TPNs are equally expressive; $\\\\epsilon$-transitions strictly\\nincrease the expressive power of TPNs; self modifying nets as well as read,\\ninhibitor and reset arcs do not add expressiveness to bounded TPNs.\\n}\\n}\\n\\n\\n\",\"author_short\":[\"Bérard, B.\",\"Cassez, F.\",\"Haddad, S.\",\"Lime, D.\",\"Roux, O. H.\"],\"key\":\"tpn-13\",\"id\":\"tpn-13\",\"bibbaseid\":\"brard-cassez-haddad-lime-roux-theexpressivepoweroftimepetrinets-2013\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/tcs-2013.pdf\"},\"keyword\":[\"time petri nets\",\"timed automata\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/timed-games.html\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Peter\",\"E.\"],\"propositions\":[],\"lastnames\":[\"Bulychev\"],\"suffixes\":[]},{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Alexandre\"],\"propositions\":[],\"lastnames\":[\"David\"],\"suffixes\":[]},{\"firstnames\":[\"Kim\",\"Guldstrand\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"Jean-François\"],\"propositions\":[],\"lastnames\":[\"Raskin\"],\"suffixes\":[]},{\"firstnames\":[\"Pierre-Alain\"],\"propositions\":[],\"lastnames\":[\"Reynier\"],\"suffixes\":[]}],\"title\":\"Controllers with Minimal Observation Power (Application to Timed Systems)\",\"booktitle\":\"Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012\",\"year\":\"2012\",\"pages\":\"223-237\",\"urlpaper\":\"papers/atva-2012.pdf\",\"url_link\":\"http://dx.doi.org/10.1007/978-3-642-33386-6_19\",\"mywebpage\":\"timed\",\"keywords\":\"timed automata, timed games, control\",\"abstract\":\"We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies. \",\"bibtex\":\"@inproceedings{atva-12,\\n  author    = {Peter E. Bulychev and\\n               Franck Cassez and\\n               Alexandre David and\\n               Kim Guldstrand Larsen and\\n               Jean-François Raskin and\\n               Pierre-Alain Reynier},\\n  title     = {Controllers with Minimal Observation Power (Application\\n               to Timed Systems)},\\n  booktitle = {Automated Technology for Verification and Analysis - 10th\\n               International Symposium, ATVA 2012},\\n  year      = {2012},\\n  pages     = {223-237},\\n  urlpaper = {papers/atva-2012.pdf},\\n  url_link  = {http://dx.doi.org/10.1007/978-3-642-33386-6_19},\\n  mywebpage = {timed},\\n  keywords = {timed automata, timed games, control},\\n  abstract = {\\n  We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies.\\n  },\\n        Type = {B - International Conferences},\\n\\n}\\n\\n\",\"author_short\":[\"Bulychev, P. E.\",\"Cassez, F.\",\"David, A.\",\"Larsen, K. G.\",\"Raskin, J.\",\"Reynier, P.\"],\"key\":\"atva-12\",\"id\":\"atva-12\",\"bibbaseid\":\"bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/atva-2012.pdf\",\" link\":\"http://dx.doi.org/10.1007/978-3-642-33386-6_19\"},\"keyword\":[\"timed automata\",\"timed games\",\"control\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/timed-games.html\"}},\"downloads\":1,\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"E - Reports\",\"author\":[{\"firstnames\":[\"Peter\",\"E.\"],\"propositions\":[],\"lastnames\":[\"Bulychev\"],\"suffixes\":[]},{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Alexandre\"],\"propositions\":[],\"lastnames\":[\"David\"],\"suffixes\":[]},{\"firstnames\":[\"Kim\",\"G.\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"Jean-François\"],\"propositions\":[],\"lastnames\":[\"Raskin\"],\"suffixes\":[]},{\"firstnames\":[\"Pierre-Alain\"],\"propositions\":[],\"lastnames\":[\"Reynier\"],\"suffixes\":[]}],\"title\":\"Controllers with Minimal Observation Power (Application to Timed Systems)\",\"journal\":\"CoRR\",\"volume\":\"abs/1207.1276\",\"year\":\"2012\",\"urlpaper\":\"http://arxiv.org/abs/1207.1276\",\"timestamp\":\"Wed, 10 Oct 2012 21:28:54 +0200\",\"biburl\":\"http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1207-1276\",\"bibsource\":\"dblp computer science bibliography, http://dblp.org\",\"abstract\":\"We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies. \",\"mywebpage\":\"timed\",\"keywords\":\"timed automata, timed games, control\",\"bibtex\":\"@article{bulychev-2012,\\n  author    = {Peter E. Bulychev and\\n               Franck Cassez and\\n               Alexandre David and\\n               Kim G. Larsen and\\n               Jean{-}Fran{\\\\c{c}}ois Raskin and\\n               Pierre{-}Alain Reynier},\\n  title     = {Controllers with Minimal Observation Power (Application to Timed Systems)},\\n  journal   = {CoRR},\\n  Type = {E - Reports},\\n  volume    = {abs/1207.1276},\\n  year      = {2012},\\n  urlpaper       = {http://arxiv.org/abs/1207.1276},\\n  timestamp = {Wed, 10 Oct 2012 21:28:54 +0200},\\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1207-1276},\\n  bibsource = {dblp computer science bibliography, http://dblp.org},\\n  abstract = {\\n  We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies.\\n  },\\n   mywebpage = {timed},\\n  keywords = {timed automata, timed games, control},\\n\\n}\\n\\n\",\"author_short\":[\"Bulychev, P. E.\",\"Cassez, F.\",\"David, A.\",\"Larsen, K. G.\",\"Raskin, J.\",\"Reynier, P.\"],\"key\":\"bulychev-2012\",\"id\":\"bulychev-2012\",\"bibbaseid\":\"bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://arxiv.org/abs/1207.1276\"},\"keyword\":[\"timed automata\",\"timed games\",\"control\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/timed-games.html\"}},\"downloads\":1,\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"A - Journal\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]}],\"title\":\"The Complexity of Codiagnosability for Discrete Event and Timed Systems\",\"journal\":\"IEEE Trans. Automat. Contr.\",\"volume\":\"57\",\"number\":\"7\",\"year\":\"2012\",\"pages\":\"1752-1764\",\"urlpaper\":\"papers/tac-2012.pdf\",\"url_link\":\"http://dx.doi.org/10.1109/TAC.2012.2183169\",\"doi\":\"http://dx.doi.org/10.1109/TAC.2012.2183169\",\"mywebpage\":\"timed\",\"keywords\":\"timed automata, Fault diagnosis, Complexity\",\"abstract\":\"In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterisation of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterises diagosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. We then generalise the previous results to the case of dynamic observers. Finally we show that the codiagnosis problem for TA under bounded resources is 2EXPTIME-complete. \",\"bibtex\":\"@article{tac-12,\\n  author    = {Franck Cassez},\\n  title     = {The Complexity of Codiagnosability for Discrete Event and\\n               Timed Systems},\\n  journal   = {IEEE Trans. Automat. Contr.},\\n  volume    = {57},\\n  number    = {7},\\n  year      = {2012},\\n  type = {A - Journal},\\n  pages     = {1752-1764},\\n  urlpaper = {papers/tac-2012.pdf},\\n  url_link       = {http://dx.doi.org/10.1109/TAC.2012.2183169},\\n  doi = {http://dx.doi.org/10.1109/TAC.2012.2183169},\\n  mywebpage = {timed},\\n  keywords = {timed automata, Fault diagnosis, Complexity},\\n  abstract = {\\n  In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterisation of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterises diagosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. We then generalise the previous results to the case of dynamic observers. Finally we show that the codiagnosis problem for TA under bounded resources is 2EXPTIME-complete.\\n  }\\n}\\n\\n\",\"author_short\":[\"Cassez, F.\"],\"key\":\"tac-12\",\"id\":\"tac-12\",\"bibbaseid\":\"cassez-thecomplexityofcodiagnosabilityfordiscreteeventandtimedsystems-2012\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/tac-2012.pdf\",\" link\":\"http://dx.doi.org/10.1109/TAC.2012.2183169\"},\"keyword\":[\"timed automata\",\"Fault diagnosis\",\"Complexity\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/timed-games.html\"}},\"downloads\":1,\"html\":\"\"},{\"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\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/timed-games.html\"}},\"html\":\"\"}],\n      metadata: {\"owner\":\"cassez, f\",\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/timed-games.html\"}},\n      ownerID: \"vad5o6DekkjXAsn8y\"\n    };\n  </script>\n\n  <script type=\"text/javascript\">\n  var site$;\n  if (typeof $ != 'undefined') {\n    console.log('existing jquery: storing and then restoring');\n    site$ = $;\n    $ = null;\n  }\n  </script>\n\n  <script src=\"https://ajax.googleapis.com/ajax/libs/jquery/2.2.4/jquery.min.js\">\n  </script>\n  <script type=\"text/javascript\">\n  if (site$) {\n    console.log('existing jquery: avoiding conflict and restoring');\n    bb$ = $.noConflict(true);\n    $ = site$;\n  } else {\n    bb$ = $;\n  }\n  </script>\n\n  <script src=\"//bibbase.org/js/bibbase.min.js\"\n          type=\"text/javascript\">\n  </script>\n\n  <script type=\"text/javascript\"\n          src=\"https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML\">\n  </script>\n  <script type=\"text/x-mathjax-config\">\n    MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\\\(','\\\\)']]},\n                        skipTags: [\"body\"],\n                        processClass: \"bibbase_paper\"});\n  </script>\n\n  <style>\n  @media print {\n    .dontprint {\n        display: none !important;\n    }\n\n  .bibbase_group {\n    background-color: #E0E0E0;\n    font-style: italic;\n    font-size: larger;\n    text-shadow: 0px 0px 3px #FFFFFF;\n    border-radius: 4px 4px 4px 4px;\n    -moz-border-radius: 4px 4px 4px 4px;\n    -webkit-border-radius: 4px;\n    padding: 5px 40px 5px;\n    margin-top: 10px;\n    margin-bottom: 5px;\n    cursor: pointer;\n  }\n\n  .bibbase_paper {\n    margin-bottom: 5px;\n  }\n\n  }\n  </style>\n\n  \n  <div style=\"float: right; margin-right: 10px; margin-top: 10px; text-align: right; font-size: 12px\">\n    generated by\n    <a href=\"//bibbase.org\"\n       onclick=\"trackOutboundLink('bibbase', 'logo clicked', window.location.href, '//bibbase.org'); return false;\">\n      <img src=\"//bibbase.org/img/logo.svg\"\n           style=\"vertical-align: middle; margin-left: 3px; height: 16px;\"/\n           alt=\"bibbase.org\"\n           title=\"BibBase – The easiest way to maintain your publications page.\"\n        ></a>\n    \n  </div>\n  \n\n  <div id=\"bibbase_header\" class=\"dontprint\" style=\"\">\n\n    <ul class=\"nav nav-pills\" style=\"margin: 0px;\">\n\n      <li class=\"dropdown\" id=\"groupby_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\">\n          Group by\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li class=\"groupby year\"><a onclick=\"groupby('year')\">\n            Year</a>\n        </li>\n        <li class=\"groupby author\"><a onclick=\"groupby('author_short')\">\n            Author</a>\n        </li>\n        <li class=\"groupby type\"><a onclick=\"groupby('type')\">\n            Type</a>\n        </li>\n        <li class=\"groupby keyword\"><a onclick=\"groupby('keyword')\">\n            Keyword</a>\n        </li>\n        <li class=\"groupby downloads\"><a onclick=\"groupby('downloads')\">\n            Downloads</a>\n        </li>\n      </ul>\n      </li>\n\n\n      <li class=\"dropdown\" id=\"menu_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\" alt=\"controls\">\n          <i class=\"fa fa-reorder\" alt=\"controls\"></i>\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li>\n          <a onclick=\"toggleAll()\">\n            <i class=\"fa fa-chevron-down fa-fw\"></i> Expand/Collapse All\n          </a>\n        </li>\n        <li>\n          <a download=\"franck-bib.bib\" href=\"data:text/bibtex;base64,QGFydGljbGV7aWpjLTE0LAphdXRob3IgPSB7QmVuYXR0YXIsIEdpbGxlcyBhbmQgRnJhbmNrIENhc3NleiBhbmQgTGltZSwgRGlkaWVyCmFuZCBSb3V4LCBPbGl2aWVyIEgufSwKdGl0bGUgPSB7Q29udHJvbCBhbmQgU3ludGhlc2lzIG9mIE5vbi1JbnRlcmZlcmVudCBUaW1lZApTeXN0ZW1zfSwKVHlwZSA9IHtBIC0gSm91cm5hbH0sCmpvdXJuYWwgPSB7SW50ZXJuYXRpb25hbCBKb3VybmFsIG9mIENvbnRyb2x9LCB2b2x1bWUgPSB7ODh9LCBudW1iZXIgPQp7Mn0sCnBhZ2VzID0gezIxNy0tMjM2fSwKeWVhciA9IHsyMDE1fSwKZG9pID0gezEwLjEwODAvMDAyMDcxNzkuMjAxNC45NDQzNTZ9LApteXdlYnBhZ2UgPSB7dGltZWR9LAp1cmxwYXBlciA9IHtwYXBlcnMvaWpjLTIwMTQucGRmfSwKZWUgPSB7aHR0cDovL3d3dy50YW5kZm9ubGluZS5jb20vZXByaW50L2g3bklLeG5lZ01HUjVNN0VhZVNGL2Z1bGx9LAprZXl3b3JkcyA9IHtzZWN1cml0eSwgbm9uLWludGVyZmVyZW5jZX0sCmNhdGVnb3J5ID0ge05vbi1pbnRlcmZlcmVuY2V9LAphYnN0cmFjdCA9IHtXZSBmb2N1cyBvbiB0aGUgY29udHJvbCBhbmQgdGhlCnN5bnRoZXNpcyBvZiBzZWN1cmUgdGltZWQgc3lzdGVtcyB3aGljaCBhcmUgbW9kZWxsZWQgYXMgdGltZWQgYXV0b21hdGEuIFRoZQpzZWN1cml0eSBwcm9wZXJ0eSB0aGF0IHRoZSBzeXN0ZW0gbXVzdCBzYXRpc2Z5IGlzIGEgbm9uLWludGVyZmVyZW5jZSBwcm9wZXJ0eS4KSW50dWl0aXZlbHksIG5vbi1pbnRlcmZlcmVuY2UgZW5zdXJlcyB0aGUgYWJzZW5jZSBvZiBhbnkgY2F1c2FsIGRlcGVuZGVuY3kgZnJvbQphIGhpZ2gtbGV2ZWwgZG9tYWluIHRvIGEgbG93ZXIgbGV2ZWwgZG9tYWluLiBWYXJpb3VzIG5vdGlvbnMgb2Ygbm9uLWludGVyZmVyZW5jZQpoYXZlIGJlZW4gZGVmaW5lZCBpbiB0aGUgbGl0ZXJhdHVyZSwgYW5kIGluIHRoaXMgcGFwZXIsIHdlIGZvY3VzIG9uIHN0cm9uZyBub24tCmRldGVybWluaXN0aWMgbm9uLWludGVyZmVyZW5jZSAoU05OSSkgYW5kIHR3byAoYmkpc2ltdWxhdGlvbi1iYXNlZCB2YXJpYW50cwp0aGVyZW9mIChjb3NpbXVsYXRpb24tYmFzZWQgU05OSSBhbmQgYmlzaW11bGF0aW9uLWJhc2VkIFNOTkkpLiBUaGVzZSBwcm9wZXJ0aWVzCmFuZCB0aGVpciBleHRlbnNpb25zIGhhdmUgYmVlbiBtb3N0bHkgc3R1ZGllZCBpbiB0aGUgY29udGV4dCBvZiBkaXNjcmV0ZSBldmVudApzeXN0ZW1zLCB3aGlsZSBpdCBpcyBub3cgd2VsbC1rbm93biB0aGF0IHRpbWUgaXMgYW4gaW1wb3J0YW50IGF0dGFjayB2ZWN0b3IKYWdhaW5zdCBzZWN1cmUgc3lzdGVtcy4gQXQgdGhlIHNhbWUgdGltZSwgdGhlcmUgaXMgYW4gb2J2aW91cyBpbnRlcmVzdCBpbiBnb2luZwpiZXlvbmQgc2ltcGxlIHZlcmlmaWNhdGlvbiB0byBjb250cm9sIHByb2JsZW1zOiB0byBiZSBhYmxlIHRvIGF1dG9tYXRpY2FsbHkgbWFrZQpzeXN0ZW1zIHNlY3VyZS4gV2UgY29uc2lkZXIgbm9uLWludGVyZmVyZW5jZSBwcm9wZXJ0aWVzIGluIHRoZSBjaGFsbGVuZ2luZwpzZXR0aW5nIG9mIGNvbnRyb2wgb2YgZGVuc2UtdGltZSBzeXN0ZW1zIHNwZWNpZmllZCBieSB0aW1lZCBhdXRvbWF0YSBhbmQgd2UKc3R1ZHkgdGhlIHR3byBmb2xsb3dpbmcgcHJvYmxlbXM6ICgxKSBjaGVjayB3aGV0aGVyIGl0IGlzIHBvc3NpYmxlIHRvIGZpbmQgYQpzdWItc3lzdGVtIHNvIHRoYXQgaXQgaXMgbm9uLSBpbnRlcmZlcmVudDsgaWYgeWVzLCAoMikgY29tcHV0ZSBhIChsYXJnZXN0KSBzdWItCnN5c3RlbSB3aGljaCBpcyBub24tIGludGVyZmVyZW50LiBXZSBleGhpYml0IGRlY2lkYWJsZSBzdWItY2xhc3NlcyBmb3IgdGhlc2UKcHJvYmxlbXMsIGFzc2VzcyB0aGVpciB0aGVvcmV0aWNhbCBjb21wbGV4aXRpZXMgYW5kIHByb3ZpZGUgZWZmZWN0aXZlIGFsZ29yaXRobXMKYmFzZWQgb24gdGhlIGNsYXNzaWNhbCBmcmFtZXdvcmsgb2YgdGltZWQgZ2FtZXMufQp9CgoKCgpAaW5wcm9jZWVkaW5nc3toc2NjLTE0LAogIGF1dGhvciAgICA9IHtSb21haW4gQnJlbmd1aWVyIGFuZAogICAgICAgICAgICAgICBGcmFuY2sgQ2Fzc2V6IGFuZAogICAgICAgICAgICAgICBKZWFuLUZyYW7Dp29pcyBSYXNraW59LAogIHRpdGxlICAgICA9IHtFbmVyZ3kgYW5kIG1lYW4tcGF5b2ZmIHRpbWVkIGdhbWVzfSwKICBib29rdGl0bGUgPSB7MTd0aCBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2Ugb24gSHlicmlkIFN5c3RlbXM6IENvbXB1dGF0aW9uCiAgICAgICAgICAgICAgIGFuZCBDb250cm9sLCBIU0NDJzE0fSwKICB5ZWFyICAgICAgPSB7MjAxNH0sCiAgcGFnZXMgICAgID0gezI4My0yOTJ9LAogIHVybHBhcGVyID0ge3BhcGVycy9oc2NjLTIwMTQucGRmfSwKICB1cmxfbGluayAgICAgPSB7aHR0cDovL2RvaS5hY20ub3JnLzEwLjExNDUvMjU2MjA1OS4yNTYyMTE2fSwKICBteXdlYnBhZ2UgPSB7dGltZWR9LAogIHNob3cgPSB7fSwKICBrZXl3b3JkcyA9IHtoeWJyaWQsIHRpbWVkIGF1dG9tYXRhLCBnYW1lc30sCiAgYWJzdHJhY3QgPSB7SW4gdGhpcyBwYXBlciwgd2Ugc3R1ZHkgZW5lcmd5IGFuZCBtZWFuLXBheW9mZiB0aW1lZCBnYW1lcy4KICBUaGUgZGVjaXNpb24gcHJvYmxlbXMgdGhhdCBjb25zaXN0IGluIGRldGVybWluaW5nIHRoZSBleGlzdGVuY2Ugb2Ygd2lubmluZyBzdHJhdGVnaWVzIGluIHRob3NlIGdhbWVzIGFyZSB1bmRlY2lkYWJsZSwKICBhbmQgd2UgdGh1cyBwcm92aWRlIHNlbWktYWxnb3JpdGhtcyBmb3Igc29sdmluZyB0aGVzZSBzdHJhdGVneSBzeW50aGVzaXMgcHJvYmxlbXMuCiAgV2UgdGhlbiBpZGVudGlmeSBhIGxhcmdlIGNsYXNzIG9mIHRpbWVkIGdhbWVzIGZvciB3aGljaCBvdXIgc2VtaS1hbGdvcml0aG1zIHRlcm1pbmF0ZSBhbmQgYXJlIHRodXMgY29tcGxldGUuCiAgV2UgYWxzbyBzdHVkeSBpbiBkZXRhaWwgdGhlIHJlbGF0aW9uIGJldHdlZW4gbWVhbi1wYXlvZmYgYW5kIGVuZXJneSB0aW1lZCBnYW1lcy4gRmluYWxseSwKICB3ZSBwcm92aWRlIGEgc3ltYm9saWMgYWxnb3JpdGhtIHRvIHNvbHZlIGVuZXJneSB0aW1lZCBnYW1lcyBhbmQgZGVtb25zdHJhdGUgaXRzIHVzZSBvbiBzbWFsbCBleGFtcGxlcyB1c2luZyBIeVRlY2gufSwKICBUeXBlID0ge0IgLSBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2VzfSwKCn0KCgoKQGFydGljbGV7dHBuLTEzLAogIGF1dGhvciAgICA9IHtCw6lhdHJpY2UgQsOpcmFyZCBhbmQKICAgICAgICAgICAgICAgRnJhbmNrIENhc3NleiBhbmQKICAgICAgICAgICAgICAgU2VyZ2UgSGFkZGFkIGFuZAogICAgICAgICAgICAgICBEaWRpZXIgTGltZSBhbmQKICAgICAgICAgICAgICAgT2xpdmllciBILiBSb3V4fSwKICB0aXRsZSAgICAgPSB7VGhlIGV4cHJlc3NpdmUgcG93ZXIgb2YgdGltZSB7UGV0cml9IG5ldHN9LAogIGpvdXJuYWwgICA9ICB7VGhlb3JldGljYWwgQ29tcHV0ZXIgU2NpZW5jZX0sCiAgVHlwZSA9IHtBIC0gSm91cm5hbH0sCiAgdm9sdW1lICAgID0gezQ3NH0sCiAgeWVhciAgICAgID0gezIwMTN9LAogIHBhZ2VzICAgICA9IHsxLTIwfSwKICBkb2kgICAgICAgID0ge2h0dHA6Ly9keC5kb2kub3JnLzEwLjEwMTYvai50Y3MuMjAxMi4xMi4wMDV9LAogIGJpYnNvdXJjZSA9IHtEQkxQLCBodHRwOi8vZGJscC51bmktdHJpZXIuZGV9LAogIGNhdGVnb3J5PSB7VGltZWQgUGV0cmkgbmV0c30sCiAgbXl3ZWJwYWdlID0ge3RpbWVkfSwKICBrZXl3b3JkcyA9IHt0aW1lIHBldHJpIG5ldHMsIHRpbWVkIGF1dG9tYXRhfSwKICB1cmxwYXBlciA9IHtwYXBlcnMvdGNzLTIwMTMucGRmfSwKICBhYnN0cmFjdCA9IHtXZSBpbnZlc3RpZ2F0ZSBleHByZXNzaXZlbmVzcyBxdWVzdGlvbnMgZm9yIHRpbWUgUGV0cmkgbmV0cyAoVFBOcykKICBhbmQgc29tZSBvZiB0aGVpciBtb3N0IHVzZWZ1bCBleHRlbnNpb25zLiBXZSBmaXJzdCBpbnRyb2R1Y2UgZ2VuZXJhbGlzZWQgdGltZSBQZXRyaSBuZXRzIChHVFBOcykKICBhcyBhbiBhYnN0cmFjdCBtb2RlbCB0aGF0IGVuY29tcGFzc2VzIHZhcmlhbnRzIG9mIFRQTnMgc3VjaCBhcyBzZWxmIG1vZGlmaWNhdGlvbnMgYW5kIHJlYWQsIHJlc2V0IGFuZCBpbmhpYml0b3IgYXJjcy4KV2UgZ2l2ZSBhIHN5bnRhY3RpY2FsIHRyYW5zbGF0aW9uIGZyb20gYm91bmRlZCBHVFBOcyB0byB0aW1lZCBhdXRvbWF0YSAoVEEpCnRoYXQgZ2VuZXJhdGVzIGlzb21vcnBoaWMgdHJhbnNpdGlvbiBzeXN0ZW1zLiBXZSBwcm92ZSB0aGF0IHRoZSBjbGFzcyBvZiBib3VuZGVkIEdUUE5zIGlzIHN0cmljdGx5IGwKZXNzIGV4cHJlc3NpdmUgdGhhbiBUQSB3LnIudC4gd2VhayB0aW1lZCBiaXNpbWlsYXJpdHkuCldlIHByb3ZlIHRoYXQgYm91bmRlZCBHVFBOcywgYm91bmRlZCBUUE5zIGFuZCBUQSBhcmUgZXF1YWxseSBleHByZXNzaXZlIHcuci50LiB0aW1lZCBsYW5ndWFnZSBhY2NlcHRhbmNlLgpGaW5hbGx5LCB3ZSBjaGFyYWN0ZXJpc2UgYSBzeW50YWN0aWNhbCBzdWJjbGFzcyBvZiBUQSB0aGF0IGlzIGVxdWFsbHkgZXhwcmVzc2l2ZSB0byBib3VuZGVkIEdUUE5zICLDoSBsYSBNZXJsaW4iIHcuci50Lgp3ZWFrIHRpbWVkIGJpc2ltaWxhcml0eS4gVGhlc2UgcmVzdWx0cyBwcm92aWRlIGEgdW5pZmllZCBjb21wYXJpc29uIG9mIHRoZSBleHByZXNzaXZlbmVzcyBvZgptYW55IHZhcmlhbnRzIG9mIHRpbWVkIG1vZGVscyBvZnRlbiB1c2VkIGluIHByYWN0aWNlLiBJdCBsZWFkcyB0byBuZXcgaW1wb3J0YW50IHJlc3VsdHMgZm9yIFRQTnMuCkFtb25nIHRoZW0gYXJlOiAxLXNhZmUgVFBOcyBhbmQgYm91bmRlZC1UUE5zIGFyZSBlcXVhbGx5IGV4cHJlc3NpdmU7ICRcZXBzaWxvbiQtdHJhbnNpdGlvbnMgc3RyaWN0bHkKaW5jcmVhc2UgdGhlIGV4cHJlc3NpdmUgcG93ZXIgb2YgVFBOczsgc2VsZiBtb2RpZnlpbmcgbmV0cyBhcyB3ZWxsIGFzIHJlYWQsCmluaGliaXRvciBhbmQgcmVzZXQgYXJjcyBkbyBub3QgYWRkIGV4cHJlc3NpdmVuZXNzIHRvIGJvdW5kZWQgVFBOcy4KfQp9CgoKCgpAaW5wcm9jZWVkaW5nc3thdHZhLTEyLAogIGF1dGhvciAgICA9IHtQZXRlciBFLiBCdWx5Y2hldiBhbmQKICAgICAgICAgICAgICAgRnJhbmNrIENhc3NleiBhbmQKICAgICAgICAgICAgICAgQWxleGFuZHJlIERhdmlkIGFuZAogICAgICAgICAgICAgICBLaW0gR3VsZHN0cmFuZCBMYXJzZW4gYW5kCiAgICAgICAgICAgICAgIEplYW4tRnJhbsOnb2lzIFJhc2tpbiBhbmQKICAgICAgICAgICAgICAgUGllcnJlLUFsYWluIFJleW5pZXJ9LAogIHRpdGxlICAgICA9IHtDb250cm9sbGVycyB3aXRoIE1pbmltYWwgT2JzZXJ2YXRpb24gUG93ZXIgKEFwcGxpY2F0aW9uCiAgICAgICAgICAgICAgIHRvIFRpbWVkIFN5c3RlbXMpfSwKICBib29rdGl0bGUgPSB7QXV0b21hdGVkIFRlY2hub2xvZ3kgZm9yIFZlcmlmaWNhdGlvbiBhbmQgQW5hbHlzaXMgLSAxMHRoCiAgICAgICAgICAgICAgIEludGVybmF0aW9uYWwgU3ltcG9zaXVtLCBBVFZBIDIwMTJ9LAogIHllYXIgICAgICA9IHsyMDEyfSwKICBwYWdlcyAgICAgPSB7MjIzLTIzN30sCiAgdXJscGFwZXIgPSB7cGFwZXJzL2F0dmEtMjAxMi5wZGZ9LAogIHVybF9saW5rICA9IHtodHRwOi8vZHguZG9pLm9yZy8xMC4xMDA3Lzk3OC0zLTY0Mi0zMzM4Ni02XzE5fSwKICBteXdlYnBhZ2UgPSB7dGltZWR9LAogIGtleXdvcmRzID0ge3RpbWVkIGF1dG9tYXRhLCB0aW1lZCBnYW1lcywgY29udHJvbH0sCiAgYWJzdHJhY3QgPSB7CiAgV2UgY29uc2lkZXIgdGhlIHByb2JsZW0gb2YgY29udHJvbGxlciBzeW50aGVzaXMgdW5kZXIgaW1wZXJmZWN0IGluZm9ybWF0aW9uIGluIGEgc2V0dGluZyB3aGVyZSB0aGVyZSBpcyBhIHNldCBvZiBhdmFpbGFibGUgb2JzZXJ2YWJsZSBwcmVkaWNhdGVzIGVxdWlwcGVkIHdpdGggYSBjb3N0IGZ1bmN0aW9uLiBUaGUgcHJvYmxlbSB0aGF0IHdlIGFkZHJlc3MgaXMgdGhlIGNvbXB1dGF0aW9uIG9mIGEgc3Vic2V0IG9mIHByZWRpY2F0ZXMgc3VmZmljaWVudCBmb3IgY29udHJvbCBhbmQgd2hvc2UgY29zdCBpcyBtaW5pbWFsLiBPdXIgc29sdXRpb24gYXZvaWRzIGEgZnVsbCBleHBsb3JhdGlvbiBvZiBhbGwgcG9zc2libGUgc3Vic2V0cyBvZiBwcmVkaWNhdGVzIGFuZCByZXVzZXMgc29tZSBpbmZvcm1hdGlvbiBiZXR3ZWVuIGRpZmZlcmVudCBpdGVyYXRpb25zLiBXZSBhcHBseSBvdXIgYXBwcm9hY2ggdG8gdGltZWQgc3lzdGVtcy4gV2UgaGF2ZSBkZXZlbG9wZWQgYSB0b29sIHByb3RvdHlwZSBhbmQgYW5hbHl6ZSB0aGUgcGVyZm9ybWFuY2Ugb2Ygb3VyIG9wdGltaXphdGlvbiBhbGdvcml0aG0gb24gdHdvIGNhc2Ugc3R1ZGllcy4KICB9LAogICAgICAgIFR5cGUgPSB7QiAtIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZXN9LAoKfQoKCgpAYXJ0aWNsZXtidWx5Y2hldi0yMDEyLAogIGF1dGhvciAgICA9IHtQZXRlciBFLiBCdWx5Y2hldiBhbmQKICAgICAgICAgICAgICAgRnJhbmNrIENhc3NleiBhbmQKICAgICAgICAgICAgICAgQWxleGFuZHJlIERhdmlkIGFuZAogICAgICAgICAgICAgICBLaW0gRy4gTGFyc2VuIGFuZAogICAgICAgICAgICAgICBKZWFuey19RnJhbntcY3tjfX1vaXMgUmFza2luIGFuZAogICAgICAgICAgICAgICBQaWVycmV7LX1BbGFpbiBSZXluaWVyfSwKICB0aXRsZSAgICAgPSB7Q29udHJvbGxlcnMgd2l0aCBNaW5pbWFsIE9ic2VydmF0aW9uIFBvd2VyIChBcHBsaWNhdGlvbiB0byBUaW1lZCBTeXN0ZW1zKX0sCiAgam91cm5hbCAgID0ge0NvUlJ9LAogIFR5cGUgPSB7RSAtIFJlcG9ydHN9LAogIHZvbHVtZSAgICA9IHthYnMvMTIwNy4xMjc2fSwKICB5ZWFyICAgICAgPSB7MjAxMn0sCiAgdXJscGFwZXIgICAgICAgPSB7aHR0cDovL2FyeGl2Lm9yZy9hYnMvMTIwNy4xMjc2fSwKICB0aW1lc3RhbXAgPSB7V2VkLCAxMCBPY3QgMjAxMiAyMToyODo1NCArMDIwMH0sCiAgYmlidXJsICAgID0ge2h0dHA6Ly9kYmxwLnVuaS10cmllci5kZS9yZWMvYmliL2pvdXJuYWxzL2NvcnIvYWJzLTEyMDctMTI3Nn0sCiAgYmlic291cmNlID0ge2RibHAgY29tcHV0ZXIgc2NpZW5jZSBiaWJsaW9ncmFwaHksIGh0dHA6Ly9kYmxwLm9yZ30sCiAgYWJzdHJhY3QgPSB7CiAgV2UgY29uc2lkZXIgdGhlIHByb2JsZW0gb2YgY29udHJvbGxlciBzeW50aGVzaXMgdW5kZXIgaW1wZXJmZWN0IGluZm9ybWF0aW9uIGluIGEgc2V0dGluZyB3aGVyZSB0aGVyZSBpcyBhIHNldCBvZiBhdmFpbGFibGUgb2JzZXJ2YWJsZSBwcmVkaWNhdGVzIGVxdWlwcGVkIHdpdGggYSBjb3N0IGZ1bmN0aW9uLiBUaGUgcHJvYmxlbSB0aGF0IHdlIGFkZHJlc3MgaXMgdGhlIGNvbXB1dGF0aW9uIG9mIGEgc3Vic2V0IG9mIHByZWRpY2F0ZXMgc3VmZmljaWVudCBmb3IgY29udHJvbCBhbmQgd2hvc2UgY29zdCBpcyBtaW5pbWFsLiBPdXIgc29sdXRpb24gYXZvaWRzIGEgZnVsbCBleHBsb3JhdGlvbiBvZiBhbGwgcG9zc2libGUgc3Vic2V0cyBvZiBwcmVkaWNhdGVzIGFuZCByZXVzZXMgc29tZSBpbmZvcm1hdGlvbiBiZXR3ZWVuIGRpZmZlcmVudCBpdGVyYXRpb25zLiBXZSBhcHBseSBvdXIgYXBwcm9hY2ggdG8gdGltZWQgc3lzdGVtcy4gV2UgaGF2ZSBkZXZlbG9wZWQgYSB0b29sIHByb3RvdHlwZSBhbmQgYW5hbHl6ZSB0aGUgcGVyZm9ybWFuY2Ugb2Ygb3VyIG9wdGltaXphdGlvbiBhbGdvcml0aG0gb24gdHdvIGNhc2Ugc3R1ZGllcy4KICB9LAogICBteXdlYnBhZ2UgPSB7dGltZWR9LAogIGtleXdvcmRzID0ge3RpbWVkIGF1dG9tYXRhLCB0aW1lZCBnYW1lcywgY29udHJvbH0sCgp9CgoKCkBhcnRpY2xle3RhYy0xMiwKICBhdXRob3IgICAgPSB7RnJhbmNrIENhc3Nlen0sCiAgdGl0bGUgICAgID0ge1RoZSBDb21wbGV4aXR5IG9mIENvZGlhZ25vc2FiaWxpdHkgZm9yIERpc2NyZXRlIEV2ZW50IGFuZAogICAgICAgICAgICAgICBUaW1lZCBTeXN0ZW1zfSwKICBqb3VybmFsICAgPSB7SUVFRSBUcmFucy4gQXV0b21hdC4gQ29udHIufSwKICB2b2x1bWUgICAgPSB7NTd9LAogIG51bWJlciAgICA9IHs3fSwKICB5ZWFyICAgICAgPSB7MjAxMn0sCiAgdHlwZSA9IHtBIC0gSm91cm5hbH0sCiAgcGFnZXMgICAgID0gezE3NTItMTc2NH0sCiAgdXJscGFwZXIgPSB7cGFwZXJzL3RhYy0yMDEyLnBkZn0sCiAgdXJsX2xpbmsgICAgICAgPSB7aHR0cDovL2R4LmRvaS5vcmcvMTAuMTEwOS9UQUMuMjAxMi4yMTgzMTY5fSwKICBkb2kgPSB7aHR0cDovL2R4LmRvaS5vcmcvMTAuMTEwOS9UQUMuMjAxMi4yMTgzMTY5fSwKICBteXdlYnBhZ2UgPSB7dGltZWR9LAogIGtleXdvcmRzID0ge3RpbWVkIGF1dG9tYXRhLCBGYXVsdCBkaWFnbm9zaXMsIENvbXBsZXhpdHl9LAogIGFic3RyYWN0ID0gewogIEluIHRoaXMgcGFwZXIgd2Ugc3R1ZHkgdGhlIGZhdWx0IGNvZGlhZ25vc2lzIHByb2JsZW0gZm9yIGRpc2NyZXRlIGV2ZW50IHN5c3RlbXMgZ2l2ZW4gYnkgZmluaXRlIGF1dG9tYXRhIChGQSkgYW5kIHRpbWVkIHN5c3RlbXMgZ2l2ZW4gYnkgdGltZWQgYXV0b21hdGEgKFRBKS4gV2UgcHJvdmlkZSBhIHVuaWZvcm0gY2hhcmFjdGVyaXNhdGlvbiBvZiBjb2RpYWdub3NhYmlsaXR5IGZvciBGQSBhbmQgVEEgd2hpY2ggZXh0ZW5kcyB0aGUgbmVjZXNzYXJ5IGFuZCBzdWZmaWNpZW50IGNvbmRpdGlvbiB0aGF0IGNoYXJhY3RlcmlzZXMgZGlhZ29zYWJpbGl0eS4gV2UgYWxzbyBzZXR0bGUgdGhlIGNvbXBsZXhpdHkgb2YgdGhlIGNvZGlhZ25vc2FiaWxpdHkgcHJvYmxlbXMgYm90aCBmb3IgRkEgYW5kIFRBIGFuZCBzaG93IHRoYXQgY29kaWFnbm9zYWJpbGl0eSBpcyBQU1BBQ0UtY29tcGxldGUgaW4gYm90aCBjYXNlcy4gRm9yIEZBIHRoaXMgaW1wcm92ZXMgb24gdGhlIHByZXZpb3VzbHkga25vd24gYm91bmQgKEVYUFRJTUUpIGFuZCBmb3IgVEEgaXQgaXMgYSBuZXcgcmVzdWx0LiBXZSB0aGVuIGdlbmVyYWxpc2UgdGhlIHByZXZpb3VzIHJlc3VsdHMgdG8gdGhlIGNhc2Ugb2YgZHluYW1pYyBvYnNlcnZlcnMuIEZpbmFsbHkgd2Ugc2hvdyB0aGF0IHRoZSBjb2RpYWdub3NpcyBwcm9ibGVtIGZvciBUQSB1bmRlciBib3VuZGVkIHJlc291cmNlcyBpcyAyRVhQVElNRS1jb21wbGV0ZS4KICB9Cn0KCgoKQGFydGljbGV7Ym91eWVyLWpsbGktMjAxMSwKICBhdXRob3IgICAgPSB7UGF0cmljaWEgQm91eWVyIGFuZAogICAgICAgICAgICAgICBGcmFuY2sgQ2Fzc2V6IGFuZAogICAgICAgICAgICAgICBGcmFue1xje2N9fW9pcyBMYXJvdXNzaW5pZX0sCiAgdGl0bGUgICAgID0ge1RpbWVkIE1vZGFsIExvZ2ljcyBmb3IgUmVhbC1UaW1lIFN5c3RlbXMgLSBTcGVjaWZpY2F0aW9uLCBWZXJpZmljYXRpb24KICAgICAgICAgICAgICAgYW5kIENvbnRyb2x9LAogIGpvdXJuYWwgICA9IHtKb3VybmFsIG9mIExvZ2ljLCBMYW5ndWFnZSBhbmQgSW5mb3JtYXRpb259LAogIHZvbHVtZSAgICA9IHsyMH0sCiAgbnVtYmVyICAgID0gezJ9LAogIHBhZ2VzICAgICA9IHsxNjktLTIwM30sCiAgeWVhciAgICAgID0gezIwMTF9LAogIFR5cGUgPSB7QSAtIEpvdXJuYWx9LAogIHVybCAgICAgICA9IHtodHRwOi8vZHguZG9pLm9yZy8xMC4xMDA3L3MxMDg0OS0wMTAtOTEyNy00fSwKICBkb2kgICAgICAgPSB7MTAuMTAwNy9zMTA4NDktMDEwLTkxMjctNH0sCiAgdGltZXN0YW1wID0ge1R1ZSwgMTIgQXByIDIwMTEgMDk6MTQ6NTkgKzAyMDB9LAogIGJpYnVybCAgICA9IHtodHRwOi8vZGJscC51bmktdHJpZXIuZGUvcmVjL2JpYi9qb3VybmFscy9qb2xsaS9Cb3V5ZXJDTDExfSwKICBiaWJzb3VyY2UgPSB7ZGJscCBjb21wdXRlciBzY2llbmNlIGJpYmxpb2dyYXBoeSwgaHR0cDovL2RibHAub3JnfSwKICB1cmxwYXBlciA9IHtwYXBlcnMvamxsaS0yMDExLnBkZn0sCiAgY2F0ZWdvcnk9IHtnYW1lc30sCiAgbXl3ZWJwYWdlID0ge3RpbWVkfSwKICBzaG93ID0ge30sCiAga2V5d29yZHMgPSB7bG9naWNzLCByZWFsLXRpbWUsIHRpbWVkIGF1dG9tYXRhLCB0aW1lZCBnYW1lc30sCiAgYWJzdHJhY3QgPSB7CiAgSW4gdGhpcyBwYXBlciwgYSB0aW1lZCBtb2RhbCBsb2dpYyBMYyBpcyBwcmVzZW50ZWQgZm9yIHRoZSBzcGVjaWZpY2F0aW9uCmFuZCB2ZXJpZmljYXRpb24gb2YgcmVhbC10aW1lIHN5c3RlbXMuIFNldmVyYWwgaW1wb3J0YW50IHJlc3VsdHMgZm9yIExjIGFyZSBkaXNjdXNzZWQuCkZpcnN0IHdlIGFkZHJlc3MgdGhlIG1vZGVsIGNoZWNraW5nIHByb2JsZW0gYW5kIHdlIHNob3cgdGhhdCBpdCBpcyBhbiBFWFBUSU1FLWNvbXBsZXRlIHByb2JsZW0uClNlY29uZGx5IHdlIGNvbnNpZGVyIGV4cHJlc3NpdmVuZXNzIGFuZCB3ZSBleHBsYWluIGhvdyB0bwpleHByZXNzIHN0cm9uZyB0aW1lZCBiaXNpbWlsYXJpdHkgYW5kIGhvdyB0byBidWlsZCBjaGFyYWN0ZXJpc3RpYyBmb3JtdWxhcyBmb3IgdGltZWQKYXV0b21hdGEuIFdlIGFsc28gcHJvcG9zZSBhIGNvbXBvc2l0aW9uYWwgYWxnb3JpdGhtIGZvciBMYyBtb2RlbCBjaGVja2luZy4gRmluYWxseQp3ZSBjb25zaWRlciBzZXZlcmFsIGNvbnRyb2wgcHJvYmxlbXMgZm9yIHdoaWNoIExjIGNhbiBiZSB1c2VkIHRvIGNoZWNrIGNvbnRyb2xsYWJpbGl0eS4KICB9Cn0KCgolJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJQolJSUgMjAxMAolJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJQoK\">\n            <i class=\"fa fa-download fa-fw\"></i> Download BibTeX\n          </a>\n        </li>\n        <li>\n          <a href=\"//bibbase.org/rss?bib=http://science.mq.edu.au/~fcassez/bib/franck-bib.bib\">\n            <i class=\"fa fa-rss fa-fw\"></i> RSS Feed\n          </a>\n          </li>\n      </ul>\n      </li>\n\n      \n\n\n      \n    </ul>\n\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_embed\"\n         style=\"display: none;\">\n\n      Excellent! Next you can\n      <a href=\"/network/register?next=/network/newSiteFromTemplate%3Fbiburl=http://science.mq.edu.au/~fcassez/bib/franck-bib.bib\"\n      >create a new website with this list</a>, or\n      embed it in an existing web page by copying &amp; pasting\n      any of the following snippets.\n\n      <div style=\"text-align: left; margin-top: 1em;\">\n        <strong>JavaScript</strong>\n        <span class=\"comment recommended\">(easiest)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;script src=\"https://bibbase.org/show?bib=http%3A%2F%2Fscience.mq.edu.au%2F%7Efcassez%2Fbib%2Ffranck-bib.bib&amp;jsonp=1&amp;filter=mywebpage:timed&amp;css=true&amp;jsonp=1\"&gt;&lt;/script&gt;\n          </code>\n        </div>\n\n        <strong>PHP</strong>\n        <div class=\"well well-small\">\n          <code>\n            &lt;?php\n            $contents = file_get_contents(\"https://bibbase.org/show?bib=http%3A%2F%2Fscience.mq.edu.au%2F%7Efcassez%2Fbib%2Ffranck-bib.bib&amp;jsonp=1&amp;filter=mywebpage:timed&amp;css=true\");\n            print_r($contents);\n            ?&gt;\n          </code>\n        </div>\n\n        <strong>iFrame</strong>\n        <span class=\"comment\">(not recommended)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;iframe src=\"https://bibbase.org/show?bib=http%3A%2F%2Fscience.mq.edu.au%2F%7Efcassez%2Fbib%2Ffranck-bib.bib&amp;jsonp=1&amp;filter=mywebpage:timed&amp;css=true\"&gt;&lt;/iframe&gt;\n          </code>\n        </div>\n\n        <p>\n          For more details see the <a href=\"//bibbase.org/help\">documention</a>.\n        </p>\n      </div>\n    </div>\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_preview\"\n         style=\"display: none;\">\n\n      This is a preview! To use this list on your own web site\n      or create a new web site from it,\n      <a href=\"/network/register?next=/network/newAccountWithFile%3FfileId=\"\n      >create a free account</a>. The file will be added\n      and you will be able to edit it in the File Manager.\n      We will show you instructions once you've created your account.\n    </div>\n\n    <div class=\"alert alert-warning bibbase_msg\" id=\"bibbase_msg_mendeley1\"\n         style=\"display: none;\">\n\n      <p>To the site owner:</p>\n\n      <p><strong>Action required!</strong> Mendeley is changing its\n        API. In order to keep using Mendeley with BibBase past April\n        14th, you need to:\n        <ol>\n          <li>renew the authorization for BibBase on Mendeley, and</li>\n          <li>update the BibBase URL\n            in your page the same way you did when you initially set up\n            this page.\n          </li>\n        </ol>\n      </p>\n\n      <p>\n        <a href=\"http://bibbase.org/cgi-bin/mendeley2/get.py\">\n          <i class=\"fa fa-angle-double-right\"></i>\n          Fix it now</a>\n      </p>\n    </div>\n\n  </div>\n\n\n  <div id=\"bibbase_body\">\n    \n  \n  <div class=\"bibbase_group_whole\" id=\"group_2015\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2015')\"\n      onkeypress=\"toggleGroup('group_2015')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2015</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2015\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/ijc-2014.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/ijc-2014.pdf', event);\">\n    Control and Synthesis of Non-Interferent Timed Systems.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Benattar, G.; <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/timed-games.html\">Cassez, F.</a>; Lime, D.;  and Roux, O. H.\n</span>\n\n  \n\n</span>\n\n  <i>International Journal of Control</i>, 88(2): 217–236.  2015.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/ijc-2014.pdf\"\n     onclick=\"log_download('benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/ijc-2014.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Control and Synthesis of Non-Interferent Timed Systems [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full\"\n     onclick=\"log_download('benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2015', 'http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Control and Synthesis of Non-Interferent Timed Systems [link]\"\n       title=\"Link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Link</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1080/00207179.2014.944356\"\n     onclick=\"log_download('benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2015', 'http://doi.org/10.1080/00207179.2014.944356', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2015\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('benattar-cassez-lime-roux-controlandsynthesisofnoninterferenttimedsystems-2015')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{ijc-14,\nauthor = {Benattar, Gilles and Franck Cassez and Lime, Didier\nand Roux, Olivier H.},\ntitle = {Control and Synthesis of Non-Interferent Timed\nSystems},\nType = {A - Journal},\njournal = {International Journal of Control}, volume = {88}, number =\n{2},\npages = {217--236},\nyear = {2015},\ndoi = {10.1080/00207179.2014.944356},\nmywebpage = {timed},\nurlpaper = {papers/ijc-2014.pdf},\nee = {http://www.tandfonline.com/eprint/h7nIKxnegMGR5M7EaeSF/full},\nkeywords = {security, non-interference},\ncategory = {Non-interference},\nabstract = {We focus on the control and the\nsynthesis of secure timed systems which are modelled as timed automata. The\nsecurity property that the system must satisfy is a non-interference property.\nIntuitively, non-interference ensures the absence of any causal dependency from\na high-level domain to a lower level domain. Various notions of non-interference\nhave been defined in the literature, and in this paper, we focus on strong non-\ndeterministic non-interference (SNNI) and two (bi)simulation-based variants\nthereof (cosimulation-based SNNI and bisimulation-based SNNI). These properties\nand their extensions have been mostly studied in the context of discrete event\nsystems, while it is now well-known that time is an important attack vector\nagainst secure systems. At the same time, there is an obvious interest in going\nbeyond simple verification to control problems: to be able to automatically make\nsystems secure. We consider non-interference properties in the challenging\nsetting of control of dense-time systems specified by timed automata and we\nstudy the two following problems: (1) check whether it is possible to find a\nsub-system so that it is non- interferent; if yes, (2) compute a (largest) sub-\nsystem which is non- interferent. We exhibit decidable sub-classes for these\nproblems, assess their theoretical complexities and provide effective algorithms\nbased on the classical framework of timed games.}\n}\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  We focus on the control and the synthesis of secure timed systems which are modelled as timed automata. The security property that the system must satisfy is a non-interference property. Intuitively, non-interference ensures the absence of any causal dependency from a high-level domain to a lower level domain. Various notions of non-interference have been defined in the literature, and in this paper, we focus on strong non- deterministic non-interference (SNNI) and two (bi)simulation-based variants thereof (cosimulation-based SNNI and bisimulation-based SNNI). These properties and their extensions have been mostly studied in the context of discrete event systems, while it is now well-known that time is an important attack vector against secure systems. At the same time, there is an obvious interest in going beyond simple verification to control problems: to be able to automatically make systems secure. We consider non-interference properties in the challenging setting of control of dense-time systems specified by timed automata and we study the two following problems: (1) check whether it is possible to find a sub-system so that it is non- interferent; if yes, (2) compute a (largest) sub- system which is non- interferent. We exhibit decidable sub-classes for these problems, assess their theoretical complexities and provide effective algorithms based on the classical framework of timed games.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2014\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2014')\"\n      onkeypress=\"toggleGroup('group_2014')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2014</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"brenguier-cassez-raskin-energyandmeanpayofftimedgames-2014\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/hscc-2014.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'brenguier-cassez-raskin-energyandmeanpayofftimedgames-2014', 'http://science.mq.edu.au/~fcassez/bib/papers/hscc-2014.pdf', event);\">\n    Energy and mean-payoff timed games.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Brenguier, R.; <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/timed-games.html\">Cassez, F.</a>;  and Raskin, J.\n</span>\n\n  \n\n</span>\n\n  In <i>17th International Conference on Hybrid Systems: Computation and Control, HSCC'14</i>, pages 283-292,  2014. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/hscc-2014.pdf\"\n     onclick=\"log_download('brenguier-cassez-raskin-energyandmeanpayofftimedgames-2014', 'http://science.mq.edu.au/~fcassez/bib/papers/hscc-2014.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Energy and mean-payoff timed games [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://doi.acm.org/10.1145/2562059.2562116\"\n     onclick=\"log_download('brenguier-cassez-raskin-energyandmeanpayofftimedgames-2014', 'http://doi.acm.org/10.1145/2562059.2562116', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Energy and mean-payoff timed games [link]\"\n       title=\" link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> link</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/brenguier-cassez-raskin-energyandmeanpayofftimedgames-2014\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('brenguier-cassez-raskin-energyandmeanpayofftimedgames-2014')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{hscc-14,\n  author    = {Romain Brenguier and\n               Franck Cassez and\n               Jean-François Raskin},\n  title     = {Energy and mean-payoff timed games},\n  booktitle = {17th International Conference on Hybrid Systems: Computation\n               and Control, HSCC&#x27;14},\n  year      = {2014},\n  pages     = {283-292},\n  urlpaper = {papers/hscc-2014.pdf},\n  url_link     = {http://doi.acm.org/10.1145/2562059.2562116},\n  mywebpage = {timed},\n  show = {},\n  keywords = {hybrid, timed automata, games},\n  abstract = {In this paper, we study energy and mean-payoff timed games.\n  The decision problems that consist in determining the existence of winning strategies in those games are undecidable,\n  and we thus provide semi-algorithms for solving these strategy synthesis problems.\n  We then identify a large class of timed games for which our semi-algorithms terminate and are thus complete.\n  We also study in detail the relation between mean-payoff and energy timed games. Finally,\n  we provide a symbolic algorithm to solve energy timed games and demonstrate its use on small examples using HyTech.},\n  Type = {B - International Conferences},\n\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  In this paper, we study energy and mean-payoff timed games. The decision problems that consist in determining the existence of winning strategies in those games are undecidable, and we thus provide semi-algorithms for solving these strategy synthesis problems. We then identify a large class of timed games for which our semi-algorithms terminate and are thus complete. We also study in detail the relation between mean-payoff and energy timed games. Finally, we provide a symbolic algorithm to solve energy timed games and demonstrate its use on small examples using HyTech.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2013\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2013')\"\n      onkeypress=\"toggleGroup('group_2013')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2013</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"brard-cassez-haddad-lime-roux-theexpressivepoweroftimepetrinets-2013\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/tcs-2013.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'brard-cassez-haddad-lime-roux-theexpressivepoweroftimepetrinets-2013', 'http://science.mq.edu.au/~fcassez/bib/papers/tcs-2013.pdf', event);\">\n    The expressive power of time Petri nets.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Bérard, B.; <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/timed-games.html\">Cassez, F.</a>; Haddad, S.; Lime, D.;  and Roux, O. H.\n</span>\n\n  \n\n</span>\n\n  <i>Theoretical Computer Science</i>, 474: 1-20.  2013.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/tcs-2013.pdf\"\n     onclick=\"log_download('brard-cassez-haddad-lime-roux-theexpressivepoweroftimepetrinets-2013', 'http://science.mq.edu.au/~fcassez/bib/papers/tcs-2013.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"The expressive power of time Petri nets [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/http://dx.doi.org/10.1016/j.tcs.2012.12.005\"\n     onclick=\"log_download('brard-cassez-haddad-lime-roux-theexpressivepoweroftimepetrinets-2013', 'http://doi.org/http://dx.doi.org/10.1016/j.tcs.2012.12.005', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/brard-cassez-haddad-lime-roux-theexpressivepoweroftimepetrinets-2013\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('brard-cassez-haddad-lime-roux-theexpressivepoweroftimepetrinets-2013')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{tpn-13,\n  author    = {Béatrice Bérard and\n               Franck Cassez and\n               Serge Haddad and\n               Didier Lime and\n               Olivier H. Roux},\n  title     = {The expressive power of time {Petri} nets},\n  journal   =  {Theoretical Computer Science},\n  Type = {A - Journal},\n  volume    = {474},\n  year      = {2013},\n  pages     = {1-20},\n  doi        = {http://dx.doi.org/10.1016/j.tcs.2012.12.005},\n  bibsource = {DBLP, http://dblp.uni-trier.de},\n  category= {Timed Petri nets},\n  mywebpage = {timed},\n  keywords = {time petri nets, timed automata},\n  urlpaper = {papers/tcs-2013.pdf},\n  abstract = {We investigate expressiveness questions for time Petri nets (TPNs)\n  and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs)\n  as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs.\nWe give a syntactical translation from bounded GTPNs to timed automata (TA)\nthat generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly l\ness expressive than TA w.r.t. weak timed bisimilarity.\nWe prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance.\nFinally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs &quot;á la Merlin&quot; w.r.t.\nweak timed bisimilarity. These results provide a unified comparison of the expressiveness of\nmany variants of timed models often used in practice. It leads to new important results for TPNs.\nAmong them are: 1-safe TPNs and bounded-TPNs are equally expressive; $\\epsilon$-transitions strictly\nincrease the expressive power of TPNs; self modifying nets as well as read,\ninhibitor and reset arcs do not add expressiveness to bounded TPNs.\n}\n}\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  We investigate expressiveness questions for time Petri nets (TPNs) and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs) as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs. We give a syntactical translation from bounded GTPNs to timed automata (TA) that generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly l ess expressive than TA w.r.t. weak timed bisimilarity. We prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance. Finally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs \"á la Merlin\" w.r.t. weak timed bisimilarity. These results provide a unified comparison of the expressiveness of many variants of timed models often used in practice. It leads to new important results for TPNs. Among them are: 1-safe TPNs and bounded-TPNs are equally expressive; $ε$-transitions strictly increase the expressive power of TPNs; self modifying nets as well as read, inhibitor and reset arcs do not add expressiveness to bounded TPNs. \n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2012\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2012')\"\n      onkeypress=\"toggleGroup('group_2012')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2012</span>\n      <span class=\"bibbase_group_count\">\n        \n        (3)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/atva-2012.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012', 'http://science.mq.edu.au/~fcassez/bib/papers/atva-2012.pdf', event);\">\n    Controllers with Minimal Observation Power (Application to Timed Systems).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Bulychev, P. E.; <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/timed-games.html\">Cassez, F.</a>; David, A.; Larsen, K. G.; Raskin, J.;  and Reynier, P.\n</span>\n\n  \n\n</span>\n\n  In <i>Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012</i>, pages 223-237,  2012. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/atva-2012.pdf\"\n     onclick=\"log_download('bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012', 'http://science.mq.edu.au/~fcassez/bib/papers/atva-2012.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Controllers with Minimal Observation Power (Application to Timed Systems) [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://dx.doi.org/10.1007/978-3-642-33386-6_19\"\n     onclick=\"log_download('bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012', 'http://dx.doi.org/10.1007/978-3-642-33386-6_19', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Controllers with Minimal Observation Power (Application to Timed Systems) [link]\"\n       title=\" link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> link</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>1 download</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{atva-12,\n  author    = {Peter E. Bulychev and\n               Franck Cassez and\n               Alexandre David and\n               Kim Guldstrand Larsen and\n               Jean-François Raskin and\n               Pierre-Alain Reynier},\n  title     = {Controllers with Minimal Observation Power (Application\n               to Timed Systems)},\n  booktitle = {Automated Technology for Verification and Analysis - 10th\n               International Symposium, ATVA 2012},\n  year      = {2012},\n  pages     = {223-237},\n  urlpaper = {papers/atva-2012.pdf},\n  url_link  = {http://dx.doi.org/10.1007/978-3-642-33386-6_19},\n  mywebpage = {timed},\n  keywords = {timed automata, timed games, control},\n  abstract = {\n  We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies.\n  },\n        Type = {B - International Conferences},\n\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies. \n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://arxiv.org/abs/1207.1276\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012', 'http://arxiv.org/abs/1207.1276', event);\">\n    Controllers with Minimal Observation Power (Application to Timed Systems).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Bulychev, P. E.; <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/timed-games.html\">Cassez, F.</a>; David, A.; Larsen, K. G.; Raskin, J.;  and Reynier, P.\n</span>\n\n  \n\n</span>\n\n  <i>CoRR</i>, abs/1207.1276.  2012.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://arxiv.org/abs/1207.1276\"\n     onclick=\"log_download('bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012', 'http://arxiv.org/abs/1207.1276', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Controllers with Minimal Observation Power (Application to Timed Systems) [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>1 download</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bulychev-cassez-david-larsen-raskin-reynier-controllerswithminimalobservationpowerapplicationtotimedsystems-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{bulychev-2012,\n  author    = {Peter E. Bulychev and\n               Franck Cassez and\n               Alexandre David and\n               Kim G. Larsen and\n               Jean{-}Fran{\\c{c}}ois Raskin and\n               Pierre{-}Alain Reynier},\n  title     = {Controllers with Minimal Observation Power (Application to Timed Systems)},\n  journal   = {CoRR},\n  Type = {E - Reports},\n  volume    = {abs/1207.1276},\n  year      = {2012},\n  urlpaper       = {http://arxiv.org/abs/1207.1276},\n  timestamp = {Wed, 10 Oct 2012 21:28:54 +0200},\n  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1207-1276},\n  bibsource = {dblp computer science bibliography, http://dblp.org},\n  abstract = {\n  We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies.\n  },\n   mywebpage = {timed},\n  keywords = {timed automata, timed games, control},\n\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies. \n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"cassez-thecomplexityofcodiagnosabilityfordiscreteeventandtimedsystems-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/tac-2012.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-thecomplexityofcodiagnosabilityfordiscreteeventandtimedsystems-2012', 'http://science.mq.edu.au/~fcassez/bib/papers/tac-2012.pdf', event);\">\n    The Complexity of Codiagnosability for Discrete Event and Timed Systems.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/timed-games.html\">Cassez, F.</a>\n</span>\n\n  \n\n</span>\n\n  <i>IEEE Trans. Automat. Contr.</i>, 57(7): 1752-1764.  2012.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/tac-2012.pdf\"\n     onclick=\"log_download('cassez-thecomplexityofcodiagnosabilityfordiscreteeventandtimedsystems-2012', 'http://science.mq.edu.au/~fcassez/bib/papers/tac-2012.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"The Complexity of Codiagnosability for Discrete Event and Timed Systems [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://dx.doi.org/10.1109/TAC.2012.2183169\"\n     onclick=\"log_download('cassez-thecomplexityofcodiagnosabilityfordiscreteeventandtimedsystems-2012', 'http://dx.doi.org/10.1109/TAC.2012.2183169', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"The Complexity of Codiagnosability for Discrete Event and Timed Systems [link]\"\n       title=\" link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> link</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/http://dx.doi.org/10.1109/TAC.2012.2183169\"\n     onclick=\"log_download('cassez-thecomplexityofcodiagnosabilityfordiscreteeventandtimedsystems-2012', 'http://doi.org/http://dx.doi.org/10.1109/TAC.2012.2183169', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-thecomplexityofcodiagnosabilityfordiscreteeventandtimedsystems-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>1 download</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-thecomplexityofcodiagnosabilityfordiscreteeventandtimedsystems-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{tac-12,\n  author    = {Franck Cassez},\n  title     = {The Complexity of Codiagnosability for Discrete Event and\n               Timed Systems},\n  journal   = {IEEE Trans. Automat. Contr.},\n  volume    = {57},\n  number    = {7},\n  year      = {2012},\n  type = {A - Journal},\n  pages     = {1752-1764},\n  urlpaper = {papers/tac-2012.pdf},\n  url_link       = {http://dx.doi.org/10.1109/TAC.2012.2183169},\n  doi = {http://dx.doi.org/10.1109/TAC.2012.2183169},\n  mywebpage = {timed},\n  keywords = {timed automata, Fault diagnosis, Complexity},\n  abstract = {\n  In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterisation of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterises diagosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. We then generalise the previous results to the case of dynamic observers. Finally we show that the codiagnosis problem for TA under bounded resources is 2EXPTIME-complete.\n  }\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterisation of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterises diagosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. We then generalise the previous results to the case of dynamic observers. Finally we show that the codiagnosis problem for TA under bounded resources is 2EXPTIME-complete. \n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2011\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2011')\"\n      onkeypress=\"toggleGroup('group_2011')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2011</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"bouyer-cassez-laroussinie-timedmodallogicsforrealtimesystemsspecificationverificationandcontrol-2011\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/jlli-2011.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bouyer-cassez-laroussinie-timedmodallogicsforrealtimesystemsspecificationverificationandcontrol-2011', 'http://science.mq.edu.au/~fcassez/bib/papers/jlli-2011.pdf', event);\">\n    Timed Modal Logics for Real-Time Systems - Specification, Verification and Control.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Bouyer, P.; <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/timed-games.html\">Cassez, F.</a>;  and Laroussinie, F.\n</span>\n\n  \n\n</span>\n\n  <i>Journal of Logic, Language and Information</i>, 20(2): 169–203.  2011.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/jlli-2011.pdf\"\n     onclick=\"log_download('bouyer-cassez-laroussinie-timedmodallogicsforrealtimesystemsspecificationverificationandcontrol-2011', 'http://science.mq.edu.au/~fcassez/bib/papers/jlli-2011.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Timed Modal Logics for Real-Time Systems - Specification, Verification and Control [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/s10849-010-9127-4\"\n     onclick=\"log_download('bouyer-cassez-laroussinie-timedmodallogicsforrealtimesystemsspecificationverificationandcontrol-2011', 'http://doi.org/10.1007/s10849-010-9127-4', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bouyer-cassez-laroussinie-timedmodallogicsforrealtimesystemsspecificationverificationandcontrol-2011\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bouyer-cassez-laroussinie-timedmodallogicsforrealtimesystemsspecificationverificationandcontrol-2011')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  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. \n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n\n\n\n  </div>\n\n\n  <!-- Modal -->\n\n  <!-- <iframe id=\"bibbase_network_frame\" -->\n  <!--         src=\"//bibbase.org/network/control\" -->\n  <!--         style=\"display: none;\"> -->\n  <!-- </iframe> -->\n\n</div>\n"}; document.write(bibbase_data.data);