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

Аннотация:

Рассмотрена проблема визуального представления темпоральных и вероятностных элементов в инструментах формального моделирования игровых механик. На основе анализа существующих систем визуального моделирования – Machinations, сетей Петри, диаграмм состояний UML и UPPAAL – выявлены их ключевые ограничения при описании сложных игровых сценариев. Предложен подход к визуализации темпоральных операторов и вероятностных конструкций в инструменте Tula, разработанном авторами. Описан набор визуальных примитивов, обеспечивающих двунаправленное соответствие между визуальным представлением и формальной спецификацией на языке геймплея. Приведены примеры визуального моделирования типовых игровых сценариев с элементами временных задержек, условных вероятностей и многопользовательских взаимодействий. Показана возможность автоматической трансформации визуальных моделей в формальные спецификации, пригодные для верификации средствами PRISM и UPPAAL. Проведён сравнительный анализ выразительных возможностей Tula и систем-предшественников, показавший, что Tula является единственной из рассмотренных систем, одновременно обеспечивающей формальную верифицируемую семантику, встроенную поддержку темпоральных операторов (X, G, F, U) и произвольных вероятностных распределений, а также визуальную нотацию, организованную вокруг ресурсных потоков и игровых событий. Предложенный в Tula принцип двухуровневой спецификации с двунаправленной трансформацией замыкает цикл «дизайн → формализация → верификация → корректировка», снижая порог входа в формальные методы для практиков без потери верификационной полноты. Это позволяет рассматривать Tula как промежуточный слой между итеративным геймдизайном и промышленными верификаторами.

Аннотация: Рассмотрена распределенная сеть, топология которой описана неориентированным графом. Сеть может сама изменять свою топологию, используя специальные «команды», подаваемые ее узлами. В работе предложена предельно локальная атомарная трансформация acb изменения конца c ребра ac, «движущегося» вдоль ребра cb от вершины c к вершине b. В результате этой операции ребро ac удаляется, а ребро ab добавляется. Такая трансформация выполняется по «команде» от общей вершины c двух смежных ребер ac и cb. Показано, что из любого дерева можно получить любое другое дерево с тем же множеством вершин, использовав только атомарные трансформации. Если степени вершин дерева ограничены числом d (d3), то трансформация не нарушает этого ограничения. В качестве примера цели такой трансформации рассмотрены задачи максимизации и минимизации индекса Винера дерева с ограниченной степенью вершин без изменения множества его вершин. Индекс Винера – это сумма попарных расстояний между вершинами графа. Максимальный индекс Винера имеет линейное дерево (дерево с двумя листовыми вершинами). Для корневого дерева с минимальным индексом Винера определены его вид и способ вычисления числа вершин в ветвях соседей корня. Предложены два распределенных алгоритма: трансформации дерева в линейное дерево и трансформации линейного дерева в дерево с минимальным индексом Винера. Доказано, что оба алгоритма имеют сложность не выше 2n–2, где n – число вершин дерева. Также рассмотрена трансформация произвольных неориентированных графов, в которых могут быть циклы, кратные ребра и петли, без ограничения на степени вершин. Показано, что любой связный граф с n вершинами может быть преобразован в любой другой связный граф с k вершинами и тем же числом ребер за время не более 2(n+k)–2.

Аннотация:

Рассмотрена задача пополнения таксономий – иерархических структур для организации понятий. Предложена архитектура на основе подхода ReAct (Reasoning + Acting), позволяющая пополнять таксономию в режиме zero-shot без дообучения больших языковых моделей. Система реализована в двух сценариях: автономная навигация от корневых узлов и верификация гипотез, сгенерированных другими моделями. Эксперименты на материале диахронического датасета RuWordNet показали, что прямое исследование таксономии от корня сталкивается с ограничениями, связанными со сложностью графа (MAP@3 = 24.6%). В то же время использование системы в качестве верификатора позволило улучшить качество предсказаний базовых моделей: прирост MAP@3 составил 9.5 п.п. для FastText и 1.1 п.п. для TaxoYandexGPT-5-Lite. Ключевыми преимуществами подхода являются универсальность, отсутствие необходимости дообучения и интерпретируемость за счет явных цепочек рассуждений.