COMPLEMENTATION OF –ω-REGULAR EXPRESSIONS. I
A.N. Chebotarev · Kibernetyka ta Systemnyi Analiz · 2024
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, a ω-regular language is usually defined by a ω-automaton A, and the automaton is constructed that recognizes the complement of the language defined by 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 a ω-regular expression consists in replacing the notions used by the notions symmetric to them. We consider the problem of the direct transition of 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 non-intersecting classes, for each of which we develop an algorithm to complement –ω-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∑*. Keywords: –ω-regular expression, complement of the –ω-regular expression, suffix of the regular expression, alphabet ∑′, contiguous words, contiguity condition.