Control Improvisation with Probabilistic Temporal Specifications

TL;DR

This paper introduces a method combining data-driven learning and formal controller synthesis to generate randomized control sequences that mimic human actions while satisfying probabilistic specifications, demonstrated on lighting control in homes.

Contribution

It presents a novel approach integrating generative models with formal specifications for control improvisation in networked systems.

Findings

Produces realistic control sequences similar to human data

Guarantees satisfaction of formal probabilistic specifications

Applicable to home security and resource management

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.