Diagnosability and Predictability of pattern in Labelled Petri Nets

International audienceThis paper addresses the problem of checkingpredictability of event patterns in labelled Petrinets. After formally introducing the predictabil-ity problem of an event pattern, a method for au-tomatically checking predictability is proposed.The proposed method has two steps. The firstone consists in checking diagnosability of eventpatterns which is a necessary condition for pre-dictability. And, if diagnosability holds, the sec-ond step is launched and concludes about thepredictability of the investigated event pattern.The proposed method uses a model-checking ap-proach and is fully implemented with the help ofa model-checking toolchain