О задаче верификации для одного класса автоматов реального времени

В. А. Захаров; Винарский Е. М.

?

О задаче верификации для одного класса автоматов реального времени

С. 257–260.

Захаров В. А., Винарский Е. М.

Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных автоматов; для моделирования течения времени автомат дополняется специальной вещественной переменной. Таким образом, воникает модель машин с конечным числом состояний, обрабатывающей потоки данных в реальном времени (TFSMs). Целью наших исследований является задача проверки выполнимости некоторых поведенческих свойств TFSMs, зависящих не только от соответствий между последовательностями входных сигналов и выходных сигналов, но также от времени их поступления и времени, затраченного на их обработку. Для формального описания мы предлагаем использовать новое расширение LP-RLTL темпоральной логики линейного времени LTL. В основу LP-RLTL положены идеи, предложенные и развитые авторами ранее для решения задачи верификации последовательных реагирующих систем.

Язык: русский

Текст на другом сайте

Ключевые слова: разрешимость model checking верификация моделей программ темпоральная логика decidability real time automata конечный автомат реального времени temporal logic

ПУБЛИКАЦИЯ ПОДГОТОВЛЕНА ПО РЕЗУЛЬТАТАМ ПРОЕКТА:

Методы синтеза, исправления, проверки соответствия и анализа моделей процессов и распределенных информационных систем (2019)

В книге

Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019)

М.: Изд-во механико-математического факультета МГУ, 2019.

О вычислительных аспектах максимальной специфичности в вероятностном объяснении

Сперанский С. О., Вестник Новосибирского государственного университета. Серия: Математика, механика, информатика 2011 Т. 11 № 4 С. 78–93

В настоящей статье изучаются вычислительные аспекты формального требования максимальной специфичности, накладываемого на правила в языке пропозициональной классической логики, когда над этим языком задана вычислимая рационально-значная вероятностная мера. Доказана неразрешимость ряда общих проблем по обнаружению максимально специфичных правил и вероятностных мер, для которых совокупность всех специфичных правил вычислима; установлена разрешимость множества максимально специфичных правил при неких ...

Добавлено: 27 декабря 2025 г.

Квантификация по пропозициональным формулам в вероятностной логике: вопросы разрешимости

Сперанский С. О., Алгебра и логика 2011 Т. 50 № 4 С. 533–546

Язык для рассуждений о вероятности обобщается за счёт добавления в него кванторов по пропозициональным формулам. Далее рассматриваются соответствующие вопросы разрешимости. В частности, представленные результаты демонстрируют неразрешимость проблемы общезначимости для довольно слабого фрагмента нового языка. С другой стороны, устанавливается разрешимость ограниченной проблемы общезначимости для АЕ-предложений. ...

Добавлено: 27 декабря 2025 г.

Complexity for probability logic with quantiﬁers over propositions

Сперанский С. О., Journal of Logic and Computation 2013 Vol. 23 No. 5 P. 1035–1055

In the present article, the quantifiers over propositions are first introduced into the language for reasoning about probability, then the complexity issues for validity problems dealing with the corresponding hierarchy of probabilistic sentences are investigated. We prove, among other things, the $\Pi^1_1$-completeness for the general validity and also indicate the least level in the hierarchy ...

Добавлено: 27 декабря 2025 г.

A note on definability in fragments of arithmetic with free unary predicates

Сперанский С. О., Archive for Mathematical Logic 2013 Vol. 52 No. 5–6 P. 507–516

We carry out a study of definability issues in the standard models of Presburger and Skolem arithmetics (henceforth referred to simply as Presburger and Skolem arithmetics, for short, because we only deal with these models, not the theories, thus there is no risk of confusion) supplied with free unary predicates — which are strongly related to definability in ...

Добавлено: 27 декабря 2025 г.

On the decision problem for quantified probability logics

Сперанский С. О., Izvestiya. Mathematics 2025 Vol. 89 No. 3 P. 193–211

