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

В настоящее время повсеместными стали методы программно-целевого управления развитием различных социально-экономических систем сложной структуры, например, таких как территории сельскохозяйственного назначения. Поэтому актуальными задачами являются верификация уже созданных программ развития и разработка «правильных» программ развития таких систем, по аналогии с верификацией и разработкой правильных компьютерных программ – развитыми дисциплинами в теоретическом программировании. В данной работе для решения задачи верификации программ развития сельскохозяйственных территорий сначала строится структурная схема программы, по которой создается аксиоматическая теория, использующая аппарат алгоритмических логик Хоара. Основной проблемой при построении аксиоматической теории является разработка аксиом теории, отражающих предусловия и эффекты выполнения содержательных действий, указанных в тексте программы развития. Верификация программы развития соответствует проверке доказуемости некоторой тройки Хоара, соответствующей начальным и целевым условиям программы. Для задачи разработки правильных программ развития описывается механизм построения модели предметной области с использованием языков описания моделей семейства PDDL. Описание конкретной модели имеет чисто декларативный характер и представляет собой набор описаний предикатов и действий выбранной предметной области. Показывается, как на описанной модели с помощью интеллектуальных планировщиков, включая темпоральные планировщики типа OPTIC, автоматически строить решения целевых задач программ развития. На основе экспертных знаний и отраслевых стандартов построена модель сельскохозяйственной территории, краткое описание которой приводится в работе. Проведенные эксперименты показали эффективность предлагаемого подхода к разработке правильных программ развития.

При дедуктивной верификации программ, написанных на императивных языках программирования, особую сложность вызывает порождение и доказательство условий корректности, соответствующих циклам, поскольку каждый из них должен быть снабжён инвариантом, построение которого часто является нетривиальной задачей. Методы синтеза инвариантов циклов, как правило, носят эвристический характер, что затрудняет их применение. Альтернативой является символический метод элиминации инвариантов циклов, предложенный В.А. Непомнящим в 2005 году. Его идея состоит в представлении тела цикла в виде специальной операции замены при выполнении определённых ограничений. Такая операция в символической форме выражает действие цикла, что позволяет ввести в аксиоматическую семантику правило вывода для циклов, не использующее инварианты. В данной работе представлено дальнейшее развитие этого метода. Он расширяет метод смешанной аксиоматической семантики, предложенный для верификации C-light программ. Данное расширение включает в себя метод верификации итераций над изменяемыми массивами с возможным выходом из тела цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов циклов. Данное правило было реализовано в генераторе условий корректности, являющемся частью системы автоматизированной верификации C-light программ. Для проведения автоматического доказательства в используемой системе ACL2 были разработаны и реализованы два алгоритма: первый порождает операцию замены на языке системы ACL2, а второй генерирует вспомогательные леммы, позволяющие системе ACL2 успешно доказать получаемые условия корректности в автоматическом режиме. Применение вышеуказанных методов и алгоритмов проиллюстрировано примером.

Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Мы полагаем, что для формального описания поведения реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционная темпоральная логика линейного времени LT L. В этой работе рассматривается новый язык формальных спецификаций LP-LT L, представляющий собой расширение темпоральной логики LT L, специально разработанное для описания свойств вычислений автоматов-преобразователей. Темпоральные операторы в формулах LP-LT L снабжены параметрами, в качестве которых используются множества слов (языки), описывающие потоки сигналов управления, поступающих на вход реагирующей системы. Базовые предикаты в формулах LP-LT L также определяются языками в алфавите элементарных действий; эти языки описывают ожидаемую реакцию системы в ответ на воздействия окружающей среды. В более ранних работах авторов этой статьи изучалась задача верификации конечных автоматов-преобразователей относительно спецификаций, представленных формулами логик LP-LT L и LP-CT L. Было показано, что для обеих логик эта задача алгоритмически разрешима. Цель данной работы — оценить выразительные возможности логики LP-LT L и сравнить ее с широко известными логиками, применяющимися в информатике для спецификации реагирующих систем. В логике LP-LT L были выделены два фрагмента LP-1-LT L и LP-n-LT L. Нам удалось установить, что язык спецификаций LP-1-LT L более выразителен, чем LT L, в то время как фрагмент LP-n-LT L обладает точно такими же выразительными возможностями, что и монадическая логика второго порядка S1S.

В работе изучается безопасность унарных операторов инфляционной неподвижной точки (IFP-операторов), то есть возможность их вычисления за конечное время. Такие операторы в точности соответствуют рекурсивным SQL-запросам, поэтому изучаемый вопрос имеет непосредственное отношение к базам данных. Исследуемая проблема возникает из-за того, что при одновременном применении в SQL запросе рекурсии и отношений универсума, например, сложения, может оказаться так, что процедура вычисления результата запроса зациклится. Более того, такая комбинация позволяет моделировать работу универсального вычислительного устройства, например, машины Тьюринга, поэтому вопрос о возможности вычисления SQL запроса за конечное время оказывается алгоритмически неразрешимым. В предыдущих работах были введены и изучены некоторые свойства универсумов, которые позволяют гарантировать возможность вычисления любых запросов за конечное время. Здесь мы изучаем вопрос о том, насколько существенна местность IFP-операторов в контексте их безопасности. Основным результатом настоящей работы является демонстрация того, что если ограничиться только унарными IFP-операторами, то не имеют места результаты, справедливые для IFP-операторов в общем случае без ограничения местности. Построен пример универсума, в котором все унарные IFP-операторы, не вложенные один в другой, безопасны. Вместе с тем в этом универсуме существуют небезопасные бинарные IFPоператоры, таким образом, при изменении местности безопасность может утрачиваться. Кроме того, существуют и небезопасные вложенные один в другой унарные операторы. Это контрастирует с общим случаем, в котором такое невозможно. Также существуют элементарно эквивалентные универсумы, в которых те же самые унарные IFP-операторы безопасными не являются. Такое поведение тоже отличается от поведения IFP-операторов произвольной местности.

