Abstract
Synchronous modeling is at the heart of programming languages like Lustre, Esterel, or SCADE used routinely for implementing safety critical control software, e.g., fly-by-wire and engine control in planes. However, to date these languages have had limited modern support for modeling uncertainty - probabilistic aspects of the software's environment or behavior - even though modeling uncertainty is a primary activity when designing a control system.
In this talk, we present ProbZelus, a synchronous probabilistic programming language. ProbZelus conservatively provides the facilities of a synchronous language to write control software as stream processors, with probabilistic constructs to model uncertainties and perform inference-in-the-loop. We discuss the design and semantics of the language, and propose a semi-symbolic inference algorithm based on delayed sampling for efficient streaming inference. We also present a static analysis that can check if a ProbZelus program will execute in bounded memory under delayed sampling, a key property for reactive systems which never stop.
