Performance preserving equivalence for stochastic process algebra dtsdPBC
Ключевые слова:
исчисление боксов Петри, дискретное время, стохастические и детерминированные задержки, система переходов, операционная семантика, dtsd-бокс, денотационная семантика, цепь Маркова, производительность, категоризацияАннотация
Исчисление боксов Петри (PBC) А. Беста, Р. Девиллерса, Дж.Г. Холла и М. Кутни - хорошо известная алгебра параллельных процессов с семантикой сетей Петри. Дискретно-временное стохастическое и детерминированное PBC
(dtsdPBC) автора расширяет PBC дискретно-временными стохастическими и детерминированными задержками. dtsdPBC обладает шаговой операционной семантикой на базе помеченных вероятностных систем переходов и основанной на сетях Петри денотационной семантикой на базе dtsd-боксов, подкласса помеченных дискретно-временных стохастических и детерминированных сетей Петри (ПДВСДСП). Для оценки производительности в dtsdPBC анализируются базовые полумарковские цепи (ПМЦ) и (редуцированные) дискретно-временные цепи Маркова (ДВМЦ и РДВМЦ) процессных выражений. Шаговая стохастическая бисимуляционная эквивалентность используется в dtsdPBC как для сравнения качественного и количественного поведения, так и для установления соответствия операционной и денотационной семантик.
Мы демонстрируем как применять шаговую стохастическую бисимуляционную эквивалентность процессных выражений для категоризации их систем переходов, ПМЦ, ДВМЦ и РДВМЦ с сохранением стационарного поведения и свойств времени пребывания. Мы также доказываем, что категоризованные поведенческие структуры (системы переходов, графы достижимости и ПМЦ) процессных выражений и их dtsd-боксов изоморфны. Так как данная эквивалентность гарантирует идентичность функциональных и производительных характеристик в классах эквивалентности, ее можно применять для упрощения анализа производительности в рамках dtsdPBC благодаря минимизации пространства состояний с помощью категоризации.
