Recent Challenges and Ideas in Temporal Synthesis

In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification against all environments. While modelchecking theory has led to industrial development and use of formal-verification tools, the integration of synthesis in the industry is slow. This has to do with theoretical limitations, like the complexity of the problem, algorithmic limitations, like the need to determinize automata on infinite words and solve parity games, methodological reasons, like the lack of satisfactory compositional synthesis algorithms, and practical reasons: current algorithms produce systems that satisfy the specification, but may do so in a peculiar way and may be larger or less wellstructured than systems constructed manually. The research community has managed to suggest some solutions to these limitations, and bring synthesis algorithms closer to practice. Significant barriers, however, remain. Moreover, the integration of synthesis in real applic...

• Type: Journal
• Year: 2012
• Where: SOFSEM
• Authors: Orna Kupferman
• Keywords: Problem Algorithms, SOFSEM 2012, Synthesis Algorithms, Synthesis Problem, Theoretical Computer Science