3
$\begingroup$

I'm working on a problem where the formalism appears to be an abstraction of a kind of Petri net, and it is possible to construct an equivalent Petri net from this formalism with the same behavior. The Petri net that is constructed is bounded, and a transition is either $L0$-Live or $L1$-Live. So in this net, a transition fires only once or not at all.

I've looked into the coverability of Petri nets and it appears that the coverability problem in general has $\text{EXPSPACE}$ complexity (https://www7.in.tum.de/~blondin/papers/BFHH16.pdf). However, I could not find any literature that relates the liveness of a Petri net to its coverability, and the impact on complexity. Is there any work that has looked into this?

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ In general, liveness is equivalent to reachability. But I'm not sure to understand your specific case, if transitions can be fired at most once, how can the net be deadlock-free? $\endgroup$
    – Michael Blondin
    Nov 8 '17 at 20:05
  • $\begingroup$ @MichaelBlondin You're right -- if a transition can never fire, it is deadlocked. I think I mixed up my terms when I was looking at this (I didn't make the connection between liveness and deadlocking). The net is definitely bounded though; I will edit the question. $\endgroup$
    – Vivin Paliath
    Nov 9 '17 at 4:23
  • 1
    $\begingroup$ Thank you for the update. If a transition can be fired at most once, then the length of any firing sequence is bounded by the number of transitions, and hence the net cannot be live. Am I missing something here? $\endgroup$
    – Michael Blondin
    Nov 9 '17 at 11:09
  • $\begingroup$ @MichaelBlondin Perhaps I am mixing up the liveness of the net and the liveness of the transition. From my pencil and paper "experiments", I see transitions starting and then at some point they stop. Given that they definitely stop, is that what makes the net not "live"? My knowledge of petri nets is pretty shallow and I only started researching it as part of this problem I'm working on. $\endgroup$
    – Vivin Paliath
    Nov 9 '17 at 23:28
  • $\begingroup$ Typically, a transition t is said to be live if "it will always be possible to fire t it in the future", i.e. if from every reachable marking M, it is possible to reach another marking M' at which t is enabled. A net is live if all its transitions are live. If you can reach a marking where none of the transitions are enabled, then this is called a deadlock. $\endgroup$
    – Michael Blondin
    Nov 10 '17 at 10:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.