CDS Seminar: Robust discrete synthesis against unspecified disturbances

Elaine Render
Postdoc, UCLA

Systems working in uncertain environments should possess a robustness property, which ensures that the behaviours of the system remain close to the original behaviours under the influence of unmodeled, but bounded, disturbances.
We present a formal definition of robustness and algorithmic tools for the design of optimally robust controllers for omega-regular properties on discrete transition systems.
Formally, we define metric automata - automata equipped with a metric on states - and strategies on metric automata which guarantee robustness for omega-regular properties. We present graph-theoretic algorithms to construct such strategies in polynomial time. In contrast to strategies computed by classical automata-theoretic algorithms, the strategies computed by our algorithm ensure that the behaviours of the controlled system under disturbances satisfy a related property which depends on the magnitude of the disturbance.
We show an application of our theory to the design of controllers that tolerate infinitely many transient errors provided they occur infrequently enough.