Detection of Illegal Behaviors Based on Unfoldings

We show how the branching process approach can be used for the detection of illegal behaviors. Our study is based on the specification of properties in terms of testers that cover safety as well as liveness properties. We demonstrate that the unfolding method can be used in this context and propose an extension of it, called unfolding graphs, for the definition of failure equivalent graphs. Keywords. Model Checking, Partial Order, Failure Equivalence, Petri Net

• Type: Conference
• Year: 1999
• Where: APN
• Authors: Jean-Michel Couvreur, Denis Poitrenaud
• Keywords: APN 1999, Artificial Intelligence, Branching Process Approach, Failure Equivalent Graphs, Illegal Behaviors