The Taub Faculty of Computer Science Events and Talks

Automata over infinite words are a core concept in program verification. Many different types of automata exist and they can be classified by the type of their transition relation and by the type of their acceptance condition. In this thesis we explore weak automata over infinite words. In weak automata the state space is partitioned into partially ordered sets. The transition relation is then restricted so that a state from one set can only move to states in partitions lower in the order. More over, the states in each partition are either all accepting states, or all non-accepting states. These restriction give weak automata a structure which makes reasoning about easier. Hence the translation from different kinds of automata to weak automata is of interest. We show that when a translation from deterministic Buchi automata to deterministic weak automata with k partitions is possible, it involves only very simple modifications to the original automaton. In particular, the state space and the transition function are untouched. More over, we show that restricting the number of partitions in deterministic weak automata also restricts their expression power. This comes as a sharp contrast to the translation of alternating Buchi automata to alternating weak automata where translation is always possible but involves a quadratic blow up in the state space. We present such quadratic translation and provide a proof that it can not be improved to less then nlog(n) blow up. More over, we discuss some leads on how to show the quadratic blow up is necessary.