Let QPL-e expand the quantifier-free ‘polynomial’ probability logic of [Fagin et al. 1990] by adding quantifiers over arbitrary events; it can be viewed as a one-sorted elementary language for reasoning about probability spaces. We prove that the $\Sigma_2$-fragment of the QPL-e-theory of finite spaces is hereditarily undecidable. By earlier observations, this implies that $\Pi_2$ is the ...

Добавлено: 26 декабря 2025 г.

An ‘elementary’ perspective on reasoning about probability spaces

Сперанский С. О., Logic Journal of the IGPL 2025 Vol. 33 No. 2 Article jzae042

This paper is concerned with a two-sorted probabilistic language, denoted by QPL, which contains quantifiers over events and over reals, and can be viewed as an elementary language for reasoning about probability spaces. The fragment of QPL containing only quantifiers over reals is a variant of the well-known ‘polynomial’ language from [Fagin et al. 1990, Section 6]. ...

Добавлено: 26 декабря 2025 г.

Variations on the Kripke trick

Рыбаков М. Н., Shkatov D., Studia Logica 2025 Vol. 113 P. 1–48

Добавлено: 2 декабря 2023 г.

РАЗРЕШИМОСТЬ ТЕОРИИ КОНЕЧНЫХ ПОДМНОЖЕСТВ БЕЗАТОМНЫХ БУЛЕВЫХ АЛГЕБР

Дудаков С. М., Авхимович Н. В., Вестник Тверского государственного университета. Серия: Прикладная математика 2023 № 1 С. 24–35

В работе рассматриваются алгебраические системы, где в качестве носителя выступают конечные подмножества некоторой безатомной булевой алгебры. Для полученной системы мы вводим новое отношение для конечных подмножеств: считаем, что одно подмножество состоит в отношении с другим подмножеством в том и только том случае, когда все элементы одного подмножества меньше всех элементов другого. Мы демонстрируем, что теория ...

Добавлено: 12 ноября 2023 г.

Algorithmic properties of modal and superintuitionistic logics of monadic predicates over finite Kripke frames

Рыбаков М. Н., Shkatov D., Journal of Logic and Computation 2025 Vol. 35 No. 2 Article exad078

Добавлено: 3 ноября 2023 г.

Algorithmic complexity of monadic multimodal predicate logics with equality over finite Kripke frames

Агаджанян И. А., Рыбаков М. Н., Шкатов Д. П., / Series arXiv "math". 2023.

Добавлено: 7 июля 2023 г.

Решетка определимости. Источники и направления исследований

Семенов А. Л., Сопрунов С. Ф., Чебышевский сборник 2021 Т. 22 № 1(77) С. 304–327

В статье представлены результаты и открытые проблемы, относящиеся к пространствам определимости (редуктам), а также источникам этой области, начиная с XIX века. Исследуются условия конечности и ограничения, в том числе глубина чередования кванторов и число аргументов. Описаны результаты, относящиеся к описанию решеток пространств определимости для числовых и других естественных структур. Методы исследования включают изучение групп автоморфизмов ...

Добавлено: 11 марта 2023 г.

Ломазова И. А., Vladimir A. Bashkin, Jančar P., Fundamenta Informaticae 2022 Vol. 186 No. 1-4 P. 175–194

Добавлено: 4 сентября 2022 г.

Merging Epistemic and Temporal Models: a History-Free Approach

Попова Е. Л., Логико-философские штудии 2022 Vol. 20 No. 1 P. 1–7

Добавлено: 1 августа 2022 г.

On the Model Checking Problem for Some Extension of CTL*

Гнатенко А. Р., Захаров В. А., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776–785

Добавлено: 17 января 2022 г.

On the Modeling of Sequential Reactive Systems by Means of Real Time Automata

Винарский Е. М., Захаров В. А., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 751–762

Добавлено: 17 января 2022 г.

О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени

Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356–371

К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, ...

Добавлено: 17 января 2022 г.