Complementation of – ω-Regular Expressions. I

When using ω-regular expressions in the verification and synthesis of reactive systems, the problem of complementing these expressions arises, which is related to the language containment problem. To this end, an ω-regular language is usually defined by an A-automaton, and the automaton is constructed that recognizes the complement of the ω-regular language defined by an automaton A. In this paper, instead of ω-regular expressions, we consider symmetric –ω-regular expressions based on the notion of reverse word (ω-word). The transition from the algorithm for complementing a –ω-regular expression to the corresponding algorithm for an ω-regular expression consists in replacing the notions used by the notions symmetric to them. We consider the problem of the direct transition from the regular expression that defines a –ω-regular language to the –ω-regular expression that defines the complement of this language. Among ω-regular expressions, we distinguish three disjoint classes, for each of which we develop an algorithm to complements –ω-regular expressions that belong to this class. This significantly simplifies solving the problem under consideration. In this paper, we consider a class of –ω-regular expressions of the form Σ^−ωR, where R ∈ Σ^* and does not have the form R₁Σ^*.