Дискретно-временное стохастическое и детерминированное исчисление боксов Петри dtsdPBC
Ключевые слова:
стохастическая процессная алгебра, исчисление боксов Петри, дискретное время, стохастическое мультидействие, детерминированное мультидействие, система переходов, операционная семантика, семантический пример.Аннотация
Мы предлагаем dtsdPBC, расширение детерминированно-временными мультидействиями дискретно-временного стохастического и мгновенного исчисления боксов Петри (dtsiPBC), ранее представленного И.В. Тарасюком, Х. Масией и В. Валеро. dtsdPBC повышает выразительность dtsiPBC и расширяет область применения связанных с ним техник спецификации и анализа. В dtsdPBC неотрицательные целые числа используются для представления фиксированных (включая нулевые) временных задержек детерминированных мультидействий. Шаговая операционная семантика конструируется посредством помеченных вероятностных систем переходов. Серия примеров построения таких систем переходов для выражений с различными типами мультидействий и операций демонстрирует как возможности спецификации, так и семантические особенности нового исчисления.
