ИСТИНА

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

The theory of discrete control systems is an intensively developing field of discrete mathematics and mathematical cybernetics. Its growth is caused by appearance of new trends (for example, obtaining of high-precise asymptotical bounds) as well as by the progress in traditional branches (for example, the development of methods and algorithms of analysis, verification, testing, and optimization of some control system models like VLSI models and program models). From the other hand, the theotetical results in this field are applicable to some practic problems like nano-level VLSI design, design and verification of distributed informational systems, program optimization. All these facts permit to conclude the usefullness of theoretical investigations and applications of obtained results in the fields of VLSI design and system programming in the frames of the suggested theme.

1. Получение асимптотических оценок, имеющих, как правило, высокую степень точности, для сложности "типичных" или "самых сложных" функций в некоторых классах схем. На базе различных вариантов предложенного С. А. Ложкиным метода асимптотических оценок высокой степени точности (АОВСТ) будет продолжено создание оригинальных эффективных методов реализации "типичных" и самых "сложных" функций в ряде моделей дискретных управляющих систем, обладающих определенными специальными метрическими, структурными или функциональными свойствами. С помощью этих методов для сложности указанных функций в рассматриваемых классах схем будут получены асимптотические оценки, имеющие, как правило, высокую степень точности. Так, будет продолжено исследование на уровне АОВСТ сложности реализации указанных функций в некоторых классах схем проводящего и предикатного типов, классах формул и схем из функциональных элементов (СФЭ) с прямыми и итеративными переменными и др., а также исследование возможности их реализации схемами, оптимальными как по сложности, так и по задержке. 2. Разработка методов синтеза схем в некоторых моделях, связанных с логическим проектированием дискретных устройств преобразования информации и, в частности, СБИС. На основе метода АОВСТ и других методов будет продолжено исследование модели задержки СФЭ, в которой задержка переключения выхода элемента, вызванного переключением одного из входов, зависит от значений на других входах этого элемента. В рамках данной модели будет установлено асимптотическое поведение функции Шеннона для задержки СФЭ в различных базисах, а также получены близкие к АОВСТ оценки этой функции. Будет продолжена разработка методов синтеза схем, оптимальных по так называемой динамической активности, которая является моделью энергопотребления СБИС. Будут установлены новые, более точные, оценки функции Шеннона для динамической активности контактных схем и СФЭ в различных базисах, разработаны методы синтеза, позволяющие получать асимптотически оптимальные по сложности схемы, динамическая активность которых оптимальна по порядку. 3. Разработка методов "вложения" ("геометрической" реализации) схем в некоторые регулярные структуры, связанные, в частности, с топологическим синтезом СБИС. Будут развиты и исследованы модели "вложения" схем в плоские прямоугольные решетки – т. н. "клеточные" схемы, единичные кубы и другие структуры. При этом будут рассмотрены различные модификации клеточных схем, моделирующие те или иные особенности структуры СБИС наноуровня. Будут созданы новые эффективные методы построения оптимальных вложений указанного вида как для "типичных" или "самых сложных" функций, так и для функций, встречающихся в приложениях. 4. Исследование индивидуальной сложности и структуры оптимальных схем для ряда "специальных" функций. Будут развиты методы синтеза и исследована структура оптимальных схем для некоторых функций, связанных с выполнением арифметических и логических операций (симметрические функции, счетчики четности, дешифраторы, мультиплексоры и др.). При этом будет продолжено исследование глубины и сложности некоторых функций и, в частности, мультиплексора, на уровне АОВСТ. Будет изучено влияние ряда структурных ограничений, а также степени самокоррекции на сложность реализации некоторых специальных функций. 5. Построение и анализ тестов для различных задач контроля в некоторых классах схем. Д. С. Романовым был разработан метод детекторных функций для построения достаточно коротких проверяющих тестов относительно неисправностей на выходах функциональных элементов. С применением этого и некоторых других методов будут построены близкие к оптимальным тесты в ряде задач контроля для схем из функциональных элементов, контактных схем и некоторых их модификаций, а также при неисправностях различных типов на входах схем; будет установлено или уточнено поведение соответствующих функций Шеннона длины теста. 6. Разработка эффективных алгоритмов проверки эквивалентности и оптимизации моделей программ. В. А. Захаровым был ранее разработан новый подход к решению задач проверки эквивалентности программ – метод совместных вычислений программ. При помощи этого метода были получены полиномиальные по времени алгоритмы решения проблемы эквивалентности в некоторых классах последовательных операторных программ. Однако возможности этого подхода к решению задач проверки эквивалентности программ еще не исчерпаны. Планируется проведение исследований с целью расширения области применения метода совместных вычислений программ и распространения его на другие модели вычислений: схемы рекурсивных программ, моделирующие функциональные программы, и обобщенные конечные автоматы-преобразователи (трансдьюсеры), моделирующие потоковые алгоритмы, проводящие вычисления в оперативном режиме. Также планируется проведение исследования ряда задач анализа программ, тесно примыкающих к проблеме эквивалентности программ – задачи унификации программ, задачи специализации программ, задачи оптимизации (минимизации) обобщенных конечных автоматов. Для различных моделей программ предполагается разработка полиномиальных по времени алгоритмы решения перечисленных задач. 7. Исследование и разработка новых методов верификации моделей распределенных вычислений. При решении задач проверки правильности функционирования систем параллельных вычислений, к числу которых относятся многонитевые программы, сетевые протоколы, микроэлектронные схемы и др., широко используются различные модели распределенных систем взаимодействующих процессов. Обычно ,каждый последовательный процесс, входящий в состав распределенной программы, моделируется конечной системой размеченных переходов (конечным автоматам). Взаимодействие отдельных процессов проявляется в одновременном исполнении определенных действий (например, действий передачи и приема сообщений). Поведение распределенной программы в рамках указанной модели представляется в виде множества трасс, каждая из которых является последовательностью чередующихся действий, выполняемых отдельными процессами программы. Спецификация (свойства поведения) распределенной программы может быть представлена формулой темпоральной логики, регулярным выражением, автоматом Бюхи и т. п. Проблема верификации моделей распределенных систем состоит в проверке выполнимости заданной спецификации для всех возможных поведений заданной распределенной системы. Планируется создание новых моделей распределенных вычислений для телекоммуникационных систем нового поколения – программно-конфигурируемых сетей, – а также алгоритмов анализа поведения и верификации моделей этих сетей. Для этой цели будут интенсивно привлекаться конструкции и методы дискретной математики – булевы функции, двоичные решающие диаграммы и др. Также планируется разработка новых методов решения задачи верификации распределенных вычислительных систем реального времени. Для этой цели предполагается разработать адаптивные методы символьной верификации моделей распределенных программ, позволяющие обнаруживать особенности устройства проверяемых моделей распределенных вычислений (симметрию, подобие и др.). Разработанные в направлениях 1-5 методы синтеза и контроля схем будут адаптированы для решения некоторых конкретных задач, связанных с проектированием СБИС. Планируется исследовать применимость предложенных в направлениях 6-7 методов для верификации описаний СБИС.

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

