Synthesis of Protocols and Discrete Controllers

Husien, IM (2017) Synthesis of Protocols and Discrete Controllers. PhD thesis, University of Liverpool.

Text 201006903_Nov2017.pdf - Unspecified Download (1MB)

Abstract

In this thesis, a number of search techniques are proposed as a solution for program and discrete controller synthesis (DCS). Classic synthesis techniques facilitate exhaus- tive search, while genetic programming has recently proven the potential of generic search techniques. But is genetic programming the right search technique for the synthesis prob- lem? In this thesis we challenge this belief and argue in favor of simulated annealing, a different class of general search techniques. We show that, in hindsight, the success of genetic programming has drawn from what is arguably a hybrid between simulated annealing and genetic programming, and compare the fitness of classic genetic program- ming, the hybrid form, and pure simulated annealing. Our experimental evaluation suggests that pure simulated annealing offers better results for automated programming than techniques based on genetic programming. Discrete Controller Synthesis (DCS) and Program Synthesis have similar goals: they are automated techniques to infer a control strategy and an implementation, respectively, that is correct by construction. We also investigate the application of the search tech- niques that we have been used for program synthesis for the computation of deterministic strategies solving symbolic Discrete Controller Synthesis (DCS) problems, where a model of the system under control is given along with desired objective behaviours. We experi- mentally confirm that relative performance results are similar to program synthesis, and give a complexity analysis of our simulated annealing algorithm for symbolic DCS. From the performance results we obtain, we draw the conclusion that simulated annealing, when combined with efficient model-checking techniques, is worth further investigating to solve symbolic DCS problems. A tool is designed to explore the parameter space of different synthesis techniques. Besides using it to synthesise a discrete control strategies for reactive systems (controller synthesis) and for protocol adapters for the coordination of different threads (software synthesis), we can also use it to study the influence of turning various screws in the syn- thesis process. For simulated annealing, PranCS allows the user to define the behaviour of the cooling schedule. For genetic programming, the user can select the population size.

Item Type:	Thesis (PhD)
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	19 Dec 2017 08:51
Last Modified:	19 Jan 2023 06:50
DOI:	10.17638/03012297
Supervisors:	Sven Schewe, Prof Dominik Wojtczak, Dr
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3012297