ИСТИНА

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

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, где «вес» «слившихся» вершин больше, чем «вес» остальных, и для сложности формул стандартного базиса с ограниченной глубиной альтернирования, соответственно. Поведение функции Шеннона для задержки СФЭ в некоторых содержательных моделях установлено на уровне АОВСТ и на уровне близких к ним оценок. В направлении, связанном с тестированием схем, участники проекта имеют опыт в получении рекордных оценок функций Шеннона длин тестов при неисправностях элементов в схемах и при неисправностях на входах схем. В направлении, связанном с теоретическим программированием, участниками темы разработаны общие методы построения эффективных алгоритмов распознавания эквивалентности программ, теория аппроксимации отношения эквивалентности для моделей программ, методы верификации моделей распределённых программ и формул темпоральных логик, методы маскировки программ.