Polynomial time algorithms for inclusion and equivalence of deterministic omega acceptors

TL;DR

This paper presents polynomial time algorithms for deciding inclusion and equivalence of deterministic omega acceptors, such as DPAs and DMAs, which are key for verifying omega language properties efficiently.

Contribution

It introduces the first polynomial time algorithms for inclusion and equivalence problems of deterministic parity and Muller acceptors, extending to Buechi and coBuechi cases.

Findings

Polynomial algorithms for inclusion of two DPAs and two DMAs

Polynomial algorithms for equivalence of DPAs and DMAs

Efficient methods for inclusion and equivalence of deterministic Buechi and coBuechi acceptors

Abstract

The class of omega languages recognized by deterministic parity acceptors (DPAs) or deterministic Muller acceptors (DMAs) is exactly the regular omega languages. The inclusion problem is the following: given two acceptors A1 and A2, determine whether the language recognized by A1 is a subset of the language recognized by A2, and if not, return an ultimately periodic omega word accepted by A1 but not A2. We describe polynomial time algorithms to solve this problem for two DPAs and for two DMAs. Corollaries include polynomial time algorithms to solve the equivalence problem for DPAs and DMAs, and also the inclusion and equivalence problems for deterministic Buechi and coBuechi acceptors.