Double Seminar: Fluidization on Petri nets and Model checking on Fault Diagnosis Graph

Fri, 09/05/2014 - 10:00 - 11:00

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.

Seminario del Departamento