Irina Lomazova ; Vladimir Bashkin ; Petr Jančar - Resource Bisimilarity in Petri Nets is Decidable

fi:8781 - Fundamenta Informaticae, October 21, 2022, Volume 186, Issues 1-4: Trakhtenbrot's centenary
Resource Bisimilarity in Petri Nets is Decidable

Authors: Irina Lomazova ; Vladimir Bashkin ; Petr Jančar

    Petri nets are a popular formalism for modeling and analyzing distributed systems. Tokens in Petri net models can represent the control flow state or resources produced/consumed by transition firings. We define a resource as a part (a submultiset) of Petri net markings and call two resources equivalent when replacing one of them with another in any marking does not change the observable Petri net behavior. We consider resource similarity and resource bisimilarity, two congruent restrictions of bisimulation equivalence on Petri net markings. Previously it was proved that resource similarity (the largest congruence included in bisimulation equivalence) is undecidable. Here we present an algorithm for checking resource bisimilarity, thereby proving that this relation (the largest congruence included in bisimulation equivalence that is a bisimulation) is decidable. We also give an example of two resources in a Petri net that are similar but not bisimilar.


    Volume: Volume 186, Issues 1-4: Trakhtenbrot's centenary
    Published on: October 21, 2022
    Accepted on: July 7, 2022
    Submitted on: December 1, 2021
    Keywords: Computer Science - Logic in Computer Science

    Share

    Consultation statistics

    This page has been seen 11 times.
    This article's PDF has been downloaded 23 times.