We are happy to announce, that our tool-paper (Hofmann and Schupp) on our tool TACoS (Timed Automata-based Controller Synthesis) was accepted for presentation at SEFM’21.

The presentation will take place on Thursday, December 9 16:45 CET at SEFM’21.

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 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. 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

References

  1. Hofmann, Till, and Stefan Schupp. “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}
}