• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Найдено 38 публикаций
Сортировка:
по названию
по году
Статья
Гнатенко А. Р., Захаров В. А. Моделирование и анализ информационных систем. 2020. Т. 27. № 4. С. 428-441.

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

Добавлено: 31 января 2021
Статья
Захаров В. А., Жайлауова Ш. Р. Моделирование и анализ информационных систем. 2017. Т. 24. № 4. С. 415-433.

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

Добавлено: 12 октября 2017
Статья
Захаров В. А., Темербекова Г. Г. Моделирование и анализ информационных систем. 2016. Т. 23. № 6. С. 741-753.

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

Добавлено: 13 октября 2016
Статья
Захаров В. А., Чемерицкий Е. В. Моделирование и анализ информационных систем. 2014. Т. 21. № 6. С. 57-69.
Разработка алгоритмов реконфигурирования сетей является важным направлением развития программного обеспечения для телекоммуникационных сетей нового поколения --- программно конфигурируемых сетей. Частный случай проблемы реконфигурирования сетей --- это задача плавного восстановления заданной сетевой конфигурации, после того как некоторые правила коммутации пакетов были удалены из таблиц коммутаторов (например, по истечении срока их активности). В данной статье проведено исследование этой задачи в рамках формальной модели программно конфигурируемых сетей, предложены корректные и безопасные алгоритмы восстановления сетевых конфигураций, и показано, что в общем случае задачу плавного восстановления конфигураций нельзя решить без обращения к правилам коммутации с приоритетами.
Добавлено: 30 сентября 2015
Статья
Челноков Г. Р. Моделирование и анализ информационных систем. 2007. Т. 14. № 4. С. 53-56.
Добавлено: 9 марта 2018
Статья
Глызин Д. С., Кубышкин Е. П., Морякова А. Р. Моделирование и анализ информационных систем. 2015. Т. 22. № 1. С. 74-84.

В работе изучается расположение нулей двух характеристических квазиполиномов, возникающих при изучении дифференциальных уравнений с запаздывающим аргументом: первый — при изучении математической модели генератора электромагнитных колебаний с запаздывающей обратной связью, второй — при изучении системы уравнений Ланга–Кобаяши, которая является известной математической моделью квантового генератора. Для квазиполиномов построена картина D-разбиений в пространстве параметров, выявлены возможные критические случаи. Рассмотрен случай большого запаздывания, который важен для приложений. В этом случае для нулей квазиполиномов получены аналитические зависимости от величины, обратной запаздыванию, и построены равномерные асимптотические формулы.

Добавлено: 19 ноября 2020
Статья
Легалов А. И., Васильев В. С. Моделирование и анализ информационных систем. 2018. Т. 25. № 4. С. 347-357.

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

Добавлено: 31 октября 2020
Статья
Башкин В. А., Ломазова И. А. Моделирование и анализ информационных систем. 2013. Т. 20. № 4. С. 23-40.

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

Добавлено: 14 ноября 2013
Статья
Челноков Г. Р. Моделирование и анализ информационных систем. 2007. Т. 14. № 2. С. 12-16.

В работе рассматриваются последовательности $W$ периода $u$ над алфавитом из $l$ букв. Требуется однозначно определить последовательность $W$ указывая слова, не являющихся ее подсловами. %Пусть $u$ --- наименьший период этой последовательности, $n$ --- его длина; $T_n$ --- %минимальное число запретов, задающих эту последовательность, $m_n=\max_{u}T_n$, %$r_n=\min_{u}T_n$. Для $n \in \NN$ обозначим за $U_n$ множество слов $u$ длины $n$, не являющихся степенями (т.е. не представимых в виде $u=v^k$ $k>1$). %очевидно, что эти и только эти слова являются периодами %последовательностей, наименьший период которых есть $n$. Пусть $T(u^{\infty})$ минимальное число запретов, задающих последовательность $u^{\infty}$.  Обозначим $$m_n=\max_{u \in U_n} T(u^{\infty}),\quad r_n=\min_{u \in U_n} T(u^{\infty})$$.

Доказаны следующие теоремы: \begin{theorem} $m_n\leq n(l-1)$. \end{theorem} Отметим, что оценка точна при бесконечно многих $n$, и реализуется, например, для периода содержащего все слова некоторой фиксированой длины $t$ (т.е. $n=l^t$). \begin{theorem} $r_n \ge \log_2 n + 1$ %$\exists c \in \Re$, $c>0$ такое, что $r_n\geq c*\ln (n)$. \end{theorem} \begin{theorem} Существует возрастающая последовательность $n_i$, такая, что $$r_{n_i}\leq \log_{\phi} n_i,\quad \text {где}\quad\phi = \frac{1+\sqrt5}{2}.$$ %$\exists c_1 \in \Re$ и возрастающая последовательность $n_i$ такая, %что $r_n\leq c_1*\ln (n_i)$. \end{theorem}

