1 V.M. Glushkov Institute of Cybernetics, National Academy of Sciences of Ukraine, Kyiv, Ukraine |
Abstract. In synthesis of a ∑-automaton specified in the language LP, the problem arises how to represent the set of left-infinite words defined by the formula F (t ) in the form of a – ω-regular expression. Construction of this representation is based on the correspondence between structural components of formulas and – ω-regular expressions. To provide such a correspondence, two additional operations on – ω-regular sets relating to the operation of quantification in formulas are introduced. The paper focuses on the representation of these operations in terms of the – ω-regular language. The results presented in this paper allow constructing – ω-regular expressions for a wide class of LP formulas of the form F (t ).
Keywords: logic LP, left-infinite word, right-bounded formulas, – ω-regular expression, prefix closed set of left-infinite words.