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

Последовательные реагирующие системы включают в себя устройства и программы, вычисления которых состоят в непрерывном взаимодействии с внешней средой, от которой они получают потоки входных сигналов (данных, команд) и в ответ на них формируют потоки выходных сигналов. К системам такого вида относятся контроллеры, сетевые коммутаторы, интерпретаторы программ, системные драйверы. Поведение некоторых реагирующих систем определяется не только последовательностью значений входных сигналов, но также временем их поступления на вход системы и задержками вычисления выходных сигналов. Эти особенности вычисления реагирующих систем хорошо учитываются вычислительными моделями реального времени, к числу которых относятся, в частности, конечные автоматы-преобразователи реального времени (Timed Finite State Machines, TFSMs). Однако в большинстве работ, посвященных изучению этой модели вычислений, используется упрощенная семантика TFSMs: элементы выходного потока, независимо от сопутствующих пометок времени, располагаются в том же порядке, в котором следуют соответствующие им элементы входного потока. Такое упрощение семантики делает модель менее адекватной для многих приложений, но зато облегчает решение задач анализа и преобразования таких автоматов. В данной статье мы изучаем модель TFSM с более реалистичной семантикой. Переход к новой модели TFSM требует и новых подходов к решению задачи верификации автоматов в этой модели. Для этой цели мы предлагаем альтернативное определение вычислений TFSM с использованием размеченных систем переходов и показываем, что два определения семантики для рассматриваемого класса автоматов реального времени хорошо взаимосвязаны друг с другом. Использование семантики TFSM, основанной на размеченных системах переходов, открывает возможность применения ранее известных методов верификации систем вычислений реального времени для анализа поведения последовательных реагирующих систем.

Мы исследуем формальную верификацию управляющего программного обеспечения критических систем, т. е. проверку соответствия функционирования проектируемой системы предъявленным требованиям. Важнейший класс управляющего программного обеспечения составляют программы для программируемых логических контроллеров (ПЛК). Особенностью программ ПЛК является цикл управления: 1) считываются входы, 2) изменяются состояния ПЛК и 3) записываются выходы. Поэтому для формальной верификации программ ПЛК нужна возможность описывать учитывающие эту специфику системы переходов, а также определять свойства систем, моделирующих программы ПЛК, как относительно переходов внутри цикла, так и относительно более крупных переходов в соответствии с семантикой цикла управления. Мы предлагаем формальную модель программы ПЛК как систему переходов гиперпроцессов и темпоральную логику cycle-LTL для формализации свойств ПЛК. Особенностью логики cycle-LTL является возможность рассматривать свойства систем управления двояким образом: воздействие окружения на систему управления и воздействие системы управления на окружение. Мы определяем модификации стандартных темпоральных операторов логики LTL для каждого из этих случаев, а также для свойств внутри цикла управления. Рассмотрены примеры требований, определенных в нашей логике. Описана трансляция формул cycle-LTL в формулы LTL и показана её корректность. Доказана возможность сведения задачи верификации методом проверки моделей для требований, определенных в логике cycle-LTL, к задаче верификации требований, определенных в стандартной логике LTL.

