DOI
10.34229/KCA2522-9664.24.6.3
UDC 519.713.1
1 V.M. Glushkov Institute of Cybernetics, National Academy of Sciences of Ukraine, Kyiv, Ukraine
ancheb@gmail.com
|
|
COMPLEMENTATION OF –ω-REGULAR EXPRESSIONS. I
Abstract. 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.
full text
REFERENCES
- 1. Kupferman O., Vardi M. Complementation constructions for nondeterministic automata on infinite words. Proc. TACAS’05. Lecture Notes Comput. Sci. 2005. Vol. 3440. P. 206–211. URL: https://doi.org/10.1007/ 978-3-540-31980-1_14 .
- 2. Fogarty S., Kupferman O., Vardi M., Wilke T. Unifying Buchi complementation constructions. Logical Methods in Computer Science. 2011. Vol. 9, N 1. P. 248–263. URL: https://doi.org/10.2168/LMCS-9(1:13)2013 .
- 3. Vardi M.Y., Fogarty S., Yong Li, Yih-Kuen Tsay. Towards a grand unification of Bchi ñomplementation ñonstructions. In: Principles of Systems Design. LNCS. 2022. Vol. 13660. P. 185–207. URL: https://doi.org/10.1007/978-3-031-22337-2_9 .
- 4. Chebotarev A.N. Synthesis of -automata specified in the first order logical languages LP and LF. Cybernetics and Systems Analysis. 2018. Vol. 54, N 4. P. 527–540. URL: https://doi.org/10.1007/ s10559-018-0054-8 .
- 5. Chebotarev A.N. Detecting fictitious states in a #-automaton synthesized from the specification in the language LP. Cybernetics and Systems Analysis. 2019. Vol. 55, N 5. P. 742–751. URL: https://doi.org/10.1007/s10559-019-00184-x .
- 6. Diekert V., Gastin P. First-order definable languages. In: Logic and Automata: History and Perspectives. Flum J., Grdel E., Wilke T. (Eds.). Amsterdam University Press, 2007. P. 261–306.
- 7. Pin J.-E., Perrin D. Infinite words: Automata, semigroups, logic and games. Pure and Applied Mathematics Series. Vol. 141. Amsterdam: Academic Press, 2004. 550 p.
- 8. Chebotarev A.M. Intersection of ω-regular expressions. Kibernetyka ta systemnyi analiz. 2021. Vol. 57, N 5. P. 12–21.