Добавлено: 9 марта 2018
Статья
Тихомиров А. С., Заводчиков М. А. Моделирование и анализ информационных систем. 2014. Т. 21. № 2. С. 90-96.

В статье доказывается приводимость пространства $M_{\mathbb{P}^3}^{\rm ref}$ модулей стабильных рефлексивных пучков ранга 2 с классами Черна $c_1=-1,\ c_2=4,\ c_3=2$ на $\mathbb{P}^3$. Это первый пример приводимого пространства в серии пространств модулей стабильных рефлексивных пучков ранга 2 с классами Черна $c_1=-1,\ c_2=4,\ c_3=2m,\ m=1,2,3,4,5,6,8$. Найдены две неприводимые компоненты этого пространства, имеющие ожидаемую размерность 27, и дается их геометрическое описание посредством конструкции Серра.

Добавлено: 20 октября 2014
Статья
Каленкова А. А., Колесников Д. А. Моделирование и анализ информационных систем. 2018. Т. 25. № 6. С. 711-725.

Поиск редакционного расстояния между графовыми моделями (определение схожести графовых моделей) является важной задачей в различных областях компьютерных наук, таких как анализ изображений, машинное обучение, химическая информатика. В последнее время, в связи с развитием методов извлечения и анализа процессов, появилась необходимость в адаптации существующих методов сравнения графовых моделей для анализа моделей процессов (аннотированных графов), извлекаемых из логов событий информационных систем. Методы нахождения минимального редакционного расстояния между графами могут быть использованы для обнаружения шаблонов (подпроцессов), а также для сравнения извлекаемых моделей процессов. Как было показано экспериментально и теоретически обосновано, точные методы нахождения минимального редакционного расстояния между извлекаемыми моделями процессов (и графами в общем случае) имеют большую временную сложность и могут быть применены лишь к небольшим моделям процессов. В этой статье мы оцениваем точность и временные характеристики генетического алгоритма, применяемого для нахождения расстояний между моделями процессов, извлекаемых из логов событий. В частности мы находим расстояния между BPMN (Business Process Model and Notation) моделями, извлекаемыми из логов событий с помощью различных алгоритмов синтеза. В этой работе показано, что представленный генетический алгоритм позволяет в значительной степени уменьшить время вычислений, при этом показывая результаты, близкие к оптимальным (минимальным редакционным расстояниям).

Добавлено: 13 октября 2019
Статья
Коломейченко М. И., Золотых А. А., Поляков И. В. и др. Моделирование и анализ информационных систем. 2014. Т. 21. № 6. С. 155-168.
В данной работе представлено описание программного комплекса для хранения, анализа и визуализации графов социальных сетей. Проводится сравнительный анализ существующих программных продуктов для анализа и визуализации графов. Кроме того, представлена общая архитектура приложения, описаны принципы его построения и работы основных модулей. Отдельно приведено описание разработанного графового хранилища, ориентированного на хранение и обработку графов больших размеров. В качестве основной функциональности программного продукта представлены разработанный алгоритм выделения сообществ и реализованные алгоритмы авто- размещения графов. Преимущество разработанного программного продукта заключатся в высокой скорости работы с сетями больших размеров, достигающих нескольких миллионов вершин и связей. Кроме того, используемая архитектура хранилища графов является уникальной и не имеет аналогов на данный момент. Имеющиеся в ней подходы и алгоритмы оптимизированы для работы с большими графами и обладают высокой производительностью.
Добавлено: 12 января 2015
Статья
Мицюк А. А., Шугуров И. С. Моделирование и анализ информационных систем. 2014. Т. 21. № 4. С. 181-198.

