TACoS is a TA Controller Synthesis tool for MTL specifications. Given a plant timed automaton, an MTL specification, and a partitioning of the actions into environment and controller actions, it synthesizes a controller such that the plant satisfies the specification.

Please check out the Wiki or the Doxygen docs for further information.

Detailed benchmark results are available here. You can also test the code and run the benchmarks on CodeOcean.

Publications

1. Hofmann, T., & Schupp, S. (2023). Controlling timed automata against MTL specifications with TACoS. Science of Computer Programming 225, 102898. (pdf) (doi)
2. Hofmann, T., & Schupp, S. (2021). TACoS: A tool for MTL controller synthesis. Proceedings of the 19th International Conference on Software Engineering and Formal Methods. Best Tool Paper Award (pdf) (doi)