@InProceedings{Sukkerd/2015/SEFM,
      AUTHOR = {Sukkerd, Roykrong and Garlan, David and Simmons, Reid},
      TITLE = {Task Planning of Cyber-Human Systems},
      YEAR = {2015},
      MONTH = {7-11 September},
      BOOKTITLE = {Proceedings of the 13th International Conference on Software Engineering and Formal Methods},
      VOLUME = {9276},
      SERIES = {LNCS },
      ADDRESS = {York, UK},
      PUBLISHER = {Springer},
      PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/SEFM15_Sukkerd_Springer.pdf},
      ABSTRACT = {Internet of Things (IoT) allows for cyber-physical applications to be created and composed to provide intelligent support or automation of end-user tasks. For many of such tasks, human participation is crucial to the success and the quality of the tasks. The cyber systems should proactively request help from the humans to accomplish the tasks when needed. However, the outcome of such system-human synergy may be affected by factors external to the systems. Failure to consider those factors when involving human participants in the tasks may result in suboptimal performance and negative experience on the humans. In this paper, we propose an approach for automated generation of control strategies of cyber-human systems. We investigate how explicit modeling of human participant can be used in automated planning to generate cooperative strategy of human and system to achieve a given task, by means of which best and appropriately utilize the human. Specifically, our approach consists of: (1) a formal framework for modeling cooperation between cyber system and human, and (2) a formalization of system-human cooperative task planning as strategy synthesis of stochastic multiplayer game. We illustrate our approach through an example of indoor air quality control in smart homes.},
      KEYWORDS = {Activity-oriented Computing, Cyberphysical Systems, Human-in-the-loop, Model Checking, Ubiquitous Computing}
}