Abstract
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.