SURF 2018: Test design for temporal logic controllers - Revision history

Haesaert at 07:06, 16 December 2017

2017-12-16T07:06:57Z

← Older revision		Revision as of 07:06, 16 December 2017
Line 27:		Line 27:
	'''References'''		'''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.		[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,		[2] Hjalmarsson, H. "From experiment design to closed-loop control." Automatica,

Haesaert at 07:05, 16 December 2017

2017-12-16T07:05:37Z

← Older revision		Revision as of 07:05, 16 December 2017
Line 18:		Line 18:
	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].		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 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.		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		Familiarity with the following topics is a bonus

Haesaert at 07:05, 16 December 2017

2017-12-16T07:05:06Z

← Older revision		Revision as of 07:05, 16 December 2017
Line 29:		Line 29:
	[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.		[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~~. (2005)~~. "From experiment design to closed-loop control." Automatica,		[2] Hjalmarsson, H. "From experiment design to closed-loop control." Automatica,
	393–43		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.		[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.

Haesaert at 07:04, 16 December 2017

2017-12-16T07:04:24Z

← Older revision		Revision as of 07:04, 16 December 2017
Line 16:		Line 16:
	the use of uncertain control models built from data is a common		the use of uncertain control models built from data is a common
	practice [2].		practice [2].
	Since these data-driven models are an empirical approximation it is important to test the designed controllers ~~for these physical system~~ before implementation. The design of experiments that ~~allow~~ for the verification of formal properties can be formulated as an stochastic optimal control problem [3].		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 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.		In this study the objective is to research smart ways of testing these 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.
Line 26:		Line 26:

	'''References'''		'''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.		[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.

Haesaert at 07:03, 16 December 2017

2017-12-16T07:03:06Z

Haesaert: Created page with "'''2018 SURF: project description''' * Mentor: Richard M. Murray * Co-mentor: Sofie Haesaert The design of complex, high-tech, safety-critical systems such as a..."

2017-12-16T07:02:17Z

Created page with "'''2018 SURF: project description''' * Mentor: Richard M. Murray * Co-mentor: Sofie Haesaert The design of complex, high-tech, safety-critical systems such as a..."

New page

'''[[SURF 2018|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. %and of correct-by-design synthesis.
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 for these physical system before implementation. The design of experiments that allow 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 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. (2005). "From experiment design to closed-loop control." Automatica,
393–43
[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.

← Older revision		Revision as of 07:03, 16 December 2017
Line 9:		Line 9:
	can be attained by the use of temporal logics in the specification and design of their controllers [1].		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		The use such formal methods carries the promise of a decrease in design
	faults and implementation errors~~. %and of correct-by-design synthesis~~.		faults and implementation errors.
	In practice, for most physical
	systems the dynamical behavior is known only in part: this holds		In practice, for most physical systems the dynamical behavior is known only in part: this holds
	in particular with biological systems		in particular with biological systems
	or with classes of engineered systems where, as a consequence,		or with classes of engineered systems where, as a consequence,
Line 27:		Line 27:
	'''References'''		'''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.		[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. (2005). "From experiment design to closed-loop control." Automatica,		[2] Hjalmarsson, H. (2005). "From experiment design to closed-loop control." Automatica,
	393–43		393–43

	[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.		[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.