Please use this identifier to cite or link to this item:
Scopus Web of Science® Altmetric
Type: Conference paper
Title: Modular state spaces for prioritised petri nets
Author: Lakos, C.
Petrucci, L.
Citation: Foundations of Computer Software: Modeling, Development, and Verification of Adaptive Systems, 2011 / vol.6662 LNCS, pp.136-156
Publisher: Springer-Verlag Berlin
Publisher Place: Heidelberger Platz 3 Berlin Germany D-14197
Issue Date: 2011
Series/Report no.: Lecture Notes in Computer Science; 6662
ISBN: 9783642212918
ISSN: 0302-9743
Conference Name: 16th Monterey Workshop (31 Mar 2010 - 02 Apr 2010 : Redmond, WA, USA)
Statement of
Charles Lakos, and Laure Petrucci
Abstract: Verification of complex systems specification often encounters the so-called state space explosion problem, which prevents exhaustive model-checking in many practical cases. Many techniques have been developed to counter this problem by reducing the state space, either by retaining a smaller number of relevant states, or by using a smart representation. Among the latter, modular state spaces [CP00, LP04] have turned out to be an efficient analysis technique in many cases [Pet05]. When the system uses a priority mechanism (e.g. timed systems [LP07]), there is increased coupling between the modules — preemption between modules can occur, thus disabling local events. This paper shows that the approach is still applicable even when considering dynamic priorities, i.e. priorities depending both on the transition and the current marking.
Keywords: Modular state spaces; prioritised Petri Nets
Rights: © Springer-Verlag Berlin Heidelberg 2011
RMID: 0020111791
DOI: 10.1007/978-3-642-21292-5_8
Published version:
Appears in Collections:Computer Science publications

Files in This Item:
There are no files associated with this item.

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.