К последовательным реагирующим системам относятся программы и устройства, которые работают с двумя потоками данных и осуществляют преобразование входных потоков данных в выходные потоки. К числу таких систем обработки информации относятся контроллеры, драйверы устройств, компьютерные интерпретаторы. Результатом работы таких вычислительных систем являются бесконечные последовательности пар событий типа запрос-отклик, и поэтому в качестве математических моделей для них наиболее часто используются конечные автоматы-преобразователи. Поведение автоматов-преобразователей представлено бинарными отношениями на бесконечных последовательностях, и традиционные прикладные темпоральные логики (HML, LTL, CTL, mu-исчисление) плохо подходят для этой цели, поскольку для интерпретации их формул используются omega-языки, а не бинарные отношения на omega-словах. Чтобы предоставить темпоральным логикам возможность определять свойства преобразований, которые характеризуют поведение реагирующих систем, мы ввели новые расширения этих логик, имеющие две отличительные особенности: 1) темпоральные операторы в расширениях этих логик параметризованы, и в качестве параметров используются языки в входном алфавите автоматов-преобразователей; 2) в качестве базовых предикатов используются языки в выходном алфавите автоматов-преобразователей. Ранее нами были исследованы выразительные возможности новых расширений Reg-LTL и Reg-CTL известных темпоральных логик линейного и ветвящегося времени LTL и CTL, в которых для параметризации темпоральных операторов и задания базовых предикатов разрешалось использовать только регулярные языки. Мы обнаружили, что такая параметризация увеличивает выразительные возможности темпоральной логики, но сохраняет разрешимость задачи проверки выполнимости формул на конечных моделях. Для указанных выше логик нами были разработаны алгоритмы верификации конечных автоматов-преобразователей. На следующем этапе изучения новых расширений темпоральной логики, предназначенных для спецификации и верификации последовательных реагирующих систем, мы обратились к задаче верификации этих систем с использованием темпоральной логики Reg-CTL*, которая является расширением обобщенной логики деревьев вычислений CTL*. В этой статье описан алгоритм проверки выполнимости формул Reg-CTL* на моделях конечных автоматов-преобразователей и показано, что эта задача принадлежит классу сложности ExpSpace.

Мультиагентный алгоритм — это распределённый алгоритм, основанный на знаниях, который решает некоторую проблему посредством совместной работы агентов. BDI-агент — это агент, обладающий убеждениями (Belief), желаниями (Desire) и намерениями (Intention). С точки зрения такого агента, мультиагентный алгоритм — это алгоритм, основанный на его знаниях и убеждениях, с помощью которого достигается выполнение его желаний посредством последовательного осуществления намерений. Мы считаем также, что агенты реактивны, проактивны и рациональны. В этой статье мы предлагаем и изучаем два мультиагентных алгоритма, которые основаны на знаниях. В частности, мы предлагаем мультиагентный алгоритм для следующей задачи аренды ресурсов. Система состоит из агентов, которые прибывают один за другим в произвольном порядке в ресурсный центр, чтобы арендовать один из предоставляемыхресурсов. Предоставляемые ресурсы пассивны, они образуют облако. Если за ресурс нет конкуренции, то он предоставляется по запросу, и возвращается в облако после использования. Агенты также образуют облако, но когда арендуют нужный ресурс, то сразу же покидают ресурсный центр. Задача состоит в разработке мультиагентного алгоритма, основанного на знаниях, обладающего следующим свойством корректности: каждый прибывающий в ресурсный центр агент рано или поздно арендует какой-либо из запрашиваемых ресурсов без конкуренции за этот ресурс в данный момент.

Степень применения методов формальной верификации в индустриальных проектах всегда была ограничена. Распространение систем распределенного реестра (СРР), известных также как блокчейн, быстро меняет ситуацию. Поскольку основной областью применения СРР является автоматизация финансовых транзакций, свойства предсказуемости и надежности являются критическими при реализации таких систем. Реальное поведение СРР определяется выбранным протоколом консенсуса, свойства которого нуждаются в строгой спецификации и формальной верификации. Формальная спецификация и верификация протокола консенсуса необходима, но недостаточна. Необходимо удостовериться, что программная реализация узлов СРР соответствует данному протоколу. Верифицированная программная реализация протокола должна запускаться на достаточно надежной операционной системе. Так называемые “умные контракт”, которые являются важной частью прикладных реализаций конкретных бизнес-процессов на основе СРР, также должны быть верифицируемы.В данной работе мы описываем реализующийся в настоящее время индустриальный проект, результатом которого станет СРР, верифицированная по меньшей мере на четырех описанных выше технологических уровнях. Мы также описываем наш опыт формальной спецификации и верификации протокола HotStuff - отказоустойчивого протокола для гарантированного достижения консенсуса в присутствии византийских процессов и лидера.

