![]() |
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ЦЭМИ РАН |
||
Теория дискретных управляющих систем является интенсивно развивающейся областью дискретной математики и математической кибернетики. Ее развитие обусловлено как появлением новых направлений (и, в частности, направления, связанного с получением асимптотических оценок высокой степени точности), так и прогрессом в традиционных направлениях (например, в разработке методов и алгоритмов анализа, верификации, тестирования и оптимизации различных моделей управляющих систем, включая модели СБИС и модели программ). С другой стороны, теоретические результаты, полученные в этой области, находят применение при решении различных прикладных задач. К их числу относятся задачи проектирования современных СБИС наноуровня, задачи проектирования и верификации распределенных информационных систем, задачи оптимизации программ. Все это дает основание говорить о целесообразности проведения как теоретических исследований по предлагаемой теме, так и исследований, связанных с применением полученных результатов в областях проектирования СБИС и системного программирования.
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. Разработан и программно реализован алгоритм перестроения реляционной модели программно-конфигурируемой сети при изменении загрузки коммутаторов для оперативной верификации политик маршрутизации сети, учитывающий приоритеты правил коммутации.
МГУ имени М.В.Ломоносова | Координатор |
госбюджет, раздел 0110 (для тем по госзаданию) |
# | Сроки | Название |
1 | 1 января 2014 г.-31 декабря 2014 г. | Теория дискретных управляющих систем, ее приложения в проектировании СБИС и программировании |
Результаты этапа: 1. Получено более компактное представление оператора итеративного замыкания, введенного в работе С.А. Ложкина для классификации полных базисов из элементов с прямыми и итеративными переменными. При этом в каждом из семейств указанной классификации, кроме двух, в которых функция Шеннона для любого базиса имеет «стандартный» порядок роста 2n/log n, приведены примеры базисов с порядком роста этой функции, равным 2n. Отдельно показано существование функций, которые могут быть самыми сложными по порядку роста в классе формул над одним базисом, но при небольших изменениях базиса, оставляющих его в том же семействе упомянутой классификации, сложность таких функций кардинально меняется. 2. Разработаны методы синтеза и получены более точные нижние оценки сложности схем из функциональных элементов (СФЭ), реализующих квазимультиплексорные функции алгебры логики (ФАЛ). 3. Разработаны методы синтеза асимптотически оптимальных по задержке СФЭ в одной модели, где положительная задержка на входе элемента произвольным образом зависит как от номера этого входа, так и от типа подключенного сверху элемента, и в другой модели, где к указанным параметрам задержки добавляется ее зависимость от наборов, поступающих на вход рассматриваемого элемента. В этих моделях установлена асимптотика функции Шеннона для задержки и задержки мультиплексорной ФАЛ. Получены асимптотические оценки высокой степени точности функции Шеннона для задержки и задержки мультиплексорной ФАЛ в широком классе базисов первого типа. 4. Проведена дальнейшая разработка методов синтеза и получение более точных новых нетривиальных верхних и нижних оценок динамической активности ФАЛ в некоторых моделях дискретных управляющих систем. 5. Установлено точное значение размерности единичного гиперкуба, допускающего вложение древовидной BDD определенного вида, реализующей мультиплексорную функцию. 6. Найдены нетривиальные оценки функции Шеннона длины проверяющего теста относительно монотонных симметрических слипаний и точное значение функции Шеннона длины диагностического теста относительно монотонных симметрических слипаний входов схем. 7. Улучшена до асимптотики оценка функции Шеннона длины проверяющего теста относительно локальных k-кратных линейных слипаний входов схем. 8. Доказано, что длина минимального проверяющего теста для почти всех булевых функций относительно вытесняющих неисправностей входов схем равна n+1. 9. Предложен новый базис из функциональных элементов, в котором за константное число наборов можно обнаружить двукратную инверсную неисправность на выходах элементов (при введении константного числа дополнительных выходов). 10. Построен полиномиальный по времени алгоритм проверки эквивалентности программ с операторами, подчиняющимися законам коммутативности и подавления. 11. Доказана разрешимость задачи проверки подобия программ относительно отношения логико-термальной эквивалентности, получена оценка сложности указанной задачи. | ||
2 | 1 января 2015 г.-31 декабря 2015 г. | Теория дискретных управляющих систем, ее приложения в проектировании СБИС и программировании |
Результаты этапа: 1. Получена асимптотика функции Шеннона для сложности булевых формул в классе полных базисов из элементов с прямыми и итеративными входами, итеративное замыкание которых содержит класс монотонных функций. В таких базисах порядок роста этой функции является «стандартным» для булевых формул, однако константа в асимптотике была неизвестна. Указан способ нахождения этой константы. В семействе таких базисов выделен достаточно широкий подкласс, в котором получены оценки высокой степени точности для соответствующей функции Шеннона. 2. Изучена модель обобщённой глубины схем из функциональных элементов в конечном полном базисе, в которой глубина базисного элемента - положительная целочисленная величина - по любому из его входов складывается из двух независимых компонент: глубины межэлементного соединения входа указанного элемента с выходом подключённой сверху надсхемы ограниченного размера и, собственно, внутренней глубины рассматриваемого элемента. В рассматриваемой модели для широкого класса так называемых равномерных по глубине базисов получены асимптотические оценки высокой степени точности функции Шеннона для обобщённой глубины функций алгебры логики от заданных n переменных и обобщённой глубины мультиплексорной функции, а также получены аналогичные асимптотические оценки для базисов произвольного вида. 3. Доказано, что для стремящегося к бесконечности натурального n почти все булевы функции от n переменных допускают реализацию их такими схемами из функциональных элементов в стандартном базисе, у которых размерность булева куба, допускающего изоморфное вложение схемы, и глубина схемы отличаются от минимально возможных значений не более чем на константу и асимптотически не более чем в три раза соответственно. 4. Получен порядок динамической активности для схем из функциональных элементов в стандартном базисе, реализующих мультиплексорную функцию. Показана возможность одновременной оптимизации схем, реализующих указанную функцию, как по сложности, так и по динамической активности. 5. Разработаны методы синтеза двухполюсных контактных и обобщенных контактных схем, с константной входной избыточностью реализующих произвольную булеву функцию n переменных и допускающих единичный проверяющий тест не зависящей от n длины. 6. Разработан метод синтеза двухполюсных обобщенных контактных схем, реализующих (с несколькими фиктивными переменными) произвольную булеву функцию n переменных и допускающих единичный проверяющий тест не зависящей от n длины. 7. Найден пример полного базиса, в котором для любой булевой функции существует неизбыточная схема, допускающая единичный проверяющий тест константной длины при константных неисправностях на входах и выходах элементов. 8. Получены асимптотические оценки высокой степени точности функции Шеннона длины проверяющего теста относительно вытеснений, асимптотика функции Шеннона длины диагностического теста относительно вытеснений, точное значение длины минимального проверяющего теста относительно вытеснений, асимптотика функции Шеннона длины проверяющего теста относительно локальных линейных k-кратных слипаний. 9. Разработаны алгоритмы проверки эквивалентности и свойств ограниченной недетерминированности для конечных автоматов-преобразователей над полугруппами. Разработан эффективный алгоритм минимизации схем последовательных программ, применимый к моделям с семантикой, допускающей эффективную проверку эквивалентности схем. 10. Разработан и программно реализован алгоритм перестроения реляционной модели программно-конфигурируемой сети при изменении загрузки коммутаторов для оперативной верификации политик маршрутизации сети, учитывающий приоритеты правил коммутации. | ||
3 | 1 января 2016 г.-31 декабря 2016 г. | Теория дискретных управляющих систем, ее приложения в проектировании СБИС и программировании, этап 2016 года |
Результаты этапа: Разработаны методы синтеза и установлены асимптотические оценки различной степени точности для «сложности» реализации как типичных или самых «сложных» функций, так и специальных функций, встречающихся в приложениях, в различных классах схем. Создан метод оптимизации решения задачи размещения элементов интегральной схемы за счет анализа ряда структурных характеристик графа интегральной схемы. Разработаны алгоритмы для решения задачи разбиения схем из функциональных элементов на соответствующие эквивалентные подсхемы, позволяющие ускорять решение задачи проверки эквивалентности и функциональной коррекции схем большой размерности. Проведена модификация комплекса программ OpenFLUX2 для расчета скоростей метаболических реакций в живой клетке на основе данных, полученных при помощи экспериментов с тяжелыми изотопами углерода, которая позволила в 10 раз уменьшить время расчета. Разработаны методы синтеза логических схем, обеспечившие получение новых оценок некоторых функций Шеннона длины теста, отличающихся от точных значений не более чем на константу. Получены новые оценки функций Шеннона длины тестов при неисправностях на входах схем. Получено решение задачи минимизации автоматов-преобразователей над одним классом полугрупп, разработан полиномиальный по времени алгоритм проверки свойства $k$-значности работающих над вложимыми в разрешимые группы полугруппами конечных автоматов-преобразователей, установлена алгоритмическая неразрешимость задачи проверки логико-термальной эквивалентности для недетерминированных стандартных схем программ, разработан эффективный алгоритм проверки эквивалентности программ в модели с перестановочными и подавляемыми операторами. | ||
4 | 1 января 2017 г.-31 декабря 2017 г. | Теория дискретных управляющих систем, ее приложения в проектировании СБИС и программировании, этап 2017 года |
Результаты этапа: Разработаны методы синтеза и установлены асимптотические оценки различной степени точности для «сложности» реализации в различных классах схем как типичных или самых «сложных» функций, так и специальных функций, встречающихся в приложениях. Разработаны, в частности, оптимальные на уровне асимптотических оценок высокой степени точности методы синтеза схем из функциональных элементов (СФЭ) в одном специальном полном базисе из элементов с прямыми и итеративными переменными. Установлено асимптотическое поведение функции Шеннона для сложности рекурсивных СФЭ с ограниченной глубиной рекурсии над произвольным конечным полным базисом. Установлено асимптотическое поведение функции Шеннона для обобщённой задержки СФЭ в некоторых моделях задержки, где эта величина зависит от степени ветвления выходов элементов схемы. Предложен полиномиальный алгоритм гомеоморфного вложения полного двоичного дерева в плоские прямоугольные решетки с расположением листьев дерева на её противоположных сторонах, который позволяет получать асимптотически оптимальные по площади вложения указанного вида. Разработаны методы синтеза асимптотически оптимальных по сложности контактных схем, имеющих оптимальный порядок роста динамической активности. Разработаны методы синтеза логических схем, обеспечившие получение новых оценок некоторых функций Шеннона длины теста, отличающихся от точных значений не более чем на константу. Получены новые оценки функций Шеннона длины тестов при неисправностях на входах схем. Установлена алгоритмическая разрешимость задачи минимизации стандартных схем программ относительно логико-термальной эквивалентности. Показано, что существуют минимальные неизоморфные логико-термально эквивалентные стандартные схемы программ. Доказано, что задачи проверки эквивалентности и минимизации стандартных схем программ относительно логико-термальной эквивалентности взаимносводима к аналогичным задачам для конечных автоматов-преобразователей, работающих над полугруппой конечных подстановок. На основании этого утверждения установлена алгоритмическая разрешимость указанных задач для конечных автоматов-преобразователей, работающих над полугруппой конечных подстановок. Предложен полиномиальный по времени алгоритм минимизации стандартных схем программ, в которых вычислительный эффект всех линейных участков характеризуется ортогональными консервативными постановками. Установлено, что алгоритмически неразрешима задача проверки выполнимости формул темпоральной логики линейного времени, в которой все темпоральные операторы параметризованы регулярными выражениями, на моделях, представленных автоматами-преобразователями, работающими над частично перестановочными полугруппами и абелевыми группами. Показано, что задача проверки выполнимости формул арифметики Пресбургера сводима к задаче проверки выполнимости формул происшествия параметризованной темпоральной логики линейного времени на моделях, представленных автоматами-преобразователями, работающими над абелевыми группами. Установлена возможность построения алгоритма трансляции иерархических временных автоматов в сети плоских временных автоматов. | ||
5 | 1 января 2018 г.-31 декабря 2018 г. | Теория дискретных управляющих систем, ее приложения в проектировании СБИС и программировании, этап 2018 года |
Результаты этапа: Разработаны новые методы синтеза формул в некоторых полных базисах из функциональных элементов с прямыми и итеративными входами. При этом для ряда специальных симметричных базисов установлены новые АОВСТ функции Шеннона для сложности реализации ФАЛ, зависящих от заданного числа переменных. Созданы метода синтеза рефлексивно-рекурсивных СФЭ над произвольным конечным полным базисом, имеющих ограниченную глубину рекурсии. С помощью этих методов установлено асимптотическое поведение функции Шеннона для сложности указанных СФЭ. Установлена асимптотика минимально возможной площади прямоугольной решетки, допускающей гомеоморфное вложение полного двоичного дерева с расположением листьев дерева на ее противоположных сторонах. Разработаны методы синтеза гомеоморфно вложенных в единичный куб СФЭ в стандартном базисе, позволяющие проводить оптимизацию размерности куба и глубины СФЭ на уровне более высоких, по сравнению с известными ранее, значений указанных параметров для почти всех ФАЛ. Получены новые более высокие нижние оценки сложности реализации мультиплексорных ФАЛ в классе контактных схем. Разработан метод синтеза асимптотически оптимальных по глубине усилительных СФЭ (УСФЭ) в новой модели обобщённой глубины, где глубина зависит как от типов функциональных элементов, так и от степени ветвления выходов функциональных элементов. На основе разработанного метода для глубины почти всех ФАЛ установлены близкие к АОВСТ асимптотические оценки глубины этих ФАЛ. Получены асимптотические оценки указанного вида для функции Шеннона обобщённой глубины ФАЛ от n переменных в классе УСФЭ в указанной модели. Доказано, что функция Шеннона длины единичного диагностического теста относительно инверсных неисправностей на выходах элементов во всех базисах, содержащих конъюнкцию или дизъюнкцию двух переменных, не больше 4. Получены порядковые и асимптотические оценки функций Шеннона длины диагностического теста относительно единичной константной неисправности и циклического сдвига всех переменных (в т. ч. при ограничениях на вид блоков, в которых происходят сдвиги). Доказано, что для каждой булевой функции существует двухполюсная контактная схема, реализующая эту функцию при отождествлениях переменных и забиваниях переменных константами и допускающая единичный проверяющий тест длины 10. Исследована задача проверки свойства строгой детерминированности для конечных автоматов-преобразователей, работающих в реальном времени. Свойство строгой детерминированности требует, чтобы для каждой последовательности входных сигналов соответствующая последовательность выходных откликов была одной и той же независимо от времени поступления входных сигналов. Установлены необходимые и достаточные условия строгой детерминированности автоматов-преобразователей, работающих в реальном времени. Показано, что задача проверки свойства строгой детерминированности автоматов-преобразователей является co-NP-полной. Предложен новый язык спецификаций поведения конечных автоматов-преобразователей над полугруппами, представляющий собой расширение языка логики деревьев вычислений CTL. Для предложенного языка спецификаций построен алгоритм верификации реагирующих систем, моделируемых автоматами-преобразователями, доказаны корректность и полнота построенного алгоритма, получены оценки его вычислительной сложности. Выделены и исследованы два фрагмента введенного языка спецификаций, семантика которых может быть задана на классических моделях Крипке; для выделенных фрагментов построены алгоритмы верификации моделей Крипке, имеющие полиномиальную сложность относительно размеров проверяемых моделей и анализируемых формул. В параметризованном расширении темпоральной логики линейного времени LP-LTL, предназначенном для спецификации поведения моделей реагирующих программ, выделены два фрагмента, семантика которых может быть задана на классических моделях Крипке - LP-1-LTL и LP-n-LTL. Проведено сравнение выразительных возможностей выделенных фрагментов и ранее известных логик, используемых для спецификации параллельных вычислений. Удалось показать, что фрагмент логики LP-1-LTL является строго более выразительной, нежели темпоральная логика LTL, а фрагмент LP-n-LTL и монадическая логика предикатов с одной функцией следования S1S обладают одинаковыми выразительными способностями. Исследована задача проверки информационной безопасности протоколов, описанных при помощи базовых средств исчисления мобильных процессов (пи-исчисления). Предложено расширение исчисления мобильных процессов, позволяющее добавлять к моделям протоколов модели пассивного противника. Сформулировано требование стойкости (информационной безопасности) протоколов относительно атак и угроз в модели пассивного противника. Показано, что задача проверки требования информационной безопасности протоколов в модели пассивного противника является co-NP-полной. Исследована задача проверки эквивалентности для класса слабо недетерминированных автоматов-преобразователей над свободной полугруппой. Показано, что эта задача разрешима за время полиномиальное относительно размеров проверяемых автоматов. Показано также, что задача проверки эквивалентности двухленточных автоматов сводима к задаче проверки эквивалентности слабо недетерминированных автоматов-преобразователей. Исследована задача минимизации конечных автоматов-преобразователей, работающих над полугруппой регулярных префиксных языков. Доказано, что в полугруппе регулярных префиксных языков можно ввести отношение частичного порядка, относительно которого данная полугруппа образует решетку, удовлетворяющую свойству обрыва убывающих цепей. Доказано, что полугруппа регулярных префиксных языков обладает свойством левой сократимости. На основании этих свойств построен полиномиальный по времени алгоритм минимизации конечных автоматов-преобразователей, работающих над полугруппой регулярных префиксных языков. Предложена модификация алгоритма уплощения иерархических временных автоматов, разработанного на предыдущем этапе проекта, применимая к более широкому классу иерархических автоматов. Предложен алгебраический язык преобразования диаграмм сигналов, возникающих на ранних стадиях разработки цифровой аппаратуры. |
Для прикрепления результата сначала выберете тип результата (статьи, книги, ...). После чего введите несколько символов в поле поиска прикрепляемого результата, затем выберете один из предложенных и нажмите кнопку "Добавить".