TR#: | MSC-2013-13 |

Class: | MSC |

Title: | Weak Omega Automata |

Authors: | Shaked Flur |

Supervisors: | Orna Grumberg |

MSC-2013-13.pdf | |

Abstract: | 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 n*log(n) blow up. More over, we discuss some leads on how to show the quadratic blow up is necessary. |

Copyright | The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information |

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2013/MSC/MSC-2013-13), rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the MSC technical reports of 2013

To the main CS technical reports page