Coherent minimisation: aggressive optimisation for symbolic finite state transducers

Al-Zobaidi, Zaid (2014). Coherent minimisation: aggressive optimisation for symbolic finite state transducers. University of Birmingham. Ph.D.

Preview

Al-Zobaidi14PhD.pdf
PDF - Accepted Version
Download (1MB)

Abstract

Automata minimisation is considered as one of the key computational resources that drive the cost of computation. Most of the conventional minimisation techniques are based on the notion of bisimulation to determine equivalent states which can be identified.

Although minimisation of automata has been an established topic of research, the optimisation of automata works in constrained environments is a novel idea which we will examine in this dissertation, along with a motivating, non-trivial application to efficient tamper-proof hardware compilation.

This thesis introduces a new notion of equivalence, coherent equivalence, between states of a transducer. It is weaker than the usual notions of bisimulation, so it leads to more states being identified as equivalent. This new equivalence relation can be utilised to aggressively optimise transducers by reducing the number of states, a technique which we call coherent minimisation. We note that the coherent minimisation always outperforms the conventional minimisation algorithms. The main result of this thesis is that the coherent minimisation is sound and compositional.

In order to support more realistic applications to hardware synthesis, we also introduce a refined model of transducers, which we call symbolic finite states transducers that can model systems which involve very large or infinite data-types.

Type of Work:

Thesis (Doctorates > Ph.D.)

Award Type:

Doctorates > Ph.D.

Supervisor(s):