Исследуются поведенческие эквивалентности параллельных систем, моделируемых сетями Петри с невидимыми переходами, помеченными невидимыми действиями τ. τ-эквивалентности - отношения, которые абстрагируются от невидимых действий, соответствующих внутренней активности моделируемой системы. Известные из литературы базисные τ-эквивалентности дополняются новыми понятиями. Выясняются взаимосвязи данных эквивалентностей как на всем классе сетей Петри, так и на двух подклассах: сетях Петри с видимыми переходами, где ни один из переходов не помечен невидимым действием, и последовательных сетях Петри, где нет параллельных срабатываний переходов. Приводится пример сохраняющей эквивалентность редукции сети Петри, моделирующей известную систему обедающих философов. Представлены результаты о разрешимости базисных τ-эквивалентностей.
We investigate behavioural equivalences of concurrent systems modeled by Petri nets with invisible transitions labeled by silent actions. τ-equivalences are the relations which abstract from silent actions corresponding to internal activity of the modeled system. The basic τ-equivalences known from the literature are supplemented by new notions. The interrelations of all the equivalences are determined on the whole class of Petri nets as well as on two subclasses: Petri nets with visible transitions, where no transitions are labeled by the invisible action, and sequential Petri nets, where no concurrent transition firings exist. We present an example of equivalence-preserving reduction of a Petri net that models the well-known dining philosophers system. The decidability results for basic τ-equivalences are outlined.
The authors declare that there are no conflicts of interest present.