КиСА | Содержание

Том 56 >>> № 5 СЕНТЯБРЬ — ОКТЯБРЬ 2020

УДК 519.713.1

А.Н. Чеботарев

ОТ ФОРМУЛ ВИДА F (t ) ЯЗЫКА LP К – ω-РЕГУЛЯРНЫМ ВЫРАЖЕНИЯМ

Аннотация. При синтезе ∑-автомата, специфицированного в языке LP, возникает задача представления множества обратных сверхслов, задаваемых формулой F (t ), в виде – ω-регулярного выражения. Построение этого выражения основано на соответствии между структурными элементами формул и – ω-регулярных выражений. Для обеспечения такого соответствия введены две дополнительные операции над – ω-регулярными множествами, соответствующие операциям квантификации в формулах. Рассмотрены методы представления этих операций в терминах языка – ω-регулярных выражений. Получены результаты, позволяющие строить – ω-регулярные выражения для достаточно широкого класса формул вида F (t ) языка LP.

Ключевые слова: логика LP, обратное сверхслово, ограниченная справа формула, – ω-регулярное выражение, префиксно замкнутое множество обратных сверхслов.

ПОЛНЫЙ ТЕКСТ

Чеботарев Анатолий Николаевич,
доктор техн. наук, ведущий научный сотрудник Института кибернетики им. В.М. Глушкова НАН Украины, Киев, ancheb@gmail.com

СПИСОК ЛИТЕРАТУРЫ

Чеботарев А.Н. Синтез ∑-автоматов, специфицированных в логических языках LP и LF. Кибернетика и системный анализ. 2018. Т. 54, № 4. С. 16–31.

Чеботарев А.Н. Определение фиктивных состояний в -автомате, синтезированном по спецификации в языке LP. Кибернетика и системный анализ. 2019. Т. 55, № 5. С. 47–57.

Schneider K. Verification of reactive systems. Berlin; Heidelberg; Springer, 2004. 606 p.

Bresolin D., Montanari A., Puppis G. A theory of ultimately periodic languages and automata with an application to time granularity. Acta Informatica. 2009. Vol. 46. P. 331–360.

Cohen-Chesnot. J. On the expressive power of temporal logic for infinite words. Theoretical Computer Science. 1991. Vol. 83, Iss. 2. P. 301–312.