?
On the model checking of sequential reactive systems
P. 233-244.
Захаров В. А., Kozlova D.
Ключевые слова: model checkingfinite state transducerконечный автомат-преобразовательверификация моделей программтемпоральная логикаtemporal logic
ПУБЛИКАЦИЯ ПОДГОТОВЛЕНА ПО РЕЗУЛЬТАТАМ ПРОЕКТА:
В книге
Vol. 1698. , Humboldt-Universität zu Berlin, 2016
Захаров В. А., Козлова Д. Г., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 204-206.
Характерная особенность моделей Крипке и большинства темпоральных логик (PLTL, CTL, PDL, mu-исчисление и др.), используемых в качестве формальных языков спецификации, состоит в том, что элементарные свойства вычислений зависят только от состояний модели, но не от вычислений, которыми достигаются состояния. Однако для стороннего наблюдателя поведение реагирующей системы проявляется в соответствии между последовательностями стимулов (сигналов), которыми внешняя ...
Добавлено: 13 октября 2016 г.
Гнатенко А. Р., Захаров В. А., В кн. : Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). : М. : Изд-во механико-математического факультета МГУ, 2019. С. 263-266.
Описаны синтаксис и семантика нового расширения Reg-CTL* темпоральной логики деревьев вычислений CTL*, предназначенного для спецификации и верификации вычислений последовательных реагирующих систем. Поеказано, что задача верификации моделей автоматов-преобразователей относительно выполнимости формул логики CTL* является PSPACE-полной. ...
Добавлено: 17 октября 2019 г.
Гнатенко А. Р., Захаров В. А., В кн. : Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды. : МГУ, МАКС Пресс, 2018. С. 131-133.
Проведено сравнение выразительных возможностей темпоральной логики LP-CTL*. В этой логике были выделены два класса формул (фрагмента) LP-1-LTL и LP-n-LTL и показано, что фрагмент LP-1-LTL превосходит по выразительным возможностям известную темпоральную логику линейного времени LTL, а фрагмент LP-n-LTL имеет такие же выразительные возможности, что и монадическая логика второго порядка с одной функцией следования S1S. ...
Добавлено: 14 июня 2018 г.
Гнатенко А. Р., Захаров В. А., Proceedings of the Institute for System Programming of the RAS 2018 Vol. 30 No. 3 P. 303-324
Добавлено: 14 июня 2018 г.
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356-371
К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, ...
Добавлено: 17 января 2022 г.
Гнатенко А. Р., Захаров В. А., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776-785
Добавлено: 17 января 2022 г.
Гнатенко А. Р., Захаров В. А., Системная информатика 2020 Vol. 17 P. 21-32
Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться ...
Добавлено: 9 ноября 2020 г.
Захаров В. А., Винарский Е. М., В кн. : Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). : М. : Изд-во механико-математического факультета МГУ, 2019. С. 257-260.
Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных ...
Добавлено: 17 октября 2019 г.
Захаров В. А., Гнатенко А. Р., , in : Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018. : Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018. P. 29-36.
Добавлено: 26 октября 2018 г.
Захаров В. А., Гнатенко А. Р., В кн. : Проблемы теоретической кибернетики: XVIII международная конференция (Пенза, 19-23 июня 2017 г.). : М. : МГУ, МАКС Пресс, 2017. С. 68-71.
В статье в качестве формальной модели последовательных реагирующих систем была предложена модель вычислений конечных автоматов-преобразователей, работающих над полугруппами действий. Для спецификации поведений таких автоматов был предложен специальный вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для параметризации темпоральных операторов. В этой же ...
Добавлено: 22 октября 2017 г.
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2018 Т. 25 № 5 С. 506-524
О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. — 2018. — Т. 25, № 5. — С. 506–524. Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых ...
Добавлено: 26 октября 2018 г.
Гнатенко А. Р., Захаров В. А., Automatic Control and Computer Sciences, Allerton Press Inc., United States 2019 Vol. 53 No. 7 P. 663-675
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a nite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. A behaviour of such a reactive system displays itself in the correspondence between ows of control signals ...
Добавлено: 17 октября 2019 г.
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2020 Т. 27 № 4 С. 428-441
К последовательным реагирующим системам относятся программы и устройства, которые работают с двумя потоками данных и осуществляют преобразование входных потоков данных в выходные потоки. К числу таких систем обработки информации относятся контроллеры, драйверы устройств, компьютерные интерпретаторы. Результатом работы таких вычислительных систем являются бесконечные последовательности пар событий типа запрос-отклик, и поэтому в качестве математических моделей для них ...
Добавлено: 31 января 2021 г.
Захаров В. А., Temerbekova G., Системная информатика 2016 No. 7 P. 33-44
Добавлено: 13 октября 2016 г.
Каменских А. А., Логико-философские штудии 2018 Т. 16 № 1-2 С. 19-20
В работе представлен к обсуждению пример неожиданного сходства решений серии ключевых проблем темпоральной логики, который обнаруживается в ряде фрагментов текстов поздних неоплатоников и в одной из работ Л.П. Карсавина (1882-1952). Речь идёт о сходстве темпоральных схем, посредством которых Ямвлих, Прокл и Дамаский конструируют своего рода «средний термин» между вечностью и физическим временем — ноэтическое время (χρόνος ...
Добавлено: 13 октября 2018 г.
Захаров В. А., Темербекова Г. Г., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 232-234.
Потоковые алгоритмы возникают при решении многих прикладных задач. В статье предложена модель потоковых программ- автоматов-преобразователей над полугруппами- и для нее была исследована проблема эквивалентности. В настоящей работе описан метод оптимизации потоковых программ. Этот метод является обобщением ранее известного подхода, предложенного в статье для минимизации автоматов-преобразователей. Решение задачи минимизации потоковых программ над группами представлено в статье ...
Добавлено: 13 октября 2016 г.
Захаров В. А., Темербекова Г. Г., Моделирование и анализ информационных систем 2016 Т. 23 № 6 С. 741-753
Автоматы-преобразователи над полугруппами можно использовать в качестве модели последовательных реагирующих программ, работающих в постоянном взаимодействии со своим окружением. Получив очередную порцию данных, реагирующая программа выполняет некоторую последовательность действий и предъявляет результат. Такие программы возникают при проектировании компьютерных драйверов, алгоритмов, работающих в оперативном режиме, сетевых коммутаторов. Во многих случаях проблема верификации программ такого рода может быть ...
Добавлено: 13 октября 2016 г.
Каменских А. А., В кн. : Логика и онтология в византийской догматической полемике. Очерки: Коллективная монография. Т. 19.: СПб. : Центр содействия образованию, 2020. С. 255-275.
В главе коллективной монографии проводится сопоставление темпоральных логик позднего неоплатонизма и раннехристианской традиции; обсуждаются проблемы генезиса представления о времени как о структуре, образованной рядом моментов-кайрос, каждый из которых может оказаться точкой разрыва временного ряда. ...
Добавлено: 5 декабря 2019 г.
Хайтович Д. Г., / Cornell University. Series arXiv "math". 2021. No. 2110.
Добавлено: 7 декабря 2021 г.
Попова Е. Л., , in : Двенадцатые Смирновские чтения: материалы Международной научной конференции, Москва, 24–26 июня 2021 г. : М. : Русское общество истории и философии науки, 2021. P. 134-137.
Данная статья посвящена формализации широкого спектра сценариев изменения знаний с течением времени. Мы исследуем комбинации временных и эпистемических модальностей, отражающих различные свойства рассуждений рациональных агентов. Для этой цели вводим модель 𝐸𝐸𝑀 – эволюционную эпистемическую модель. ...
Добавлено: 28 июня 2021 г.
Захаров В. А., Джусупекова З., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 190-192.
Автоматы-преобразователи в качестве модели последовательных реагирующих программы используются в системном программировании, в компьютерной лингвистике, в криптографии, при проектировании микроэлектронных схем и др. Преобразователь принимает на входе последовательность сигналов и выполняет некоторую последовательность действий, преобразуя тем самым конечные слова входного алфавита в полугрупповое выражение, значения которых и являются результатами вычислений.
Мы рассматриваем автоматы-преобразователи над произвольной полугруппой $S$, ...
Добавлено: 13 октября 2016 г.
Авдошин С. М., Набебин А. А., М. : ДМК Пресс, 2018
Книга содержит основные сведения из формально-логических систем. Это функции алгебры логики (булевы функции), теорема Поста о функциональной полноте, k-значные логики, производные булевых функций, аксиоматические исчисления высказываний, предикатов, секвенций, резолюций и язык программирования Пролог. Рассматриваются монадическая логика, конечные автоматы и представимые ими языки, темпоральная логика, аксиоматический язык программирования OBJ3. В основу книги положен многолетний опыт преподавания ...
Добавлено: 2 декабря 2017 г.