Полипрограмма — это обобщение программы, допускающее множественность определений одной и той же функции. Подобные объекты возникают в различных системах преобразования программ, таких как система Бёрстолла–Дарлингтона и насыщение равенствами. В данной работе мы вводим понятие полипрограммы на нестрогом функциональном языке первого порядка. Мы определяем денотационную семантику полипрограмм и описываем некоторые преобразования полипрограмм в двух разных стилях: в стиле системы Бёрстолла–Дарлингтона и в стиле насыщения равенствами. Преобразования в стиле насыщения равенствами осуществляются над полипрограммами в расчленённой форме, в которой стирается грань между функциями и выражениями и между подстановкой и раскрытием вызова функции. Расчленённые полипрограммы хорошо подходят для реализации и проведения рассуждений, но трудны для человеческого восприятия. Мы также вводим понятие бисимуляции полипрограмм, на котором основано преобразование — слияние по бисимуляции, соответствующее доказательству эквивалентности функций по индукции или коиндукции. Бисимуляция полипрограмм — понятие, вдохновлённое понятием бисимуляции размеченных систем переходов, но несколько от него отличающееся, поскольку бисимуляция полипрограмм рассматривает каждое определение как самодостаточное, т.е. функция полипрограммы задаётся любым своим определением, в то время как в размеченной системе переходов поведение системы в состоянии определяется всей совокупностью переходов, которые можно осуществить из этого состояния. Мы предлагаем алгоритм перечисления бисимуляций некоторого определённого вида. Алгоритм состоит из двух фаз: перечисление пребисимуляций и преобразование их в бисимуляции. Такое разделение требуется из-за того, что бисимуляции полипрограмм учитывают возможность перестановки параметров функций. Мы доказываем корректность данного алгоритма, а также формулируем некоторую слабую форму его полноты. Статья публикуется в авторской редакции.

Трансформационный подход к верификации программ был очень популярной темой исследований в первые десятилетия теории программирования. Многие выдающиеся пионеры теории программирования внесли свой вклад в разработку данного направления исследований: Джон Маккарти, Амир Пнуели, Дональд Кнут ... Много интересных примеров трансформационного подхода было тщательно изучено, что привело к методам устранения рекурсии, известным как хвостовая рекурсия и как ко-рекурсия. В данной работе мы подробно исследуем (мы надеемся, новый) пример устранения рекурсии, основанный на трансформациях программы и анализе задачи, решаемой этой программой. Наш пример является частным случаем нисходящего динамического программирования, но не является ни примером хвостовой рекурсии, ни кo-рекурсии. Этот пример можно рассмотреть с разных точек зрения: как пример преобразования нисходящего динамического программирования к восходящему (с использованием только статической памяти фиксированного размера), или как доказательство функциональной эквивалентности между рекурсивной и итеративной программами (которое в дальнейшем может послужить примером для автоматического доказательства), или как захватывающую алгоритмическую головоломку либо задачу дизайна, анализа и верификации алгоритмов. Статья публикуется в авторской редакции.

Гиперграфическими автоматами называются автоматы, у которых множества состояний и выходных символов наделены структурами гиперграфов, сохраняющимися функциями переходов и выходными функциями. Универсальные притягивающие объекты в категории таких автоматов представляются автоматами Atm(H₁,H₂) с гиперграфом состояний H₁, гиперграфом выходных символов H₂ и полугруппой входных символов S = EndH₁ × Hom(H₁,H₂), которые называются универсальными гиперграфическими автоматами. Для такого автомата Atm(H₁,H₂) полугруппа входных символов S является производной алгеброй отображений, свойства которой взаимосвязаны со свойствами алгебраической структуры данного автомата. Это позволяет изучать универсальные гиперграфические автоматы с помощью исследования их полугрупп входных символов. В настоящей работе рассматривается проблема представления универсальных гиперграфических автоматов в их полугруппах входных сигналов: описывается представление универсального гиперграфического автомата в виде многосортной алгебраической системы, канонически построенной из автономных входных сигналов этого автомата. Эта конструкция является одним из инструментов доказательства относительно элементарной определимости рассматриваемых автоматов в классе полугрупп, которая позволяет проанализировать взаимосвязь элементарных свойств этих автоматов и их полугрупп входных сигналов. Основной результат работы дает решение этой задачи для универсальных гиперграфических автоматов над эффективными гиперграфами p-определимыми ребрами. Это достаточно широкий и весьма важный класс автоматов, так как он содержит, в частности, автоматы, у которых гиперграфы состояний и выходных символов являются плоскостями (например, проективными или аффинными) или разбиениями на классы нетривиальных эквивалентностей. Статья публикуется в авторской редакции.

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