Извлечение процессов (process mining) -- новая и активно развивающаяся область исследований, тесно связанная с управлением процессами, формальными моделями процессов и извлечением данных (data mining). Одна из основных задач извлечения процессов -- синтез (извлечение) модели процесса на основании анализа журнала событий. Разработан широкий спектр алгоритмов для извлечения, анализа и усовершенствования моделей процессов. Журналы событий реальных систем часто содержат шум различных видов.   В данной работе описываются основные причины возникновения шума в журналах событий и изучается влияние шума на эффективность применения основных алгоритмов извлечения процессов. Приводятся экспериментальные результаты применения основных алгоритмов извлечения моделей процессов к искусственным журналам событий с шумами различного типа. Для этого специальным образом сгенерированные журналы событий с шумом обрабатывались с использованием четырех основных методов извлечения процессов. Хотя современные алгоритмы могут справляться с некоторыми типами шума, в большинстве случаев их применение не приводит к получению удовлетворительного результата. Таким образом, существует необходимость в разработке более совершенных подходов для журналов событий с шумом.

Добавлено: 20 октября 2014
Статья
Твардовский А. С., Эль-Факи К., Громов М. Л. и др. Моделирование и анализ информационных систем. 2017. Т. 24. № 4. С. 496-507.

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

Добавлено: 11 августа 2018
Статья
Козачок М. А., Магазинов А. Н. Моделирование и анализ информационных систем. 2014. Т. 21. № 4. С. 47-53.

Совершенным призмоидом называется выпуклый многогранник P такой, что для каждой его гиперграни F существует опорная гиперплоскость α, параллельная F, такая что любая вершина многогранника P лежит либо в F, либо в α. Совершенные призмоиды связаны с гипотезой Калаи о том, что у любого выпуклого центрально-симметричного многогранника не менее 3^d граней, а ровно 3^d граней содержат только многогранники Ханнера. Любой многогранник Ханнера является совершенным призмоидом (обратное не верно). Многогранник, который является выпуклой оболочкой некоторого подмоножества вершин единичного куба, называется 0/1-многогранником. Мы докажем, что любой совершенный призмоид аффинно эквивалентен некоторому 0/1-многограннику той же размерности. (Это означает, что любой совершенный призмоид является решетчатым многогранником). Пусть в пространстве R^d задана решетка Λ и многогранник D, вписанный в шар B. Многогранник D называется решетчатым многогранником Делоне, если внутри шара нет точек решетки и D является выпуклой оболочкой множества Λ∩∂B, где ∂B — граница шара BB. Мы докажем, что любой совершенный призмоид аффинно эквивалентен некоторому решетчатому многограннику Делоне.

Добавлено: 4 октября 2018
Статья
Захаров В. А., Смелянский Р. Л., Чемерицкий Е. В. Моделирование и анализ информационных систем. 2013. Т. 20. № 6. С. 33-48.
Программно-коммутируемые сети (ПКС) --- это класс компьютерных телекоммуникационных сетей, появившийся несколько лет назад в стремлении упростить проектирование и повысить гибкость управления сетями за счет разделения потоков данных (пакетов) и потоков управления (сообщений и команд), циркулирующие в сетях. ПКС представляет собой распределенную систему, в которой один или несколько контроллеров управляют множеством сетевых коммутаторов, обеспечивающих продвижение пакетов по каналам сети. Функциональные возможности и порядок взаимодействия коммутаторов и контроллеров ПКС определяются протоколом OpenFlow. На основе аппарата булевых функций и дискретных преобразователей нами предложена формальная модель ПКС, введен прототип формального языка спецификаций, поставлены задачи верификации моделей ПКС и получены оценки их сложности. Для одной из задач верификации моделей ПКС описан метод ее решения, на основе которого разработано программно-инструментальное средство верификации ПКС.
Добавлено: 30 сентября 2015
Статья
Захаров В. А. Моделирование и анализ информационных систем. 2020. Т. 27. № 3. С. 260-303.

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

1. При помощи алгебраического метода построен новый алгоритм проверки эквивалентности детерминированных конечных автоматов, имеющий сложность по времени O(n log n).

2. Выделен новый класс префиксных конечных трансдьюсеров и показано, что проверка эквивалентности трансдьюсеров из этого класса может быть осуществлена новым методом за время, квадратичное (для префиксных трансдьюсеров реального времени) и кубическое (для префиксных трансдьюсеров с epsilon-переходами) относительно размеров анализируемых автоматов.

3. Показано, что проблема эквивалентности для детерминированных двухленточных конечных автоматов сводится к задаче проверки эквивалентности префиксных конечных трансдьюсеров и может быть решена за время, кубическое относительно их размеров.

4. Аналогичным образом установлена разрешимость проблемы эквивалентности для детерминированных конечных биавтоматов за время, кубическое относительно их размеров.

5. При помощи нового метода построен алгоритм проверки эквивалентности для простых грамматик, соответствующих детерминированным магазинным автоматам с одним состоянием.

Добавлено: 28 сентября 2020
1 2