![]() |
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ЦЭМИ РАН |
||
Цель исследования состоит в получении асимптотических оценок высокой степени точности для сложности управляющих систем, разработке методов и алгоритмов анализа управляющих систем, тестировании и оптимизации управляющих систем. Кроме того, целью проекта является исследование и решение серии задач, связанных с двумя проблемами теоретического программирования – проблемой верификации программ и проблемой оптимизации программ.
Discrete control systems are traditionallly studied in discrete mathematics and mathematical cybernetics. Either new trends (obtaining of high-precise asymptotical bounds) or classical branches (the development of methods and algorithms of analysis, testing, and optimization of some control system models like VLSI models) are very perspective. The theotetical results in this field are applicable to some practic problems like nano-level VLSI design, design of distributed informational systems. All these facts permit to conclude the usefullness of theoretical investigations and applications of obtained results in the fields of VLSI design in the frames of the suggested theme.
Планируется получить новые оценки различных сложностных функционалов (таких как схемная сложность, глубина, задержка, длина теста) булевых функций и систем булевых функций, а также разработать новые специальные математические методы для решения различных задач верификации и оптимизации программ и информационных систем.
Участники проекта имеют большой набор методов и результатов, связанных с разработкой методов синтеза и получением асимптотических оценок высокой и близкой к ней степени точности как для различных функций Шеннона, так и для некоторых специальных ФАЛ. Основным методом, с помощью которого планируется получать новые результаты, является метод асимптотических оценок высокой степени точности (АОВСТ) и его модификации. В недавних работах были получены следующие результаты. Поведение функции Шеннона на уровне АОВСТ установлено для сложности BDD, где «вес» «слившихся» вершин больше, чем «вес» остальных, и для сложности формул стандартного базиса с ограниченной глубиной альтернирования, соответственно. Поведение функции Шеннона для задержки СФЭ в некоторых содержательных моделях установлено на уровне АОВСТ и на уровне близких к ним оценок. В направлении, связанном с тестированием схем, участники проекта имеют опыт 1) в получении рекордных оценок функций Шеннона длины проверяющего теста при неисправностях элементов в схемах, 2) в получении оценок функций Шеннона длины теста при неисправностях на входах схем. В направлении, связанном с теоретическим программированием, участниками темы разработаны общие методы построения эффективных алгоритмов распознавания эквивалентности программ, теория аппроксимации отношения эквивалентности для моделей программ, методы верификации моделей распределённых программ и формул темпоральных логик, методы маскировки программ.
МГУ имени М.В.Ломоносова | Координатор |
госбюджет, раздел 0110 (для тем по госзаданию) |
# | Сроки | Название |
1 | 1 января 2019 г.-31 декабря 2019 г. | Математические модели дискретных управляющих систем и их приложения |
Результаты этапа: Установлено асимптотическое поведение функции Шеннона для сложности скалярных рекурсивных схем из функциональных элементов (СФЭ) над произвольным конечным полным базисом, имеющих ограниченную глубину рекурсии. Разработан метод синтеза СФЭ в некоторых базисах, позволяющий получить как для «типичной», так и для «самой сложной» ФАЛ асимптотически оптимальные - на уровне асимптотических оценок высокой степени точности (АОВСТ) - по сложности схемы, имеющие высокую степень защищенности от раскрытия функциональности. Получены более точные по сравнению с известными ранее нижние оценки сложности реализации стандартной мультиплексорной ФАЛ порядка n. Установлено, что функция Шеннона длины единичного проверяющего теста относительно вставки элемента «стрелка Пирса» в СФЭ над базисом Жегалкина не превосходит 2. Получена экспоненциальная нижняя оценка функции Шеннона длины полного диагностического теста относительно замещений элементов на конъюнкторы и дизъюнкторы в СФЭ. Рассмотрен подкласс монадических стандартных схем программ, в котором используются только одноместные функциональные и предикатные символы, и для данного класса предложен экспоненциальный по сложности (относительно размеров проверяемых программ) переборный алгоритм проверки комбинированной эквивалентности схем программ. Предложен подход к решению задачи проверки совместного останова программ без процедур, позволяющий с учетом известных результатов обосновать разрешимость и полиномиальную разрешимость проблемы эквивалентности программ с процедурами для многих перегородчатых моделей с полугрупповыми законами тождества операций преобразования данных и построить соответствующие решающие и полиномиальные решающие алгоритмы. | ||
2 | 1 января 2020 г.-31 декабря 2020 г. | Математические модели дискретных управляющих систем и их приложения |
Результаты этапа: Для ФАЛ от не более чем пяти переменных были построены ориентированные контактные схемы, оптимизированные по динамической активности. Разработаны методы синтеза СФЭ в некоторых новых базисах, позволяющие получить как для «типичной», так и для «самой сложной» ФАЛ асимптотически оптимальные по сложности схемы, имеющие линейную динамическую активность. Описана структура и установлено точное значение глубины минимальных по сложности СФЭ, реализующих ступенчатые ФАЛ. Исследована возможность оптимизации СФЭ, реализующих ступенчатые ФАЛ, как по сложности, так и по глубине. Доказано, что для любого натурального $n$ любую булеву функцию $f$, зависящую от $n$ переменных, можно реализовать неизбыточной схемой из функциональных элементов в базисе $\{ xy, x\vee y, \bar x\}$, допускающей в случае неисправностей вида «закорачивание входа элемента на его выход с инвертированием» единичный проверяющий тест длины 2. Доказано, что в модели последовательных императивных программ с процедурами отношение обобщенной логико-термальной эквивалентности аппроксимирует отношение функциональной эквивалентности. Предложено понятие бисимуляционной эквивалентности моделей систем реального времени, являющейся достаточным условием неотличимости моделей формулами логики ветвящегося реального времени. | ||
3 | 1 января 2021 г.-31 декабря 2021 г. | Математические модели дискретных управляющих систем и их приложения |
Результаты этапа: Предложена и рассмотрена достаточно общая модель для вычисляющих булевы функции двоичных программ над произвольными конечными базисами из вычислительных и переадресующихся команд, а также команд вызова подпрограмм. При этом допускается рекурсивный вызов подпрограмм, глубина которого ограничена заданным числом. Разработаны методы синтеза, с помощью которых уставлено асимптотическое поведение функции Шеннона для сложности реализации булевых функций от заданного числа переменных в рамках этой модели. Разработаны алгоритмы поиска оптимальных по статической и динамической активности схем из функциональных элементов (СФЭ) в произвольном конечном полном базисе, реализующих функции алгебры логики(ФАЛ) от малого числа переменных. В основе разработанных алгоритмов лежит подход, основанный на сведении задачи поиска схемы к задаче выполнимости булевых формул. Был создан прототип программной реализации данных подходов на основе системы поиска оптимальных по сложности схем. Предложенные ранее участниками проекта методы синтеза для «типичных» ФАЛ асимптотически оптимальных по сложности СФЭ в стандартном базисе, которые при этом имеют линейную относительно числа переменных реализуемых функций динамическую активность, обобщены на случай базисов более общего вида. Разработаны методы синтеза, с помощью которых получены новые более точные оценки функции Шеннона для глубины усилительных схем из функциональных элементов в некоторых базисах с емкостными параметрами выходов элементов. Установлены новые более точные и близкие к асимптотическим оценкам высокой степени точности (АОВСТ) оценки сложности реализации стандартных мультиплексорных функций в классе контактных схем с более слабыми, по сравнению с известными ранее, ограничениями на их структуру. В рамках модели клеточных схем получены близкие к АОВСТ оценки для сложности мультиплексорной функции, а также установлена асимптотика сложности некоторых связанных с ней операторов в данной модели. Установлены новые оценки функции Шеннона длины единичного проверяющего теста относительно замен элементов на инвенторы в СФЭ, функции Шеннона длины единичного диагностического теста относительно вставок элементов СФЭ, функций Шеннона длины k-диагностического теста относительно инверсных неисправностей элементов СФЭ. Для расширенной модели стандартных схем программ с операторами вызова процедур разработан алгоритм проверки логико-термальной эквивалентности полиномиальной по времени сложности, доказаны завершаемость и корректность предложенного разрешающего алгоритма. Предложен алгоритм проверки эквивалентности пропозициональных операторных программ на левосократимых уравновешенных полугрупповых шкалах, более эффективный по сравнению с имеющимися. Уточнено для соответствия практическим нуждам предложенное ранее понятие бисимуляционной эквивалентности моделей систем реального времени с часами. | ||
4 | 1 января 2022 г.-31 декабря 2022 г. | Математические модели дискретных управляющих систем и их приложения |
Результаты этапа: Предложенные ранее исполнителями темы методы синтеза для «типичных» функций алгебры логики (ФАЛ) асимптотически оптимальных по сложности схем из функциональных элементов (СФЭ) в стандартном базисе, которые при этом имеют линейную относительно числа переменных реализуемых функций динамическую активность, распространены на более «широкий» по сравнению с известными ранее класс базисов. Получена нижняя оценка статической активности схем из функциональных элементов в достаточно широком классе базисов на основе положительной чувствительности функций алгебры логики, реализуемыми данными схемами. Для динамической активности схем построен контрпример, который показывает, что аналогичную оценку доказать невозможно. Для целочисленных умножителей размера $3\times 4$ и $3\times 5$ улучшены значения сложности схем единичной глубины в базисе из адаптивных логических элементов архитектуры Stratix10. Разработан метод синтеза, с помощью которого получены асимптотические оценки высокой степени точности функции Шеннона для сложности схем из функциональных элементов над произвольным конечным базисом, имеющих глубину ветвления 1. Установлена асимптотика функции Шеннона для сложности программ общего вида, вычисляющих булевы функции, в том случае, когда удельный вес переадресующих команд не меньше удельного веса вычислительных команд. Получены асимптотически точные оценки сложности реализации универсальной системы функций в классе клеточных схем из функциональных и коммутационных элементов, а также сложности реализации системы из нескольких мультиплексорных функций с общим набором информационных переменных в одном достаточно широком классе контактных схем. Установлено точное значение глубины мультиплексорной функции с числом адресных переменных от 11 до 19 в стандартном базисе Получены новые оценки функций Шеннона длин тестов относительно зеркальных неисправностей на входах схем, локальных константных неисправностей на входах схем, а также относительно отождествлений входов элементов в схемах из функциональных элементов над некоторыми базисами. Предложено решение проблемы эквивалентности линейных унарных рекурсивных программ в одном классе полугрупповых семантик, более эффективное в смысле порядка сложности решающих алгоритмов по сравнению с имеющимися. Исследованы способы представления выражений логики Брусенцова, предложено представление, эффективное для случая выражений с многократно повторяющимися подвыражениями. | ||
5 | 1 января 2023 г.-31 декабря 2023 г. | Математические модели дискретных управляющих систем и их приложения |
Результаты этапа: Получена логарифмическая по числу переменных нижняя оценка динамической активности для любой функции, существенно зависящей от всех своих переменных в произвольном базисе. Построена схема, реализующая мультиплексорную функцию, асимптотически оптимальная по сложности и порядку роста динамической активности в стандартном базисе. Начато исследование поведения функции Шеннона для площади клеточных схем ограниченной высоты с кратными входами, расположенными на её горизонтальных сторонах, в некоторых случаях получены первые асимптотические точные оценки этой функции. Получены асимптотические оценки высокой степени точности (АОВСТ) для сложности реализации мультиплексорной функции в классе клеточных схем из функциональных и коммутационных элементов. Установлено точное значение глубины данной функции с числом адресных переменных 10 в стандартном базисе. Получены АОВСТ для площади мультиплексора и для системы всех симметрических ФАЛ в стандартном базисе. Доработаны методы поиска оптимальных и близких к ним инверсных графов в некоторых базисах, встречающихся в приложениях. Уточнены базы данных конъюнктивно-инверсных и мажоритарно инверсных графов, реализующие функции от не более, чем пяти переменных. Получены новые оценки функций Шеннона длин тестов относительно зеркальных неисправностей на входах схем. Установлено, что универсальный полином для класса линейных функций существует тогда и только тогда, когда для каждого простого числа в разложении модуля существует универсальная функция соответствующего числа переменных. Предложено решение проблемы эквивалентности линейных унарных рекурсивных программ для ряда полугрупповых семантик, основанных на уравновешенных полугруппах, порождённых операторами программ. |
Для прикрепления результата сначала выберете тип результата (статьи, книги, ...). После чего введите несколько символов в поле поиска прикрепляемого результата, затем выберете один из предложенных и нажмите кнопку "Добавить".
№ | Имя | Описание | Имя файла | Размер | Добавлен |
---|