Cybernetics And Systems Analysis logo
Editorial Board Announcements Abstracts Authors Archive
KIBERNETYKA TA SYSTEMNYI ANALIZ
International Theoretical Science Journal
-->

DOI 10.34229/KCA2522-9664.24.6.3
UDC 519.713.1
A.N. Chebotarev1


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.




© 2024 Kibernetika.org. All rights reserved.