Данная статья посвящена проблеме верификации параллельных программ, которые могут содержать особые виды ошибок, связанных с синхронизацией параллельно исполняемых потоков и доступом к общей памяти. К таким ошибкам относятся тупики и гонки данных. Существует разделение методов верификации параллельных программ на статические и динамические. Последние требуют запуска кода и позволяют проверить на гонки лишь текущую реализацию программы, что при наличии большого числа ветвлений может привести к пропуску гонок. Среди статических методов наибольшее применение нашли аналитические методы (например, на основе дедуктивного анализа) и методы проверки моделей. Однако они сложны в реализации, а последние по-прежнему требуют от программиста значительного объёма ручной работы для построения модели. В этой связи необходимо использование моделей, которые могут быть построены автоматически. Ранее авторами была разработана модель на основе расширения сетей Петри, позволяющая автоматическое построение на основе последовательного кода и преобразование её в параллельный код. Автоматическое построение модели параллельной программы вводит новые, ранее не использовавшиеся требования, связанные со взаимодействием параллельных потоков. Таким образом, в данной статье рассматриваются особенности моделирования с использованием расширенных сетей Петри с семантическими связями основных примитивов синхронизации, реализуемых в большинстве языков и технологий параллельного программирования для систем с общей памятью. В дальнейшем на основе этих моделей будет проводится поиск гонок данных и тупиков для параллельных программ.
В статье рассматриваются неориентированные кратные графы произвольной натуральной кратности k > 1. Кратный граф содержит ребра трех типов: обычные, кратные и мультиребра. Ребра последних двух типов представляют собой объединение k связанных ребер, которые соединяют 2 или вершину соответственно. Связанные ребра могут использоваться только согласованно. Делимые графы представляют собой специальный класс кратных графов. Их основная особенность состоит в возможности разделить граф на k частей, которые будут согласованы на связанных ребрах и не будут иметь общих ребер. Каждая часть является обычным графом. Кратное дерево представляет собой кратный граф без кратных циклов. Количество ребер может быть разным для кратных деревьев с одинаковым количеством вершин. Также можно рассмотреть остовные деревья в кратном графе. Остовное дерево является полным, если кратный путь, соединяющий любые две выбранные вершины, существует в дереве тогда и только тогда, когда такой путь существует в исходном графе. Задача о минимальном полном остовном дереве в кратном графе NP-трудна даже в случае делимого графа. В данной статье мы получим точный алгоритм для задачи о минимальном полном остовном дереве в делимом кратном графе. Также мы определим подкласс делимых графов, для которых алгоритм будет выполняться за полиномиальное время.
Рассматривается NP-трудная задача динамического распределения виртуальных машин по серверам с группами размещения. Для каждой виртуальной машины известны такие параметры, как необходимое количество ресурсов и временные метки создания и удаления. Каждый сервер представляет собой композицию NUMA-узлов и размещается в некоторой стойке. Рассматриваются большие виртуальные машины, размещаемые на два узла одного сервера, и маленькие, что накладывает дополнительные условия для их размещения. Группы размещения представляют собой объединения подмножеств виртуальных машин с условиями конфликта между подмножествами. Задача состоит в том, чтобы упаковать все виртуальные машины с использованием минимального количества стоек серверов в течение рассматриваемого временного горизонта. Для решения данной задачи предлагается эвристика, основанная на методе генерации столбцов. Анализируется набор статических задач в различные моменты времени, необходимых для формирования общего набора шаблонов, используемых при построении верхних оценок. Результаты вычислительных экспериментов на реальных открытых примерах указывают на незначительные расхождения между нижними и верхними границами.
В данной статье изучается существование максимального и минимального элементов множества непрерывно дифференцируемых выпуклых продолжений на произвольной булевой функции и мощность множества непрерывно дифференцируемых выпуклых продолжений на булевой функции. В результате исследования установлено, что мощность множества непрерывно дифференцируемых выпуклых продолжений на произвольной булевой функции равна континууму. Аргументировано, что для любой булевой функции среди её непрерывно дифференцируемых выпуклых продолжений на нет минимального элемента. Доказано, что для любой булевой функции множество её непрерывно дифференцируемых выпуклых продолжений на имеет максимальный элемент лишь тогда, когда количество существенных переменных данной булевой функции меньше 2.
В условиях стремительного роста числа научных публикаций актуальной задачей становится разработка эффективных инструментов для их систематизации и поиска. Одним из таких инструментов является универсальная десятичная классификация (УДК), которая позволяет структурировать статьи по тематическим областям. Однако ручное присвоение кодов УДК зачастую оказывается неточным или недостаточно детализированным, что снижает эффективность использования этого подхода. В данной статье предлагается подход к автоматическому присвоению кодов УДК научным статьям с использованием моделей на основе архитектуры BERT. Для обучения и оценки модели был использован набор данных, содержащий более 19 тысяч статей по математике и смежным наукам. Мы разработали две специализированные метрики качества, учитывающие иерархическую природу УДК: иерархическую классификационную точность и иерархическую рекомендательную точность. Кроме того, мы предложили несколько стратегий преобразования иерархических меток в плоские. В ходе экспериментов нам удалось достичь значения иерархической рекомендательной точности 0,8220. Дополнительно проведено слепое тестирование с участием экспертов, которое выявило, что часть расхождений между эталонными и сгенерированными метками обусловлена некорректным выбором кода УДК авторами статей. Предложенный подход демонстрирует высокий потенциал для автоматической классификации научных статей и может быть адаптирован для других иерархических систем классификации.
Авторы предлагают методику извлечения предметно-ориентированных сущностей (ПОС) из русскоязычных текстов студенческих отчетных документов с использованием предварительно обученных языковых моделей на основе трансформеров. Извлечение ПОС из студенческих работ представляет собой актуальную задачу, так как полученные данные могут использоваться для различных целей — начиная от формирования проектных групп и заканчивая персонализацией учебных маршрутов, а также автоматизация процесса обработки документов снижает затраты труда на ручную обработку. В качестве материала для дообучения исследуемых моделей использовались размеченные экспертами отчетные документы студентов, обучающихся по направлениям информационных технологий и поступивших в период с 2019 по 2022 год, по проектным, практическим дисциплинам и выпускным квалификационным работам. Задача извлечения ПОС рассматривается как две задачи: идентификация именованных сущностей и генерация размеченного текста. Сравнительный анализ проводился между моделями, основанными исключительно на энкодерах (ruBERT, ruRoBERTa), предназначенными для извлечения именованных сущностей, и моделями, использующими как энкодеры, так и декодеры (ruT5, mBART), а также моделями, базирующимися только на декодерах (ruGPT, T-lite), применяемыми для генерации текста. Для оценки эффективности сравниваемых моделей использовалась F-мера, а также проведен анализ типичных ошибок. Наиболее высокие показатели по F-мере на тестовом наборе данных продемонстрировала модель mBART (93.55%). Эта же модель показала наименьший уровень ошибок при идентификации ПОС во время генерации текста и разметки. Модели для извлечения именованных сущностей проявляют меньшую склонность к ошибкам, однако имеют тенденцию к фрагментарному выделению ПОС. Полученные результаты свидетельствуют о применимости рассматриваемых моделей для решения поставленных задач с учетом специфики предъявляемых требований.
Авторы предлагают методику извлечения предметно-ориентированных сущностей (ПОС) из русскоязычных текстов студенческих отчетных документов с использованием предварительно обученных языковых моделей на основе трансформеров. Извлечение ПОС из студенческих работ представляет собой актуальную задачу, так как полученные данные могут использоваться для различных целей — начиная от формирования проектных групп и заканчивая персонализацией учебных маршрутов, а также автоматизация процесса обработки документов снижает затраты труда на ручную обработку. В качестве материала для дообучения исследуемых моделей использовались размеченные экспертами отчетные документы студентов, обучающихся по направлениям информационных технологий и поступивших в период с 2019 по 2022 год, по проектным, практическим дисциплинам и выпускным квалификационным работам. Задача извлечения ПОС рассматривается как две задачи: идентификация именованных сущностей и генерация размеченного текста. Сравнительный анализ проводился между моделями, основанными исключительно на энкодерах (ruBERT, ruRoBERTa), предназначенными для извлечения именованных сущностей, и моделями, использующими как энкодеры, так и декодеры (ruT5, mBART), а также моделями, базирующимися только на декодерах (ruGPT, T-lite), применяемыми для генерации текста. Для оценки эффективности сравниваемых моделей использовалась F-мера, а также проведен анализ типичных ошибок. Наиболее высокие показатели по F-мере на тестовом наборе данных продемонстрировала модель mBART (93.55%). Эта же модель показала наименьший уровень ошибок при идентификации ПОС во время генерации текста и разметки. Модели для извлечения именованных сущностей проявляют меньшую склонность к ошибкам, однако имеют тенденцию к фрагментарному выделению ПОС. Полученные результаты свидетельствуют о применимости рассматриваемых моделей для решения поставленных задач с учетом специфики предъявляемых требований.
Разработка систем автоматического оценивания является актуальной задачей, призванной упростить рутинный труд учителя и ускорить обратную связь для учащегося. Обзор посвящён исследованиям в области автоматической оценки ответов учащихся на основе эталонного ответа учителя. Авторы работы проанализировали модели текстов, применяемые для задач автоматической оценки коротких ответов (ASAG) и автоматизированной оценки эссе (AES). Также принималось во внимание несколько подходов для задачи определения близости текстов, так как она является аналогичной задачей, и методы её решения могут быть полезны и для анализа ответов студентов. Модели текста можно разделить на несколько больших категорий. Первая — это лингвистические модели, основанные на разнообразных стилометрических характеристиках, как простых вроде мешка слов и n-грамм, так и сложных вроде синтаксических и семантических. Ко второй категории авторы отнесли нейросетевые модели, основанные на разнообразных эмбеддингах. В ней выделяются большие языковые модели как универсальные, популярные и качественные методы моделирования. Третья категория включает в себя комбинированные модели, которые объединяют в себе как лингвистические характеристики, так и нейросетевые эмбеддинги. Сравнение современных исследований по моделям, методам и метрикам качества показало, что тренды в предметной области совпадают с трендами в компьютерной лингвистике в целом. Большое количество авторов выбирают для решения своих задач большие языковые модели, но и стандартные характеристики остаются востребованными. Универсальный подход выделить нельзя, каждая подзадача требует отдельного выбора метода и настройки его параметров. Комбинированные и ансамблевые подходы позволяют достичь более высокого качества, чем остальные методы. В подавляющем большинстве работ исследуются тексты на английском языке. Однако успешные результаты для национальных языков также встречаются. Можно сделать вывод, что разработка и адаптация методов оценки ответов студентов на национальных языках является актуальной и перспективной задачей.
Подмножество образует -доминирующее множество графа G, если для любой вершины найдется вершина такая, что длина кратчайшей цепи, соединяющей эти вершины; — число вершин в минимальном -доминирующем множестве; при; для числа, вычисление является NP-полной задачей. В работе рассматривается класс деревьев диаметра, степени внутренних вершин которых равны. Приводятся конструктивные описания деревьев. Разработаны процедуры вычисления значений в диапазоне. Установлены асимптотические оценки для и их доли от общего числа вершин деревьев при. Приводятся вычислительные примеры.
В статье рассматривается индекс Винера для слабо связных ориентированных графов. Для таких графов из-за слабой связности не всегда определено расстояние между вершинами и, что требует уточнения чтобы индекс Винера имел содержательный смысл. Достаточно хорошо изучен случай, когда полагают что при отсутствии пути между вершинами. Мы рассматриваем уточнение, когда равно количеству вершин в графе при отсутствии пути между вершинами и. В статье представлены графы на вершинах, где индекс Винера с таким уточнением достигает минимального и максимального значения. Мы также представляем результаты экспериментов, которые показывают как изменяется индекс Винера (с учетом обоих способов уточнения расстояния) при добавлении дуг в слабо связный ориентированный граф как фиксированной, так и случайной структуры.
Рассматривается задача об устойчивости состояния равновесия в лазерной системе с быстро осциллирующими коэффициентами. Построена усредненная по быстрым осцилляциям система с распределенным запаздыванием. Выделены критические случаи в задаче об устойчивости состояния равновесия. Показано, что пороговое значение коэффициента обратной связи, при котором состояние равновесия становится неустойчивым, увеличивается вследствие быстрых осцилляций по сравнению с соответствующим значением при отсутствии модуляции. В критических случаях построены нормальные формы — уравнения для медленной амплитуды периодических решений. Выявлены условия существования, устойчивости и неустойчивости циклов.
Эта статья посвящена использованию метода верификации моделей для точного теста планируемости систем реального времени, выполняющихся на мультипроцессорных платформах. Чтобы использовать этот метод, мы формально описываем системы реального времени с абстрактным планировщиком, используя модели Крипке. Эта формализация содержит термины, достаточные для специализации абстрактного планировщика. Мы иллюстрируем наш подход, явно определяя планировщики, которые учитывают вытеснение/невытеснение задач и глобальный фиксированный приоритет или приоритет ближайшего дедлайна в различных сочетаниях. Свойство безопасности (планируемости) систем реального времени сформулировано с помощью линейной темпоральной логики LTL. Формализация систем реального времени как моделей Крипке и задание свойства безопасности (планируемости) как формулы LTL позволяет свести точный тест планируемости таких систем к задаче верификации моделей. Мы апробируем этот подход к точному тесту планируемости, реализуя на Promela — входном языке инструмента верификации моделей SPIN — нашу формализацию систем реального времени с невытесняющим планировщиком с глобальным фиксированным приоритетом (NP-GFP), вытесняющим планировщиком с глобальным фиксированным приоритетом (P-GFP), невытесняющим планировщиком с приоритетом ближайшего дедлайна (NP-EDF) и вытесняющим планировщиком с приоритетом ближайшего дедлайна (P-EDF). Мы проводим эксперименты в SPIN для доказательства/опровержения свойства безопасности (планируемости), чтобы оценить эффективность нашего подхода. Мы предлагаем эвристическую оценку планируемости системы реального времени на основе доказуемости небезопасности и недоказуемости безопасности системы реального времени при выполнении на мультипроцессорных платформах с числом процессоров, отличающимся на единицу.