Classical workflow nets and workflow nets with reset arcs: using Lyapunov stability for soundness verification. Issue 1 (2nd January 2017)

• Record Type: Journal Article
• Authors: Clempner, Julio B.
• Is Part Of: Journal of experimental & theoretical artificial intelligence. Volume 29:Issue 1(2017)
• Page Start: 43
• Page End: 57
• Publication Date: 2017-01-02
• Subjects: Workflow nets -- Lyapunov stability -- soundness -- decidability -- verification -- traffic signal-control -- Petri nets; Artificial intelligence -- Periodicals; 006.3
• DOI: 10.1080/0952813X.2015.1080472
• Languages: English
• ISSNs: 0952-813X

Abstract

Abstract : This paper presents a novel analytical method for soundness verification of workflow nets and reset workflow nets, using the well-known stability results of Lyapunov for Petri nets. We also prove that the soundness property is decidable for workflow nets and reset workflow nets. In addition, we provide evidence of several outcomes related with properties such as boundedness, liveness, reversibility and blocking using stability. Our approach is validated theoretically and by a numerical example related to traffic signal-control synchronisation.