КіСА | Зміст

Том 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.