Quantitative Specifications for Reactive Systems

In this project, we attempt to construct a quantitative specification framework for analysis of reactive systems. Our framework is built on a novel notion called simulation distances. A simulation distance measures some aspect of «match» of a given system with respect to a property. The «match» could be anything including a measure of correctness (how often the system violates the property) or robustness (how much can the system be externally disturbed before it violates the property). We give algorithms to synthesize optimal systems with respect to this quantitative specifications. A large fraction of this project was a part of my dissertation which was awarded the 2014 ACM SIGBED Paul Caspi Memorial Dissertation Award. The award is presented annually to the author of an outstanding dissertation in the area of Embedded Systems to recognize work that significantly advances the state of the art in the science of embedded systems, in the spirit and legacy of Dr. Paul Caspi’s work.