Аннотация:
Вводится новый класс стохастических сетей Петри (ССП), который является модификацией дискретно-временных ССП (ДВССП) посредством введения пометки и называется помеченными ДВССП (ПДВССП). Воспринимаемое «внешним наблюдателем» поведение ПДВССП описывается посредством помечающих переходы действий, соответствующих элементарным активностям. Определяется динамическое поведение ПДВССП, и конструируется соответствующая дискретно-временная марковская цепь (ДВМЦ). Вводятся поведенческие эквивалентности ПДВССП, представляющие из себя варианты известных следовых и бисимуляционных отношений. Исследуются взаимосвязи всех упомянутых отношений эквивалентности. Дается логическая характеризация данных эквивалентностей в терминах формул вероятностных модальных логик. Демонстрируется, как понятия эквивалентностей можно использовать для сравнения стационарного поведения ПДВССП. Предлагается стохастическая алгебра процессов, формулы которой описывают особый подкласс ПДВССП.