Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis

Shaull Almagor, Orna Kupferman, Yaron Velner

In Boolean synthesis, we are given an LTL specification, and the goal is to construct a transducer that realizes it against an adversarial environment. Often, a specification conta…