# SURF 2018: Test design for temporal logic controllers

**2018 SURF: project description**

- Mentor: Richard M. Murray
- Co-mentor: Sofie Haesaert

The design of complex, high-tech, safety-critical systems such as autonomous vehicles, intelligent robots, and cyber-physical infrastructures, demands guarantees on their correct and reliable behavior. Correct functioning and reliability over models of systems can be attained by the use of temporal logics in the specification and design of their controllers [1]. The use such formal methods carries the promise of a decrease in design faults and implementation errors.

In practice, for most physical systems the dynamical behavior is known only in part: this holds in particular with biological systems or with classes of engineered systems where, as a consequence, the use of uncertain control models built from data is a common practice [2]. Since these data-driven models are an empirical approximation it is important to test the designed controllers before implementation. The design of experiments that allows for the verification of formal properties can be formulated as an stochastic optimal control problem [3].

In this study the objective is to research smart ways of testing these temporal logic controllers. By looking at the confidence in the modeling assumptions, we want to develop tests to optimally verify the robustness of the designed controlled systems.

Familiarity with the following topics is a bonus

- Classical control theory for discrete systems (or continuous)
- Data-driven modeling and experiment design
- Convex optimization in control theory

**References**

[1] Wongpiromsarn, T., Topcu, U., Ozay, N., Xu, H., & Murray, R. M. ``TuLiP: a software toolbox for receding horizon temporal logic planning." In Proceedings of the 14th international conference on Hybrid systems: computation and control, pp. 313-314. ACM, 2011.

[2] Hjalmarsson, H. "From experiment design to closed-loop control." Automatica, 393–43, 2005.

[3] Haesaert, Sofie, Paul M.J. Van den Hof, and Alessandro Abate. "Experiment design for formal verification via stochastic optimal control." Control Conference (ECC), 2016 European. IEEE, 2016.