@inproceedings{hofmannTACoSToolMTL2021,
  title = {{{TACoS}}: A Tool for {{MTL}} Controller Synthesis},
  booktitle = {Proceedings of the 19th {{International Conference}} on {{Software Engineering}} and {{Formal Methods}}},
  author = {Hofmann, Till and Schupp, Stefan},
  year = {2021},
  abstract = {We introduce TACoS, a tool for synthesizing controllers
              satisfying MTL specifications of undesired behavior with timing
              constraints.  Our contribution extends an existing theoretical
              approach towards practical applications.  The most notable
              features include: Online labeling to terminate early if a
              solution has been found, heuristic search to expand the most
              promising nodes first, search graph pruning to reduce the problem
              size by pruning irrelevant parts of the search graph, and
              re-using previously explored search nodes to further reduce the
              search graph.  Finally, multi-threading support allows to make
              use of modern CPUs with many parallel threads.  TACoS comes with
              a C++ library with minimal external dependencies and
              simple-to-use API.  We evaluate our approach on a number of
              scenarios and investigate how each of the enhancements improves
              the performance. The tool is publicly available at
              https://github.com/morxa/tacos.},
  url = {https://kbsg.rwth-aachen.de/papers/sefm21-tacos.pdf},
  url_slides = {https://kbsg.rwth-aachen.de/papers/sefm21-tacos-slides.pdf},
  doi = {10.1007/978-3-030-92124-8_21},
  note = {Best Tool Paper Award},
  url_Code = {https://github.com/morxa/tacos}
}

{"_id":"DknZ4uZwKMYonccKY","bibbaseid":"hofmann-schupp-tacosatoolformtlcontrollersynthesis-2021","author_short":["Hofmann, T.","Schupp, S."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"TACoS: A Tool for MTL Controller Synthesis","booktitle":"Proceedings of the 19th International Conference on Software Engineering and Formal Methods","author":[{"propositions":[],"lastnames":["Hofmann"],"firstnames":["Till"],"suffixes":[]},{"propositions":[],"lastnames":["Schupp"],"firstnames":["Stefan"],"suffixes":[]}],"year":"2021","abstract":"We introduce TACoS, a tool for synthesizing controllers satisfying MTL specifications of undesired behavior with timing constraints. Our contribution extends an existing theoretical approach towards practical applications. The most notable features include: Online labeling to terminate early if a solution has been found, heuristic search to expand the most promising nodes first, search graph pruning to reduce the problem size by pruning irrelevant parts of the search graph, and re-using previously explored search nodes to further reduce the search graph. Finally, multi-threading support allows to make use of modern CPUs with many parallel threads. TACoS comes with a C++ library with minimal external dependencies and simple-to-use API. We evaluate our approach on a number of scenarios and investigate how each of the enhancements improves the performance. The tool is publicly available at https://github.com/morxa/tacos.","url":"https://kbsg.rwth-aachen.de/papers/sefm21-tacos.pdf","url_slides":"https://kbsg.rwth-aachen.de/papers/sefm21-tacos-slides.pdf","doi":"10.1007/978-3-030-92124-8_21","note":"Best Tool Paper Award","url_code":"https://github.com/morxa/tacos","bibtex":"@inproceedings{hofmannTACoSToolMTL2021,\n title = {{{TACoS}}: A Tool for {{MTL}} Controller Synthesis},\n booktitle = {Proceedings of the 19th {{International Conference}} on {{Software Engineering}} and {{Formal Methods}}},\n author = {Hofmann, Till and Schupp, Stefan},\n year = {2021},\n abstract = {We introduce TACoS, a tool for synthesizing controllers\n satisfying MTL specifications of undesired behavior with timing\n constraints. Our contribution extends an existing theoretical\n approach towards practical applications. The most notable\n features include: Online labeling to terminate early if a\n solution has been found, heuristic search to expand the most\n promising nodes first, search graph pruning to reduce the problem\n size by pruning irrelevant parts of the search graph, and\n re-using previously explored search nodes to further reduce the\n search graph. Finally, multi-threading support allows to make\n use of modern CPUs with many parallel threads. TACoS comes with\n a C++ library with minimal external dependencies and\n simple-to-use API. We evaluate our approach on a number of\n scenarios and investigate how each of the enhancements improves\n the performance. The tool is publicly available at\n https://github.com/morxa/tacos.},\n url = {https://kbsg.rwth-aachen.de/papers/sefm21-tacos.pdf},\n url_slides = {https://kbsg.rwth-aachen.de/papers/sefm21-tacos-slides.pdf},\n doi = {10.1007/978-3-030-92124-8_21},\n note = {Best Tool Paper Award},\n url_Code = {https://github.com/morxa/tacos}\n}\n\n","author_short":["Hofmann, T.","Schupp, S."],"key":"hofmannTACoSToolMTL2021","id":"hofmannTACoSToolMTL2021","bibbaseid":"hofmann-schupp-tacosatoolformtlcontrollersynthesis-2021","role":"author","urls":{"Paper":"https://kbsg.rwth-aachen.de/papers/sefm21-tacos.pdf"," slides":"https://kbsg.rwth-aachen.de/papers/sefm21-tacos-slides.pdf"," code":"https://github.com/morxa/tacos"},"metadata":{"authorlinks":{}},"downloads":2},"bibtype":"inproceedings","biburl":"https://ml.rwth-aachen.de/~till.hofmann/files/hofmann.bib","dataSources":["dqRQPSg6Hy3ZXQg7z","P2RLsqAnkwjGHmpeQ","zp5TdwDdbpGvos9cF"],"keywords":[],"search_terms":["tacos","tool","mtl","controller","synthesis","hofmann","schupp"],"title":"TACoS: A Tool for MTL Controller Synthesis","year":2021,"downloads":2}