Improving the Efficiency and Quality of Omega-Regular Synthesis

Sohail, Saqib

Graduate Thesis Or Dissertation

Improving the Efficiency and Quality of Omega-Regular Synthesis Public Deposited

Analytics

Download PDF

Citations

Citeable URL: https://scholar.colorado.edu/concern/graduate_thesis_or_dissertations/mg74qm27m

Abstract

The automatic synthesis of a program from its specification has been an ambitious goal since Alonzo Church asked in 1962 if given a Monadic Second Order (MSO) formula as a logical specification of reactive system with inputs I and outputs O then is it possible to decide where there exists a reactive system that satisfies the specification; and if the specification is realizabile then a reactive system should be generated as a proof. Buechi and Landwaber proved in 1969 that solving the automatic synthesis problem is decidable. While in 1989 Pnueli and Rosner described an automatic synthesis procedure with the best complexity bounds to date. Since then there have been significant advancements in developing methodologies for the automatic synthesis of an arbitrary MSO formula as well as special cases which are practically relevant. The current focus has been on improving the efficiency of the automatic synthesis procedures. However, all the current techniques generate an implementation as a proof which is significantly larger than a handwritten implementation. Thus making the automatic synthesis of reactive systems from a logical specification unattractive for industrial adoption. (In addition, writing a complete logical specification of a reactive system is not a trivial task.) The focus of this thesis is to improve the quality of the implementation generated by an automatic synthesis approach as a proof of realizability of the specification. In all the automatic synthesis approaches, the logical specification is converted to a two player game (the size and complexity of the game is different) where the objective of the antagonist is to find a strategy through which the specification cannot be satisfied while the objective of the protagonist is to find a strategy through which the satisfaction of the specification is guaranteed. In this thesis it is argued that the conversion of the specification to a game is crucial step for both the efficiency of the synthesis approach and quality of the implementation generated as a result. After a thorough investigation into the reasons why the current approaches fail at generating a reasonably sized implementation, a framework has been proposed through which the specification is converted to a significantly more compact game that drastically improves the efficiency and the quality of the implementation generated as a proof. Furthermore, this framework does not compromise the efficiency of the automatic synthesis approach when the specification is restricted to a GR(1) specification. Experiments show the main advantage of the automatic synthesis approach based on this framework. Furthermore, many of the salient features of this framework can be adopted by other automatic synthesis approaches.

Creator