Preview

Моделирование и анализ информационных систем

Расширенный поиск
Том 22, № 4 (2015)
Скачать выпуск PDF

Оригинальные статьи 

453-463 668
Аннотация

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

464-482 987
Аннотация

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

483-499 599
Аннотация

Пусть G – конечная неединичная группа с неприводимым комплексным характером χ степени d. Согласно соотношениям ортогональности для неприводимых характеров, сумма квадратов степеней этих характеров равна порядку группы G. Н. Снайдером доказано, что если |G| = d(d + e), то порядок группы G ограничен функцией e при e > 1. Я. Берковичем доказано, что в случае e = 1 группа G является группой Фробениуса с дополнением порядка d. В данной работе изучается конечная неединичная группа G, обладающая неприводимым комплексным характером Θ, для которого |G| ≤ 2Θ(1)2. Доказано, что в случае, когда Θ(1) – произведение двух различных простых чисел p и q, группа G является разрешимой группой с абелевой нормальной подгруппой K индекса pq. С помощью классификации простых конечных групп доказано, что простая неабелева группа, порядок которой делится на простое число p и не превышает 2p4, изоморфна одной из следующих групп: L2(q), L3(q), U3(q), Sz(8), A7, M11, J1.

500-506 585
Аннотация

В 1973 году Аленби и Грегорас доказали следующее утверждение. Пусть G – расщепляемое
расширение конечно порожденной группы A с помощью группы B. 1) Если в группах A и B все подгруппы (все циклические подгруппы) финитно отделимы, то и в группе G все подгруппы (все циклические подгруппы) финитно отделимы; 2) если в группе A все подгруппы финитно отделимы, а в группе B все конечно порожденные подгруппы финитно отделимы, то в группе G все конечно порожденные подгруппы финитно отделимы. Напомним, что группа G называется расщепляемым расширением группы A с помощью группы B, если группа A является нормальной подгруппой группы G, B – подгруппа группы G, G = AB и A ∩ B = 1. Напомним также, что подгруппа H группы G называется финитно отделимой, если для каждого элемента g группы G, не принадлежащего подгруппе H, существует гомоморфизм группы G на некоторую конечную группу, при котором образ элемента g не принадлежит образу подгруппы H. В данной работе получено обобщение теоремы Аленби и Грегораса за счет замены условия конечной порожденности группы A более общим: для любого натурального числа n число всех подгрупп группы A индекса n конечно. В действительности при этом условии удалось получить необходимое и достаточное условие финитной отделимости всех подгрупп (всех циклических подгрупп, всех конечно порожденных подгрупп) в группе G

507-520 641
Аннотация

Статья посвящена подходу к построению и верификации «дискретных» программ логических контроллеров (ПЛК) по LTL-спецификации. Этот подход обеспечивает возможность анализа корректности программ логических контроллеров с помощью метода проверки модели (Model Checking). В рамках подхода в качестве языка спецификации программного поведения используется язык темпоральной логики LTL. Анализ корректности LTL-спецификации относительно программных свойств производится автоматически с помощью программного средства символьной проверки модели Cadence SMV. В статье демонстрируется состоятельность подхода к построению и верификации ПЛК-программ по LTL-спецификации с точки зрения тьюринговой мощности. Доказывается, что в соответствии с этим подходом для произвольной счётчиковой машины Минского может быть построена LTL-спецификация, по которой осуществляется её программная реализация на любом из языков программирования ПЛК стандарта МЭК 61131-3. Поскольку счётчиковые машины Минского равномощны машинам Тьюринга, то и рассматриваемый подход к программированию ПЛК будет обладать тьюринговой мощностью. В доказательстве основное внимание уделяется заданию поведения счётчиковой машины в виде набора LTL-формул и сопоставлению этим формулам конструкций языков ST и SFC. SFC представляет интерес с точки зрения специфики графического языка, а язык ST рассматривается в качестве базового в том смысле, что реализация счётчиковой машины на языках IL, FBD/CFC и LD сводится к переписыванию на них конструкций ST-программы. Идея доказательства демонстрируется на примере трехсчетчиковой машины Минского, реализующей функцию возведения числа в квадрат.

