Double Seminar: Fluidization on Petri nets and Model checking on Fault Diagnosis Graph
a) The “bound Reaching Problem” on the Fluidization of Timed Petri Nets
Estíbaliz Fraca, Jorge Júlvez, Manuel Silva.
In
the Petri nets framework, continuous net systems are the result of
removing the integrality constraint in the firing of transitions. This
relaxation may highly reduce the complexity of analysis techniques but
may not approximate some properties of the original system, such as its
throughput. This paper deals with the basic operation of fluidization of
discrete timed Petri nets. More precisely, the “bound reaching problem”
is identified, which points out the differences between discrete and
continuous behaviour in a case in which the probability of a transition
to be enabled is low in the discrete case. An approach denoted
-semantics is proposed to tackle this problem and compared with other
methods.
b) Model Checking on Fault Diagnosis Graph
Xu Wang, Cristian Mahulea, Manuel Silva.
This
talk presents the use of model checking techniques for fault diagnosis
on timed systems. The timed systems are modeled with time Petri nets
(TPN). Our approach is based on the fault diagnosis graph (FDG), which
is obtained from the state class graph of TPN, by removing nodes and
edges that are not used in fault diagnosis. In order to apply the
reduction rules, we assume that the FDG is bounded and completely
constructed. We first propose some reduction rules on the FDG to obtain a
more compact representation and then we use model checking techniques
on the reduced FDG to compute the diagnosis states. We compare the
complexity of model checking on FDG with the one on the reduced FDG.