Controller Synthesis for MTL Specifications. Bouyer, P., Bozzelli, L., & Chevalier, F. In Baier, C. & Hermanns, H., editors, Proceedings of the 17th International Conference on Concurrency Theory (CONCUR), of Lecture Notes in Computer Science, pages 450–464, 2006. Springer Berlin Heidelberg. abstract bibtex We consider the control problem for timed automata against specifications given as MTL formulas. The logic MTL is a linear-time timed temporal logic which extends LTL with timing constraints on modalities, and recently, its model-checking has been proved decidable in several cases. We investigate these decidable fragments of MTL (full MTL when interpreted over finite timed words, and Safety-MTL when interpreted over infinite timed words), and prove two kinds of results. (1) We first prove that, contrary to model-checking, the control problem is undecidable. Roughly, the computation of a lossy channel system could be encoded as a model-checking problem, and we prove here that a perfect channel system can be encoded as a control problem. (2) We then prove that if we fix the resources of the controller (by resources we mean clocks and constants that the controller can use), the control problem becomes decidable. This decidability result relies on properties of well (and better) quasi-orderings.
@inproceedings{bouyer_controller_2006,
series = {Lecture {Notes} in {Computer} {Science}},
title = {Controller {Synthesis} for {MTL} {Specifications}},
isbn = {978-3-540-37377-3},
abstract = {We consider the control problem for timed automata against specifications given as MTL formulas. The logic MTL is a linear-time timed temporal logic which extends LTL with timing constraints on modalities, and recently, its model-checking has been proved decidable in several cases. We investigate these decidable fragments of MTL (full MTL when interpreted over finite timed words, and Safety-MTL when interpreted over infinite timed words), and prove two kinds of results. (1) We first prove that, contrary to model-checking, the control problem is undecidable. Roughly, the computation of a lossy channel system could be encoded as a model-checking problem, and we prove here that a perfect channel system can be encoded as a control problem. (2) We then prove that if we fix the resources of the controller (by resources we mean clocks and constants that the controller can use), the control problem becomes decidable. This decidability result relies on properties of well (and better) quasi-orderings.},
language = {en},
booktitle = {Proceedings of the 17th {International} {Conference} on {Concurrency} {Theory} ({CONCUR})},
publisher = {Springer Berlin Heidelberg},
author = {Bouyer, Patricia and Bozzelli, Laura and Chevalier, Fabrice},
editor = {Baier, Christel and Hermanns, Holger},
year = {2006},
keywords = {Control Problem, Controller Synthesis, Temporal Logic, Undesired Behaviour, Winning Strategy},
pages = {450--464}
}
Downloads: 0
{"_id":"RYX8jvWAW2JioSsy8","bibbaseid":"bouyer-bozzelli-chevalier-controllersynthesisformtlspecifications-2006","authorIDs":[],"author_short":["Bouyer, P.","Bozzelli, L.","Chevalier, F."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","series":"Lecture Notes in Computer Science","title":"Controller Synthesis for MTL Specifications","isbn":"978-3-540-37377-3","abstract":"We consider the control problem for timed automata against specifications given as MTL formulas. The logic MTL is a linear-time timed temporal logic which extends LTL with timing constraints on modalities, and recently, its model-checking has been proved decidable in several cases. We investigate these decidable fragments of MTL (full MTL when interpreted over finite timed words, and Safety-MTL when interpreted over infinite timed words), and prove two kinds of results. (1) We first prove that, contrary to model-checking, the control problem is undecidable. Roughly, the computation of a lossy channel system could be encoded as a model-checking problem, and we prove here that a perfect channel system can be encoded as a control problem. (2) We then prove that if we fix the resources of the controller (by resources we mean clocks and constants that the controller can use), the control problem becomes decidable. This decidability result relies on properties of well (and better) quasi-orderings.","language":"en","booktitle":"Proceedings of the 17th International Conference on Concurrency Theory (CONCUR)","publisher":"Springer Berlin Heidelberg","author":[{"propositions":[],"lastnames":["Bouyer"],"firstnames":["Patricia"],"suffixes":[]},{"propositions":[],"lastnames":["Bozzelli"],"firstnames":["Laura"],"suffixes":[]},{"propositions":[],"lastnames":["Chevalier"],"firstnames":["Fabrice"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Baier"],"firstnames":["Christel"],"suffixes":[]},{"propositions":[],"lastnames":["Hermanns"],"firstnames":["Holger"],"suffixes":[]}],"year":"2006","keywords":"Control Problem, Controller Synthesis, Temporal Logic, Undesired Behaviour, Winning Strategy","pages":"450–464","bibtex":"@inproceedings{bouyer_controller_2006,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Controller {Synthesis} for {MTL} {Specifications}},\n\tisbn = {978-3-540-37377-3},\n\tabstract = {We consider the control problem for timed automata against specifications given as MTL formulas. The logic MTL is a linear-time timed temporal logic which extends LTL with timing constraints on modalities, and recently, its model-checking has been proved decidable in several cases. We investigate these decidable fragments of MTL (full MTL when interpreted over finite timed words, and Safety-MTL when interpreted over infinite timed words), and prove two kinds of results. (1) We first prove that, contrary to model-checking, the control problem is undecidable. Roughly, the computation of a lossy channel system could be encoded as a model-checking problem, and we prove here that a perfect channel system can be encoded as a control problem. (2) We then prove that if we fix the resources of the controller (by resources we mean clocks and constants that the controller can use), the control problem becomes decidable. This decidability result relies on properties of well (and better) quasi-orderings.},\n\tlanguage = {en},\n\tbooktitle = {Proceedings of the 17th {International} {Conference} on {Concurrency} {Theory} ({CONCUR})},\n\tpublisher = {Springer Berlin Heidelberg},\n\tauthor = {Bouyer, Patricia and Bozzelli, Laura and Chevalier, Fabrice},\n\teditor = {Baier, Christel and Hermanns, Holger},\n\tyear = {2006},\n\tkeywords = {Control Problem, Controller Synthesis, Temporal Logic, Undesired Behaviour, Winning Strategy},\n\tpages = {450--464}\n}\n\n","author_short":["Bouyer, P.","Bozzelli, L.","Chevalier, F."],"editor_short":["Baier, C.","Hermanns, H."],"key":"bouyer_controller_2006","id":"bouyer_controller_2006","bibbaseid":"bouyer-bozzelli-chevalier-controllersynthesisformtlspecifications-2006","role":"author","urls":{},"keyword":["Control Problem","Controller Synthesis","Temporal Logic","Undesired Behaviour","Winning Strategy"],"downloads":0},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/tillhofmann","creationDate":"2019-12-09T14:42:18.050Z","downloads":0,"keywords":["control problem","controller synthesis","temporal logic","undesired behaviour","winning strategy"],"search_terms":["controller","synthesis","mtl","specifications","bouyer","bozzelli","chevalier"],"title":"Controller Synthesis for MTL Specifications","year":2006,"dataSources":["9pYjFWPBodPyDyb7N"]}