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

Рассматривается краевая задача для логистического уравнения с запаздыванием и диффузией, моделирующая динамику плотности популяции в одномерном ареале. На левой границе задано нулевое условие Неймана, а на правой поток пропорционален отклонению плотности от равновесного значения, взятому с запаздыванием $\delta$, что отвечает задержке миграционного отклика на границе. Изучается влияние запаздывания $\delta$ на локальную устойчивость положения равновесия и характер потери устойчивости. Проведён линейный анализ, границы области устойчивости в плоскости параметров $\gamma$ и $r$ найдены методом продолжения по параметру. Установлено, что при $\gamma > 0$ потеря устойчивости возможна двумя способами: дивергентно, через нулевой корень характеристического уравнения, и колебательно, через пару чисто мнимых корней, а при $\gamma \leqslant 0$ — только колебательно. Показано, что граница дивергентной потери устойчивости не зависит от $\delta$. Выявлен эффект существенного расширения области устойчивости при значениях $\delta$, близких к 0.5. При подходящем выборе параметров равновесие сохраняет устойчивость при значениях $r$, существенно превосходящих порог $\pi/2$ случая $\gamma=0$. Вместе с тем это расширение ограничено. При $d=1$ область устойчивости остаётся ограниченной по $r$, а её точная верхняя грань $r_*\approx7.6714$ достигается в предельной точке $(\delta_*,\gamma_*)\approx(0.4792, 2.6314)$, в которой характеристическое уравнение имеет одновременно три пары чисто мнимых корней. Существование и единственность предельной точки установлены численно с гарантированной точностью средствами интервальной арифметики. Тем самым умеренная задержка в миграционном отклике способна компенсировать дестабилизирующее влияние быстрого размножения, но лишь до определённого предела. Результаты подтверждены численным моделированием с использованием метода линий и явной схемы Рунге-Кутты 6-го порядка.

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

В статье рассматривается задача восстановления аналитического вида систем обыкновенных дифференциальных уравнений по наблюдаемым временным рядам нелинейных динамических систем. Актуальность задачи обусловлена необходимостью получения интерпретируемых математических моделей в естественных науках, когда фундаментальные законы эволюции неизвестны или известны лишь частично. Предложен метод T‑SINDy, сочетающий метод временных задержек, тензорные представления и разреженную регрессию. В отличие от классического подхода SINDy, где число параметров растёт экспоненциально с увеличением числа функций-кандидатов, предлагаемое тензорное отображение позволяет параметризовать все возможные нелинейные взаимодействия через полилинейное отображение. Для снижения вычислительной сложности применяется каноническое разложение, которое сокращает число параметров до линейной зависимости от числа модальностей и ранга. Разреженность модели достигается двухэтапной процедурой: сначала пороговым обнулением элементов фактор-матриц с последующей донастройкой ненулевых коэффициентов, затем дополнительным отсечением малых значений в развёрнутом тензоре параметров. Это обеспечивает отбор значимых слагаемых и устойчивость к шуму. Вычислительные эксперименты проведены на системе Лоренца (наблюдаются две переменные из трёх) и на нормальной форме бифуркации Хопфа (наблюдается одна переменная) при уровнях шума от 0 до 10%. Для каждой системы варьировались максимальная задержка и начальный момент обучающей выборки. Показано, что T‑SINDy обеспечивает точность прогноза, сопоставимую с классическим методом SINDy, при меньшем времени обучения. Восстановленные уравнения сохраняют интерпретируемость, явно выражая динамику через исходные переменные, что выгодно отличает предложенный подход от нейросетевых методов, дающих неинтерпретируемые скрытые представления. Предложенный подход представляет собой эффективную и интерпретируемую альтернативу для идентификации динамических систем по неполным зашумленным данным.

В настоящей работе рассматривается технология синтеза программ по моделям. На языке темпоральной логики задаются требуемые свойства программы, согласно которым разрабатывается модель поведения. Проверка соответствия модели заданным свойствам осуществляется методом проверки модели (model checking). Синтезированная по формально верифицированной модели программа наследует все её темпоральные свойства. Модель поведения программы может оказаться несогласованной с проверяемыми свойствами, если их формализация выполнена с учетом ошибочных предположений относительно модели. Внесение изменений в модель для согласования осложняет процедуру синтеза, так как адаптированная под свойства модель описывает поведение, которое отличается от поведения программы. Для решения данной проблемы в настоящей работе предлагается применять шаблон проектирования «Декоратор». Ориентированная на синтез модель является декорированным объектом. Адаптированная под свойства модель является объектом-декоратором, который содержит в себе декорированный объект и «на лету» модифицирует его поведение с учетом особенностей проверяемых свойств. Декорирование позволяет без вмешательства в исходную модель адаптировать её к проверяемым свойствам — для изменения поведения под заданный набор свойств требуется разработать только объект-декоратор, декорированный объект остается без изменений и используется для синтеза программы. Результаты работы продемонстрированы на примере разработки и верификации протокола безопасной сделки. Для задания свойств протокола используется логика деревьев вычислений CTL. Модель протокола представляет собой конечный автомат. Реализованная в виде декоратора адаптированная под CTL-свойства модель воспроизводит промежуточные состояния, отсутствующие в конечном автомате. Декоратор и декорированный объект оформляются в виде модулей инструмента проверки модели nuXmv. Верифицированная спецификация протокола переводится в Java-класс, который используется как доверенный модуль при построении веб-сервиса безопасной сделки на основе эскроу-счёта.