В настоящей работе рассматривается архитектура системы распределенного реестра (СРР) InnoChain. Основной целью этой архитектуры является реализуемость 5-ти уровней формальной верификации программного обеспечения (ПО) системы InnoChain, включая операционное окружение. Методы формальной верификации являются основными методами обеспечения качества ПО с критическими требованиями по надежности, но до сих пор онине находилиширокого применения в СРР. Архитектура InnoChain включает (1) предметно-ориентированный язык смарт-контрактов с формальной семантикой, встроенный в функциональный язык CakeML (диалект языка ML), что позволяет осуществлять формальную верификацию свойств корректности смарт-контрактов в системах логики высших порядков (например, HOL4); (2) верифицированную трансляцию смарт-контрактов в машинный код с использованием компилятора CakeML вместо использования виртуальных машин для исполнения смарт-контрактов; (3) реализацию функционала узла СРР также на CakeML с формальной верификацией свойств корректности и с верифицированной трансляцией исходного кода узла в машинный код; (4) формальную верификацию протокола консенсуса СРР (HotStuff BFT); (5) использование формально-верифицированного микроядра seL4 в качестве операционного окружения СРР вместо операционных систем общего назначения. Предлагаемая архитектура открывает возможности для использования СРР InnoChain в критических по надежности приложениях, в частности, в системе управления заправкой воздушных судов ПАО Аэрофлот.

Известно, что настройка параметров может существенно улучшить время работы эволюционных алгоритмов.
Ярким примером этого является генетический алгоритм (1 + (λ,λ)), где адаптация размера популяции в процессе работы помогает достичь линейного времени работы на задаче OneMax. Однако если свойства решаемой задачи вступают в конфликт с принципами работы используемого метода настройки параметров, производительность эволюционного алгоритма может существенно ухудшаться. Так, например, происходит при использовании правила «одной пятой» в упомянутом алгоритме при решении задач со слабой корреляцией между приспособленностью и расстоянием до оптимума.
В данной работе предлагается модификация правила «одной пятой», существенно снижающая отрицательные эффекты от его использования при их наличии. Показывается, что данная модификация также достигает линейного времени работы на задаче OneMax, при этом ее использование приводит к улучшению производительности на линейных псевдобулевых функциях со случайными весами, а также на некотором классе задач MAX-3SAT.

Автор сожалеет, что в исходном списке ссылки [3] и [4] находятся в неправильных местах и их следует переставить.
Кроме того, [3] содержит ошибку в названии статьи. Исправленный список цитируемых источников приведен ниже. Автор приносит извинения за причиненные неудобства.
References
[1] A. I. Mal'tsev, “Constructive algebras I”, Russian Mathematical Surveys, vol. 16, no. 3, pp. 77-129, 1961.
[2] A.I. Mal'tsev, Algoritmy i rekursivnye funktsii. Moscow: Nauka, 1965, In Russian.
[3] R. M. Robinson, “Primitive recursive functions”, Bulletin of the American Mathematical Society, vol. 53, no. 10, pp. 925-942, 1947.
[4] J. Robinson, “General recursive functions”, Proceedings of the American Mathematical Society, vol. 1, no. 6, pp. 703-718, 1950.
[5] V.A. Sokolov, “Ob odnom klasse tozhdestv v algebre Robinsona”, in 14-ya Vsesoyuznaya algebraicheskaya konferentsiya: tezisy dokladov, In Russian, vol. 2, Novosibirsk, 1977, pp. 123-124.
[6] P. M. Cohn, Universal Algebra. New York, Evanston, and London: Harper & Row, 1965.
[7] A. Robinson, “Equational logic for partial functions under Kleene equality: a complete and an incomplete set of rules”, The Journal of Symbolic Logic, vol. 54, no. 2, pp. 354-362, 1989.