Sumit Nain, Automated synthesis from probabilistic components

In automated verification, we aim to prove that a given system satisfies its specification. Synthesis aims to avoid verification by using the specification to guide the construction of a model that satisfies the specification. In the classical approach to synthesis, the desired system is constructed from scratch. However, real-world systems are usually built from reusable components. This motivates the component-based approach to synthesis, where the system is automatically generated using components from a fixed library. In this case, the desired outcome is a finite state controller that co-ordinates between the available components. In the probabilistic setting, the components are probabilistic transducers.