Synthesis for Human-in-the-Loop Control Systems

Wenchao Li, Dorsa Sadigh, S. Shankar Sastry, and Sanjit A. Seshia. Synthesis for Human-in-the-Loop Control Systems. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 470–484, April 2014.

Download

[pdf] 

Abstract

Several control systems in safety-critical applications involve the interaction of an autonomous controller with one or more human operators. Examples include pilots interacting with an autopilot system in an aircraft, and a driver interacting with automated driver-assistance features in an automobile. The correctness of such systems depends not only on the autonomous controller, but also on the actions of the human controller. In this paper, we present a formalism for human-in-the-loop (HuIL) control systems. Particularly, we focus on the problem of synthesizing a semi-autonomous controller from high-level temporal specifications that expect occasional human intervention for correct operation. We presentan algorithm for this problem, and demonstrate its operation on problems related to driver assistance in automobiles.

BibTeX

@inproceedings{li-tacas14,
  author    = {Wenchao Li and Dorsa Sadigh and S. Shankar Sastry and Sanjit A. Seshia},
  title     = {Synthesis for Human-in-the-Loop Control Systems},
 booktitle = {Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
 month = "April",
 year = {2014},
  pages = {470--484},
  abstract = {Several control systems in safety-critical applications involve the interaction 
of an autonomous controller with one or more human operators. Examples 
include pilots interacting with an autopilot system in an aircraft, and a driver 
interacting with automated driver-assistance features in an automobile. The correctness 
of such systems depends not only on the autonomous controller, but also 
on the actions of the human controller. In this paper, we present a formalism for 
human-in-the-loop (HuIL) control systems. Particularly, we focus on the problem 
of synthesizing a semi-autonomous controller from high-level temporal specifications 
that expect occasional human intervention for correct operation. We present
an algorithm for this problem, and demonstrate its operation on problems related 
to driver assistance in automobiles.},
}