Spring 2021

Synthesis for Correctness Is Not Enough: How to Specify, Verify, and Synthesize Robust Systems

Monday, Apr. 26, 2021 9:00 am9:30 am

Add to Calendar



While most synthesis approaches address system correctness, ensuring robustness has remained a challenge. In this talk we introduce the logic rLTL (robust LTL) which provides a means to formally reason about both correctness and robustness in system design. We will review the decidability and complexity of the verification and synthesis problems for rLTL and its fragments, and report on several case studies illustrating its usefulness in practice.