521-532 655
Аннотация

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

533-545 645
Аннотация

В статье рассматривается задача о наибольшем кратном потоке в сети произвольной натуральной кратности k. Определяется три типа дуг в сети: обычная дуга, кратная дуга, мультидуга. Каждая кратная и мультидуга представляет собой объединение k связанных дуг, согласованных между собой. Задаются правила построения сети. Вводится понятие делимой сети и ряд связанных определений. Отмечается важная особенность делимых сетей – возможность разделить их на k частей, согласованных на связанных дугах кратных и мультидуг, таким образом, что каждая часть является обычной транспортной сетью. Основным результатом статьи является выделение следующих подклассов задачи о наибольшем кратном потоке в делимой сети.
1. Делимая сеть с ограничениями на мультидуги. Если в k−1 части делимой сети имеется только одна вершина, являющаяся концом мультидуги, то задача о наибольшем потоке полиномиально разрешима.
2. Делимая сеть со слабыми ограничениями на мультидуги. Если в s частях делимой сети (1 ≤ s < k − 1) имеется только одна вершина, являющаяся концом мультидуги, а в остальных частях таких вершин несколько, то размерность задачи о наибольшем кратном потоке может быть понижена до k − s.
3. Делимая сеть параллельной структуры. Пусть компонента делимой сети, состоящая из всех кратных дуг, может быть разделена на субкомпоненты, содержащие ровно по одной вершиненачалу мультидуги. Пусть при этом каждая пара субкомпонент пересекается только в источнике сети x0. Если k = 2, то задача о максимальном кратном потоке разрешима за полиномиальное время. Если k ≥ 3, то задача NP-полна. Для каждого из полиномиальных подклассов получены алгоритмы. Также сформулирован алгоритм понижения размерности задачи для делимой сети со слабыми ограничениями на мультидуги.

546-562 708
Аннотация

В данной статье рассмотрены принципы организации беспроводных mesh-сетей  программно-конфигурируемых сетей подвижных объектов. Основное внимание уделяется вопросам построения эффективных алгоритмов маршрутизации для подобных сетей. Математической моделью системы является стандартная транспортная сеть. В качестве ключевого параметра системы маршрутизации рассматривается коэффициент доступности узла  функция, зависящая от ряда основных и дополнительных параметров ((mesh-факторовв), характеризующих маршрут между двумя узлами сети. Каждой паре (дуга, узел) сопоставляется композитный параметр, характеризующий 裂доступностьь узла по маршруту, начинающемуся данной дугой. Лучшим ((кратчайшимм) маршрутом между двумя узлами считается маршрут с наибольшим коэффициентом доступности. Описаны правила построения и обновления таблиц маршрутизации узлами сети. Получая анонс от соседа, узел имеет сведения об энергетике соединения, надежности соединения, времени
получения анонса, отсутствии промежуточных узлов, а также располагаемой пропускной способности. На основании этой информации ко всем маршрутам, проходящим через данного соседа, может быть применена пенализация (наложение штрафа) или поощрение (увеличение коэффициента доступности). Указанная схема пенализации / поощрения складывается из отдельных аспектов:
1. Пенализация за актуальность информации.
2. Пенализация / вознаграждение за надежность узла.
3. Пенализация за энергетику соединения.
4. Пенализация за располагаемую пропускную способность.
На основе предложенных эвристических алгоритмов маршрутизации построен симулятор беспроводной mesh-сети подвижных объектов, описание и характеристики которого приведены в статье. Также рассмотрены особенности программной реализации симулятора.

563-577 739
Аннотация

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

578-589 792
Аннотация

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



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)