Getting the Priorities Right: Saturation for Prioritised Petri Nets

Marussy, Kristóf and Molnár, Vince and Vörös, András and Majzik, István (2017) Getting the Priorities Right: Saturation for Prioritised Petri Nets. In: Application and Theory of Petri Nets and Concurrency. Lecture Notes in Computer Science (10258). Springer International Publishing, Cham (Svájc), pp. 223-242. ISBN 978-3-319-57860-6

Preview

Text main.pdf Download (634kB) | Preview

Abstract

Prioritised Petri net is a powerful modelling language that often constitutes the core of even more expressive modelling languages such as GSPNs (Generalized Stochastic Petri nets). The saturation state space traversal algorithm has proved to be efficient for non-prioritised concurrent models. Previous works showed that priorities may be encoded into the transition relation, but doing so defeats the main idea of saturation by spoiling the locality of transitions. This paper presents an extension of saturation to natively handle priorities by considering the priority-related enabledness of transitions separately, adopting the idea of constrained saturation. To encode the highest priority of enabled transitions in every state we introduce edge-valued interval decision diagrams. We show that in case of Petri nets, this data structure can be constructed offline. According to preliminary measurements, the proposed solution scales better than previously known matrix decision diagram-based approaches, paving the way towards efficient stochastic analysis of GSPNs and the model checking of prioritised models.

Actions (login required)

Edit Item