Paper Info
Title
Determinization of timed Petri nets behaviors
Abstract
In this paper we are interested in sequentialization of formal power series with coefficients in the semiring which represent the behavior of timed Petri nets. Several approaches make it possible to derive nondeterministic (max, + ) automata modeling safe timed Petri nets. Their nondeterminism is a serious drawback since determinism is a crucial property for numerous results on (max, + ) automata (in particular, for applications to performance evaluation and control) and existing procedures for determinization succeed only for restrictive classes of (max, + ) automata. We present a natural semi-algorithm for determinization of behaviors based on the semantics of bounded timed Petri nets. The resulting deterministic (max, + ) automata can be infinite, but a sufficient condition called strong liveness is proposed to ensure the termination of the semi-algorithm. It is shown that strong liveness is closely related to bounded fairness, which has been widely studied for Petri nets and other models for concurrency. Moreover, if the net cannot be sequentialized we propose a restriction of its logical behavior so that the sufficient condition becomes satisfied for the restricted net. The restriction is based on the synchronous product with non injectively labeled scheduler nets that are built in an incremental hierarchical way from simple scheduler nets.
Year
DOI
Venue
2016
10.1007/s10626-015-0214-1
Discrete Event Dynamic Systems
Keywords
Field
DocType
Timed Petri nets,(max,+ ) automata,Determinization
Discrete mathematics,Petri net,Nondeterministic algorithm,Concurrency,Computer science,Formal power series,Stochastic Petri net,Semiring,Bounded function,Liveness
Journal
Volume
Issue
ISSN
26
3
0924-6703
Citations 
PageRank 
References 
3
0.37
17
Authors
3
Name
Order
Citations
PageRank
Jan Komenda114721.85
Sébastien Lahaye271.46
Jean-Louis Boimond315220.21