-
Time Petri Nets with Dynamic Firing Dates: Semantics and Applications
Authors:
Silvano Dal Zilio,
Lukasz Fronc,
Bernard Berthomieu,
François Vernadat
Abstract:
We define an extension of time Petri nets such that the time at which a transition can fire, also called its firing date, may be dynamically updated. Our extension provides two mechanisms for updating the timing constraints of a net. First, we propose to change the static time interval of a transition each time it is newly enabled; in this case the new time interval is given as a function of the c…
▽ More
We define an extension of time Petri nets such that the time at which a transition can fire, also called its firing date, may be dynamically updated. Our extension provides two mechanisms for updating the timing constraints of a net. First, we propose to change the static time interval of a transition each time it is newly enabled; in this case the new time interval is given as a function of the current marking. Next, we allow to update the firing date of a transition when it is persistent, that is when a concurrent transition fires. We show how to carry the widely used state class abstraction to this new kind of time Petri nets and define a class of nets for which the abstraction is exact. We show the usefulness of our approach with two applications: first for scheduling preemptive task, as a poor man's substitute for stopwatch, then to model hybrid systems with non trivial continuous behavior.
△ Less
Submitted 28 April, 2014;
originally announced April 2014.
-
Model Checking Contest @ Petri Nets, Report on the 2013 edition
Authors:
Fabrice Kordon,
Alban Linard,
Marco Beccuti,
Didier Buchs,
Łukasz Fronc,
Lom-Messan Hillah,
Francis Hulin-Hubard,
Fabrice Legond-Aubry,
Niels Lohmann,
Alexis Marechal,
Emmanuel Paviot-Adet,
Franck Pommereau,
César Rodríguez,
Christian Rohr,
Yann Thierry-Mieg,
Harro Wimmel,
Karsten Wolf
Abstract:
This document presents the results of the Model Checking Contest held at Petri Nets 2013 in Milano. This contest aimed at a fair and experimental evaluation of the performances of model checking techniques applied to Petri nets. This is the third edition after two successful editions in 2011 and 2012.
The participating tools were compared on several examinations (state space generation and evalu…
▽ More
This document presents the results of the Model Checking Contest held at Petri Nets 2013 in Milano. This contest aimed at a fair and experimental evaluation of the performances of model checking techniques applied to Petri nets. This is the third edition after two successful editions in 2011 and 2012.
The participating tools were compared on several examinations (state space generation and evaluation of several types of formulæ -- reachability, LTL, CTL for various classes of atomic propositions) run on a set of common models (Place/Transition and Symmetric Petri nets).
After a short overview of the contest, this paper provides the raw results from the contest, model per model and examination per examination. An HTML version of this report is also provided (http://mcc.lip6.fr).
△ Less
Submitted 10 September, 2013;
originally announced September 2013.
-
Effective Marking Equivalence Checking in Systems with Dynamic Process Creation
Authors:
Łukasz Fronc
Abstract:
The starting point of this work is a framework allowing to model systems with dynamic process creation, equipped with a procedure to detect symmetric executions (ie., which differ only by the identities of processes). This allows to reduce the state space, potentially to an exponentially smaller size, and, because process identifiers are never reused, this also allows to reduce to finite size some…
▽ More
The starting point of this work is a framework allowing to model systems with dynamic process creation, equipped with a procedure to detect symmetric executions (ie., which differ only by the identities of processes). This allows to reduce the state space, potentially to an exponentially smaller size, and, because process identifiers are never reused, this also allows to reduce to finite size some infinite state spaces. However, in this approach, the procedure to detect symmetries does not allow for computationally efficient algorithms, mainly because each newly computed state has to be compared with every already reached state.
In this paper, we propose a new approach to detect symmetries in this framework that will solve this problem, thus enabling for efficient algorithms. We formalise a canonical representation of states and identify a sufficient condition on the analysed model that guarantees that every symmetry can be detected. For the models that do not fall into this category, our approach is still correct but does not guarantee a maximal reduction of state space.
△ Less
Submitted 13 February, 2013;
originally announced February 2013.
-
Raw Report on the Model Checking Contest at Petri Nets 2012
Authors:
F. Kordon,
A. Linard,
D. Buchs,
M. Colange,
S. Evangelista,
L. Fronc,
L. M. Hillah,
N. Lohmann,
E. Paviot-Adet,
F Pommereau,
C. Rohr,
Y. Thierry-Mieg,
H. Wimmel,
K. Wolf
Abstract:
This article presents the results of the Model Checking Contest held at Petri Nets 2012 in Hambourg. This contest aimed at a fair and experimental evaluation of the performances of model checking techniques applied to Petri nets. This is the second edition after a successful one in 2011.
The participating tools were compared on several examinations (state space generation and evaluation of sever…
▽ More
This article presents the results of the Model Checking Contest held at Petri Nets 2012 in Hambourg. This contest aimed at a fair and experimental evaluation of the performances of model checking techniques applied to Petri nets. This is the second edition after a successful one in 2011.
The participating tools were compared on several examinations (state space generation and evaluation of several types of formulae - structural, reachability, LTL, CTL) run on a set of common models (Place/Transition and Symmetric Petri nets).
After a short overview of the contest, this paper provides the raw results from the context, model per model and examination per examination.
△ Less
Submitted 8 September, 2012;
originally announced September 2012.
