Transforming Undecidable Synthesis Problems into Decidable Problems
Synthesis holds the promise to revolutionize the development ofcomplex systems by automating the translation from specifications toimplementations. Synthesis algorithms are based on the same level ofmathematical rigor as verification algorithms but can be applied atearlier development stages, when only parts of the design areavailable. Given a formal specification of the desired systemproperties, for example in a temporal logic, we determine if thepartial design can be completed into a full design that satisfies theproperties.For general distributed systems, the synthesis problem is undecidable.However, there has been a sequence of discoveries where thedecidability was established for specific system architectures, suchas pipelines and rings, or other restrictions on the problem, such aslocal specifications. Encouraged by these findings, new specificationlanguages like Coordination Logic aim for a uniform treatment of thesynthesis problem.In this talk, I will review several techniques that transformundecidable synthesis problems into decidable problems.
