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