Controlling Timed Automata against MTL Specifications with TACoS. Hofmann, T. & Schupp, S. Science of Computer Programming, 225:102898, January, 2023.
Paper doi abstract bibtex 6 downloads TACoS is a tool for synthesizing controllers against specifications of undesired behavior with timing constraints. Given a timed automaton and an MTL specification, the tool synthesizes a controller that guarantees that every possible execution of the system satisfies the given specification. TACoS comes with a C++ library with a simple-to-use API and can read from and write to human-readable text input and output. In this paper, we outline the approach of the tool and present two examples in further detail.
@article{hofmannControllingTimedAutomata2023,
title = {Controlling Timed Automata against {{MTL}} Specifications with {{TACoS}}},
author = {Hofmann, Till and Schupp, Stefan},
year = {2023},
month = jan,
journal = {Science of Computer Programming},
volume = {225},
pages = {102898},
issn = {0167-6423},
url = {https://kbsg.rwth-aachen.de/papers/scico2023-tacos.pdf},
doi = {https://doi.org/10.1016/j.scico.2022.102898},
abstract = {TACoS is a tool for synthesizing controllers against specifications of undesired behavior with timing constraints. Given a timed automaton and an MTL specification, the tool synthesizes a controller that guarantees that every possible execution of the system satisfies the given specification. TACoS comes with a C++ library with a simple-to-use API and can read from and write to human-readable text input and output. In this paper, we outline the approach of the tool and present two examples in further detail.},
langid = {english},
keywords = {Controller synthesis,Metric temporal logic,Timed automata}
}
Downloads: 6
{"_id":"gyXP3PQBSuXZsF2WG","bibbaseid":"hofmann-schupp-controllingtimedautomataagainstmtlspecificationswithtacos-2023","author_short":["Hofmann, T.","Schupp, S."],"bibdata":{"bibtype":"article","type":"article","title":"Controlling Timed Automata against MTL Specifications with TACoS","author":[{"propositions":[],"lastnames":["Hofmann"],"firstnames":["Till"],"suffixes":[]},{"propositions":[],"lastnames":["Schupp"],"firstnames":["Stefan"],"suffixes":[]}],"year":"2023","month":"January","journal":"Science of Computer Programming","volume":"225","pages":"102898","issn":"0167-6423","url":"https://kbsg.rwth-aachen.de/papers/scico2023-tacos.pdf","doi":"https://doi.org/10.1016/j.scico.2022.102898","abstract":"TACoS is a tool for synthesizing controllers against specifications of undesired behavior with timing constraints. Given a timed automaton and an MTL specification, the tool synthesizes a controller that guarantees that every possible execution of the system satisfies the given specification. TACoS comes with a C++ library with a simple-to-use API and can read from and write to human-readable text input and output. In this paper, we outline the approach of the tool and present two examples in further detail.","langid":"english","keywords":"Controller synthesis,Metric temporal logic,Timed automata","bibtex":"@article{hofmannControllingTimedAutomata2023,\n title = {Controlling Timed Automata against {{MTL}} Specifications with {{TACoS}}},\n author = {Hofmann, Till and Schupp, Stefan},\n year = {2023},\n month = jan,\n journal = {Science of Computer Programming},\n volume = {225},\n pages = {102898},\n issn = {0167-6423},\n url = {https://kbsg.rwth-aachen.de/papers/scico2023-tacos.pdf},\n doi = {https://doi.org/10.1016/j.scico.2022.102898},\n abstract = {TACoS is a tool for synthesizing controllers against specifications of undesired behavior with timing constraints. Given a timed automaton and an MTL specification, the tool synthesizes a controller that guarantees that every possible execution of the system satisfies the given specification. TACoS comes with a C++ library with a simple-to-use API and can read from and write to human-readable text input and output. In this paper, we outline the approach of the tool and present two examples in further detail.},\n langid = {english},\n keywords = {Controller synthesis,Metric temporal logic,Timed automata}\n}\n\n","author_short":["Hofmann, T.","Schupp, S."],"key":"hofmannControllingTimedAutomata2023","id":"hofmannControllingTimedAutomata2023","bibbaseid":"hofmann-schupp-controllingtimedautomataagainstmtlspecificationswithtacos-2023","role":"author","urls":{"Paper":"https://kbsg.rwth-aachen.de/papers/scico2023-tacos.pdf"},"keyword":["Controller synthesis","Metric temporal logic","Timed automata"],"metadata":{"authorlinks":{}},"downloads":6},"bibtype":"article","biburl":"https://ml.rwth-aachen.de/~till.hofmann/files/hofmann.bib","dataSources":["dqRQPSg6Hy3ZXQg7z","P2RLsqAnkwjGHmpeQ","zp5TdwDdbpGvos9cF"],"keywords":["controller synthesis","metric temporal logic","timed automata"],"search_terms":["controlling","timed","automata","against","mtl","specifications","tacos","hofmann","schupp"],"title":"Controlling Timed Automata against MTL Specifications with TACoS","year":2023,"downloads":6}