×

From LP formulas of the form \(F(t)\) to \(-\omega \)-regular expressions. (English. Russian original) Zbl 1477.68149

Cybern. Syst. Anal. 56, No. 5, 689-700 (2020); translation from Kibern. Sist. Anal. 2020, No. 5, 3-17 (2020).
Summary: When synthesizing a \(\Sigma \)-automaton specified in the language LP, the problem arises of representing the set of left-infinite words given by a formula \(F(t)\) in the form of a \(-\omega \)-regular expression. Construction of this expression is based on the correspondence between structural elements of formulas and \(-\omega \)-regular expressions. To ensure this correspondence, two additional operations that correspond to the quantification operations in formulas are introduced over \(-\omega \)-regular sets. Methods of representation of these operations in terms of the language of \(-\omega \)-regular expressions are considered. The results obtained allow to construct \(-\omega \)-regular expressions for a rather wide class of LP formulas of the form \(F(t)\).

MSC:

68Q45 Formal languages and automata
03D05 Automata and formal grammars in connection with logical questions
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Chebotarev, AN, Synthesis of Σ-automata specified in the first order logical languages LP and LF, Cybern. Syst. Analysis, 54, 4, 527-540 (2018) · Zbl 1400.68122
[2] Chebotarev, AN, Detecting fictitious states in a Σ-automaton synthesized from its specification in the language LP, Cybern. Syst. Analysis, 55, 5, 742-751 (2019) · Zbl 1448.68261
[3] Schneider, K., Verification of Reactive Systems (2004), Berlin-Heidelberg: Springer, Berlin-Heidelberg
[4] Bresolin, D.; Montanari, A.; Puppis, G., A theory of ultimately periodic languages and automata with an application to time granularity, Acta Informatica, 46, 331-360 (2009) · Zbl 1186.68246
[5] Cohen-Chesnot, J., On the expressive power of temporal logic for infinite words, Theoretical Computer Science, 83, 2, 301-312 (1991) · Zbl 0728.68073
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.