Coherent minimisation: aggressive optimisation for symbolic finite state transducers

[摘要] 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.

[发布机构] University:University of Birmingham;Department:School of Computer Science

[关键词] Q Science;QA Mathematics;QA75 Electronic computers. Computer science