We give new constructions for complementing subclasses of Emerson-Lei automata using modifications of rank-based Büchi automata complementation. In particular, we propose a specialized rank-based construction for a Boolean combination of Inf acceptance conditions, which heavily relies on a novel way of a run DAG labelling enhancing the ranking functions with models of the acceptance condition. Moreover, we propose a technique for complementing generalized Rabin automata, which are structurally as concise as general Emerson-Lei automata (but can have a larger acceptance condition). The construction is modular in the sense that it extends a given complementation algorithm for a condition  \(\varphi \) in a way that the resulting procedure handles conditions of the form  \(\text {Fin}\wedge \varphi \) . The proposed constructions give upper bounds that are exponentially better than the state of the art for some of the classes.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Complementation of Emerson-Lei Automata

  • Vojtěch Havlena,
  • Ondřej Lengál,
  • Barbora Šmahlíková

摘要

We give new constructions for complementing subclasses of Emerson-Lei automata using modifications of rank-based Büchi automata complementation. In particular, we propose a specialized rank-based construction for a Boolean combination of Inf acceptance conditions, which heavily relies on a novel way of a run DAG labelling enhancing the ranking functions with models of the acceptance condition. Moreover, we propose a technique for complementing generalized Rabin automata, which are structurally as concise as general Emerson-Lei automata (but can have a larger acceptance condition). The construction is modular in the sense that it extends a given complementation algorithm for a condition  \(\varphi \) in a way that the resulting procedure handles conditions of the form  \(\text {Fin}\wedge \varphi \) . The proposed constructions give upper bounds that are exponentially better than the state of the art for some of the classes.