Этап 2014 года. 1. Получено более компактное представление оператора итеративного замыкания, введенного в работе С.А. Ложкина для классификации полных базисов из элементов с прямыми и итеративными переменными. При этом в каждом из семейств указанной классификации, кроме двух, в которых функция Шеннона для любого базиса имеет «стандартный» порядок роста 2n/log n, приведены примеры базисов с порядком роста этой функции, равным 2n. Отдельно показано существование функций, которые могут быть самыми сложными по порядку роста в классе формул над одним базисом, но при небольших изменениях базиса, оставляющих его в том же семействе упомянутой классификации, сложность таких функций кардинально меняется. 2. Разработаны методы синтеза и получены более точные нижние оценки сложности схем из функциональных элементов (СФЭ), реализующих квазимультиплексорные функции алгебры логики (ФАЛ). 3. Разработаны методы синтеза асимптотически оптимальных по задержке СФЭ в одной модели, где положительная задержка на входе элемента произвольным образом зависит как от номера этого входа, так и от типа подключенного сверху элемента, и в другой модели, где к указанным параметрам задержки добавляется ее зависимость от наборов, поступающих на вход рассматриваемого элемента. В этих моделях установлена асимптотика функции Шеннона для задержки и задержки мультиплексорной ФАЛ. Получены асимптотические оценки высокой степени точности функции Шеннона для задержки и задержки мультиплексорной ФАЛ в широком классе базисов первого типа. 4. Проведена дальнейшая разработка методов синтеза и получение более точных новых нетривиальных верхних и нижних оценок динамической активности ФАЛ в некоторых моделях дискретных управляющих систем. 5. Установлено точное значение размерности единичного гиперкуба, допускающего вложение древовидной BDD определенного вида, реализующей мультиплексорную функцию. 6. Найдены нетривиальные оценки функции Шеннона длины проверяющего теста относительно монотонных симметрических слипаний и точное значение функции Шеннона длины диагностического теста относительно монотонных симметрических слипаний входов схем. 7. Улучшена до асимптотики оценка функции Шеннона длины проверяющего теста относительно локальных k-кратных линейных слипаний входов схем. 8. Доказано, что длина минимального проверяющего теста для почти всех булевых функций относительно вытесняющих неисправностей входов схем равна n+1. 9. Предложен новый базис из функциональных элементов, в котором за константное число наборов можно обнаружить двукратную инверсную неисправность на выходах элементов (при введении константного числа дополнительных выходов). 10. Построен полиномиальный по времени алгоритм проверки эквивалентности программ с операторами, подчиняющимися законам коммутативности и подавления. 11. Доказана разрешимость задачи проверки подобия программ относительно отношения логико-термальной эквивалентности, получена оценка сложности указанной задачи. Этап 2015 года. 1. Получена асимптотика функции Шеннона для сложности булевых формул в классе полных базисов из элементов с прямыми и итеративными входами, итеративное замыкание которых содержит класс монотонных функций. В таких базисах порядок роста этой функции является «стандартным» для булевых формул, однако константа в асимптотике была неизвестна. Указан способ нахождения этой константы. В семействе таких базисов выделен достаточно широкий подкласс, в котором получены оценки высокой степени точности для соответствующей функции Шеннона. 2. Изучена модель обобщённой глубины схем из функциональных элементов в конечном полном базисе, в которой глубина базисного элемента - положительная целочисленная величина - по любому из его входов складывается из двух независимых компонент: глубины межэлементного соединения входа указанного элемента с выходом подключённой сверху надсхемы ограниченного размера и, собственно, внутренней глубины рассматриваемого элемента. В рассматриваемой модели для широкого класса так называемых равномерных по глубине базисов получены асимптотические оценки высокой степени точности функции Шеннона для обобщённой глубины функций алгебры логики от заданных n переменных и обобщённой глубины мультиплексорной функции, а также получены аналогичные асимптотические оценки для базисов произвольного вида. 3. Доказано, что для стремящегося к бесконечности натурального n почти все булевы функции от n переменных допускают реализацию их такими схемами из функциональных элементов в стандартном базисе, у которых размерность булева куба, допускающего изоморфное вложение схемы, и глубина схемы отличаются от минимально возможных значений не более чем на константу и асимптотически не более чем в три раза соответственно. 4. Получен порядок динамической активности для схем из функциональных элементов в стандартном базисе, реализующих мультиплексорную функцию. Показана возможность одновременной оптимизации схем, реализующих указанную функцию, как по сложности, так и по динамической активности. 5. Разработаны методы синтеза двухполюсных контактных и обобщенных контактных схем, с константной входной избыточностью реализующих произвольную булеву функцию n переменных и допускающих единичный проверяющий тест не зависящей от n длины. Разработан метод синтеза двухполюсных обобщенных контактных схем, реализующих (с несколькими фиктивными переменными) произвольную булеву функцию n переменных и допускающих единичный проверяющий тест не зависящей от n длины. 6. Получены асимптотические оценки высокой степени точности функции Шеннона длины проверяющего теста относительно вытеснений, асимптотика функции Шеннона длины диагностического теста относительно вытеснений, точное значение длины минимального проверяющего теста относительно вытеснений, асимптотика функции Шеннона длины проверяющего теста относительно линейных k-кратных слипаний. 7. Разработаны алгоритмы проверки эквивалентности и свойств ограниченной недетерминированности для конечных автоматов-преобразователей над полугруппами. Разработан эффективный алгоритм минимизации схем последовательных программ, применимый к моделям с семантикой, допускающей эффективную проверку эквивалентности схем. 8. Разработан и программно реализован алгоритм перестроения реляционной модели программно-конфигурируемой сети при изменении загрузки коммутаторов для оперативной верификации политик маршрутизации сети, учитывающий приоритеты правил коммутации.