Our tool TACoS was published at the Elsevier Journal Science of Computer Programming (Hofmann and Schupp).

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.

References

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