TACoS

TACoS (Hofmann and Schupp), a tool for synthesizing controllers satisfying MTL specifications of undesired behavior with timing constraints is a product of this project. The project was initiated by Till Hofmann in the course of the UnRAVeL Research Training Group which we were both part of.

The tool started as an implementation of the theoretical works from Bouyer et al.. During this project, we extended this theoretical work towards practical application. 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 reusing 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. It has been additionally published in Science of Computer Programming (Hofmann and Schupp).

Publications

Hofmann, Till, and Stefan Schupp. “Controlling Timed Automata against MTL Specifications with TACoS.” Science of Computer Programming, vol. 225, 2023, p. 102898, doi:10.1016/j.scico.2022.102898.

@article{HOFMANN2023102898,
  title = {Controlling timed automata against MTL specifications with TACoS},
  journal = {Science of Computer Programming},
  volume = {225},
  pages = {102898},
  year = {2023},
  issn = {0167-6423},
  doi = {10.1016/j.scico.2022.102898},
  url = {https://www.sciencedirect.com/science/article/pii/S0167642322001319},
  author = {Hofmann, Till and Schupp, Stefan},
  keywords = {Controller synthesis, Timed automata, Metric temporal logic}
}

---. “TACoS: A Tool for MTL Controller Synthesis.” Software Engineering and Formal Methods, edited by Radu Calinescu and Corina S. Păsăreanu, vol. 13085, Springer International Publishing, 2021, pp. 372–79, doi:10.1007/978-3-030-92124-8_21.

@incollection{hofmannTACoSToolMTL2021,
  title = {{{TACoS}}: {{A Tool}} for {{MTL Controller Synthesis}}},
  shorttitle = {{{TACoS}}},
  booktitle = {Software {{Engineering}} and {{Formal Methods}}},
  author = {Hofmann, Till and Schupp, Stefan},
  editor = {Calinescu, Radu and P{\u a}s{\u a}reanu, Corina S.},
  year = {2021},
  volume = {13085},
  pages = {372--379},
  publisher = {{Springer International Publishing}},
  address = {{Cham}},
  doi = {10.1007/978-3-030-92124-8_21},
  isbn = {978-3-030-92123-1 978-3-030-92124-8},
  langid = {english}
}

Links

Publications