Paper Info
Title
Optimal Liveness-Enforcing Control for a Class of Petri Nets Arising in Multithreaded Software.
Abstract
We investigate the synthesis of optimal liveness-enforcing control policies for Gadara nets, a special class of Petri nets that arises in the modeling of the execution of multithreaded computer programs for the purpose of deadlock avoidance. We consider maximal permissiveness as the notion of optimality. Deadlock-freeness of a multithreaded program corresponds to liveness of its Gadara net model. We present a new control synthesis algorithm for liveness enforcement of Gadara nets that need not be ordinary. The algorithm employs structural analysis of the net and synthesizes monitor places to prevent the formation of a special class of siphons, termed resource-induced deadly-marked siphons. The algorithm also accounts for uncontrollable transitions in the net in a minimally restrictive manner. The algorithm is generally an iterative process and converges in a finite number of iterations. It exploits a covering of the unsafe states that is updated at each iteration. The proposed algorithm is shown to be correct and maximally permissive with respect to the goal of liveness enforcement.
Year
DOI
Venue
2013
10.1109/TAC.2012.2230814
IEEE Trans. Automat. Contr.
Keywords
Field
DocType
Monitoring,System recovery,Petri nets,Process control,Software,Automata,Computational modeling
Mathematical optimization,Petri net,Optimal control,Iterative and incremental development,Computer science,Deadlock,Stochastic Petri net,Process architecture,Theoretical computer science,Software,Liveness
Journal
Volume
Issue
ISSN
58
5
0018-9286
Citations 
PageRank 
References 
6
0.53
7
Authors
5
Name
Order
Citations
PageRank
Hongwei Liao11159.58
StéPhane Lafortune21738181.23
Spyros A. Reveliotis336429.24
Yin Wang431516.98
Scott Mahlke54811312.08