Control Improvisation for Probabilistic Temporal Specifications

Ilge Akkaya, Daniel Fremont, Rafael Valle, Alexandre Donzé, Edward A. Lee, and Sanjit A. Seshia. Control Improvisation for Probabilistic Temporal Specifications. In Proceedings of the 1st IEEE International Conference on Internet-of-Things Design and Implementation (IoTDI), April 2016.
Best Paper Award.

Download

[pdf] 

Abstract

We consider the problem of generating randomized control sequences for complex networked systems typically actuated by human agents. Our approach leverages a concept known as control improvisation, which is based on a combination of data-driven learning and controller synthesis from formal specifications. We learn from existing data a generative model (for instance, an explicit-duration hidden Markov model, or EDHMM) and then supervise this model in order to guarantee that the generated sequences satisfy some desirable specifications given in Probabilistic Computation Tree Logic (PCTL). We present an implementation of our approach and apply it to the problem of mimicking the use of lighting appliances in a residential unit, with potential applications to home security and resource management. We present experimental results showing that our approach produces realistic control sequences, similar to recorded data based on human actuation, while satisfying suitable formal requirements.

BibTeX

@inproceedings{akkaya-iotdi16,
  author    = {Ilge Akkaya and Daniel Fremont and Rafael Valle and Alexandre Donz{\'{e}} and Edward A. Lee and Sanjit A. Seshia},
  title     = {Control Improvisation for Probabilistic Temporal Specifications},
  booktitle = {Proceedings of the 1st IEEE International Conference on Internet-of-Things Design and Implementation (IoTDI)},
  Year = {2016},
  Month = {April},
  OPTpages = {55--70},
  wwwnote = {<b>Best Paper Award</b>.},
  abstract = {We consider the problem of generating randomized 
control sequences for complex networked systems typically 
actuated by human agents. Our approach leverages a 
concept known as control improvisation, which is based on a 
combination of data-driven learning and controller synthesis 
from formal specifications. We learn from existing data a 
generative model (for instance, an explicit-duration hidden 
Markov model, or EDHMM) and then supervise this model in 
order to guarantee that the generated sequences satisfy some 
desirable specifications given in Probabilistic Computation Tree 
Logic (PCTL). We present an implementation of our approach 
and apply it to the problem of mimicking the use of lighting 
appliances in a residential unit, with potential applications to 
home security and resource management. We present experimental 
results showing that our approach produces realistic 
control sequences, similar to recorded data based on human 
actuation, while satisfying suitable formal requirements.},
}