Лаборатория теории параллельных процессов

Заведующий – Вирбицкайте Ирина Бонавентуровна

Исследования лаборатории направлены на разработку, исследование и применение формальных методов и средств спецификации, анализа и верификации параллельных систем со сложной структурной организацией, поведение которых в значительной степени зависит от количественных временных характеристик. Научно-исследовательские изыскания ведутся в следующих тесно связанных направлениях:

• Теоретико-категорное сравнение параллельных моделей с реальным временем и унификация поведенческих эквивалентностей в семантиках «интерливинг/истинный параллелизм» и «линейного/ветвистого времени».
• Построение иерархий взаимосвязей поведенческих эквивалентностей различных классов и расширений временных и стохастических сетей Петри, формулировка логической характеризации эквивалентностей и решение проблемы их распознавания.
• Исследование свойств достижимости, безопасности, управления моделей различных классов динамических и гибридных систем, совершенствование алгоритмов построения симуляций и бисимуляций, основанных на инвариантах и ограничениях.
• Разработка дискретно-временных стохастических расширений алгебры параллельных процессов, PBC (Petri Box Calculus), определение согласованных шаговой операционная семантики на основе вероятностных систем переходов и денотационной семантики на основе дискретно-временных стохастических сетей Петри. Построение стохастических алгебраических эквивалентностей и исследование их взаимосвязей, а также логическая характеризация стохастических бисимуляционных эквивалентностей формулами вероятностных модальных логик.
• Проектирование алгоритмов параметрической верификации поведения различных классов временных сетей Петри с использованием метода проверки моделей относительно темпоральных логик реального времени.