Motivation
Controller synthesis is the problem of determining a policy for a given system that ensures the resulting behavior satisfies a given specification, independent of the behavior of the environment. As an example, consider a robot that works in a coffee house. Whenever a customer orders a coffee, the robot should prepare the coffee and deliver it to the customer. In MTL controller synthesis, the system is modeled as a timed automaton and the specification is given as a formula in Metric Temporal Logic. This allows to consider timing aspects, e.g., whenever a customer orders a coffee, they should receive their order within 5 minutes.
In our group, we have developed TACoS [1, 2], a tool that is able to synthesize a controller for MTL specifications. While we have used several optimization techniques to improve the performance of the tool, the synthesis problem is still computationally expensive and TACoS uses an explicit representation of the state space. Symbolic representations do not use an explicit representation, but instead represent a set of states compactly, e.g., as a set of constraints. These methods have been researched extensively on related problems, but not for MTL synthesis.
Goals
The goal of this thesis is to investigate existing methods for symbolic synthesis on timed systems and to extend TACoS to support suitable symbolic representations. Suitable candidates may be zone constructions [3], symmetry reduction [4], or control structure analysis [5]. More specifically, the thesis will involve the following steps:
- Analyze existing methods for symbolic synthesis on timed systems and check which methods are suitable for MTL controller synthesis.
- Implement selected symbolic representations in TACoS.
- Evaluate the performance of the symbolic synthesis approach on a set of benchmarks and compare it to the existing approach.
What we expect:
You should
- be familiar with C++,
- have a basic understanding of logic and automata, ideally with some background in temporal logic.
Interested?
If you are interested or have further questions, please contact Matthew Lynn or Till Hofmann.
-
T. Hofmann and S. Schupp, “TACoS: A tool for MTL controller synthesis,” in Proceedings of the 19th International Conference on Software Engineering and Formal Methods (SEFM), 2021, pp. 372–379. doi: 10.1007/978-3-030-92124-8_21. ↩︎
-
T. Hofmann and S. Schupp, “Controlling timed automata against MTL specifications with TACoS,” Sci.Co., vol. 225, p. 102898, Jan. 2023, doi: 10.1016/j.scico.2022.102898. ↩︎
-
K. G. Larsen, P. Pettersson, and W. Yi, “Model-checking for real-time systems,” in Fundamentals of Computation Theory, H. Reichel, Ed., in Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1995, pp. 62–88. doi: 10.1007/3-540-60249-6_41. ↩︎
-
M. Hendriks, G. Behrmann, K. Larsen, P. Niebert, and F. Vaandrager, “Adding Symmetry Reduction to Uppaal,” in Formal Modeling and Analysis of Timed Systems, K. G. Larsen and P. Niebert, Eds., in Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2004, pp. 46–59. doi: 10.1007/978-3-540-40903-8_5. ↩︎
-
K. G. Larsen, P. Pettersson, and W. Yi, “Uppaal: Status & developments,” in Computer Aided Verification, O. Grumberg, Ed., in Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1997, pp. 456–459. doi: 10.1007/3-540-63166-6_47. ↩︎