A.N. CHEBOTEREV,
V.M. Glushkov Institute of Cybernetics, National Academy of Sciences of Ukraine, Kyiv, Ukraine
ancheb@gmail.com
Abstract. In synthesis of a –ω-automaton specified in the LP language, the problem arises how to represent the set of –ω-words defined by a formula F(t) in the form of a –ω-regular expression. Construction of this representation is based on the correspondence between structural components of the formulas and –ω-regular expressions. To provide such a correspondence, two additional operations on –ω-regular sets relating to the operation of quantification in the formulas were introduced. The problem was reduced to calculating the –ω-regular expressions defined by these operations. This calculation relies on the construction of an elementary extensions graph, in which certain set of infinite paths corresponds to all –ω-words that belong to the –ω-set to be calculated. A method for constructing a –ω-regular expression specified by such a graph is proposed in the paper. This method is based on the solution of a system of linear equations over –ω-regular sets.
Keywords: : –ω-word, –ω-regular expression, prefix-closed set of –ω-words, elementary extensions graph, linear equations over –ω-regular sets.