Controlling Timed Automata against MTL Specifications with TACoS. Hofmann, T. & Schupp, S. Science of Computer Programming, 225:102898, January, 2023.
Controlling Timed Automata against MTL Specifications with TACoS [pdf]Paper  doi  abstract   bibtex   6 downloads  
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.

Downloads: 6