Объектно-ориентированный process mining сформировался как эффективная парадигма анализа событийных данных, включающих несколько взаимодействующих бизнес-объектов. Существующие методы обнаружения моделей часто опираются на объектно-ориентированные сети Петри с фиксированными кратностями дуг, что ограничивает их способность представлять параметрические закономерности потребления и производства ресурсов, а также отражать количественные зависимости между взаимодействующими типами объектов. В данной работе предлагается метод обнаружения объектно-ориентированных сетей Петри с параметрическими дугами. Предлагаемый подход строит модели по объектно-ориентированным журналам событий, одновременно выявляя поведенческие закономерности с переменными весами дуг. Сначала обнаруживается управляющее поведение для отдельных типов объектов, после чего полученные модели объединяются в единую объектно-ориентированную структуру. Затем анализируется количество объектов, участвующих в событиях одного и того же вида деятельности, с целью выявления повторяющихся количественных зависимостей между типами объектов. Эти зависимости представляются константами или линейными выражениями и назначаются в качестве весов дуг результирующей модели. В работе формализуется используемая модель, представляется алгоритм обнаружения и доказывается, что при выполнении сформулированных предположений относительно моделей, обнаруженных для отдельных типов объектов, результирующая сеть способна идеально воспроизводить наблюдаемые многообъектные трассы. Кроме того, применимость подхода оценивается на репрезентативных реальных и синтетических объектно-ориентированных журналах событий. Результаты показывают, что предложенный метод позволяет заменить неопределённые переменные кратности явными параметрическими зависимостями, сохраняя при этом наблюдаемое поведение, представленное обнаруженной моделью. Получаемые объектно-ориентированные сети Петри обеспечивают более компактное и выразительное представление объектно-ориентированных процессов и делают явными количественные закономерности синхронизации между взаимодействующими типами объектов.

Рассматривается задача автоматической тематической классификации текстов на татарском языке — низкоресурсном языке с развитой агглютинативной морфологией. В условиях активного развития больших языковых моделей (LLM) одной из центральных задач становится создание открытых корпусов, токенизаторов и размеченных датасетов, без которых невозможны ни дообучение современных архитектур, ни объективное сравнение их эффективности. Работа направлена на создание открытой ресурсной базы для обработки татарского языка и её экспериментальную валидацию в задаче тематической классификации. В работе представлены и апробированы специально подготовленные ресурсы: корпус TatCorp 222M (222 млн токенов), токенизаторы TatarTokenizers, модели векторных представлений Tatar2Vec (FastText, Word2Vec, CBOW) и размеченный датасет из 13 160 текстов десяти тематических категорий. Модели эмбеддингов обучены на корпусе TatCorp 222M и отобраны из 57 конфигураций с использованием предложенной композитной метрики. Выполнено систематическое сравнение пяти методов векторизации, включая предобученные эмбеддинги Tatar2Vec, TF-IDF и Bag of Words, в сочетании с семью алгоритмами классификации — от линейных моделей и ансамблей до многослойного перцептрона. Дополнительно исследовано влияние субсловной токенизации BPE на качество тематической классификации. Наивысший показатель макро"=$F_1$"=меры (0.7789) получен для комбинации предобученных эмбеддингов Word2Vec (без субсловной токенизации) и многослойного перцептрона (MLP); практически сопоставимый результат (0.7760) и максимальный ROC AUC (0.9683) достигнуты при использовании Bag of Words и XGBoost. Установлено, что применение субсловной токенизации BPE в задаче тематической категоризации текстов на агглютинативном языке не повышает, а систематически снижает качество классификации (снижение макро"=$F_1$"=меры составляет до 0.0234). Созданные открытые ресурсы и воспроизводимые бенчмарки могут служить основой для дальнейших исследований, включая оценку эффективности трансформерных моделей для татарского и других низкоресурсных тюркских языков.