Minimality of critical scenarios with linear logic and cutsets

Abstract

This work proposes a new approach for analyzing the dependability of mechatronic systems; its goal is to extract all minimal feared scenarios that lead a system in a state of failure, directly from the proof trees of linear logic to establish the causality between undesirable events and normal operations. The proof trees of linear logic contain events that are the result of event in the scenario, but not strictly necessary for the final production of the critical feared state. The size of the proof tree is proportional to the number of firing transitions in the sequent provable. The proposed approach is based on the concept of minimal cutsets of the fault tree method applied to the proof trees of linear logic of Petri net model in an unknown context. The aim is to reduce the size of the proof trees of linear logic and generate a minimum number of feared scenarios.

Keywords: Dependability - Mechatronic systems -Petri net - Linear logic - Minimal Feared scenarios - Cutsets

Ce travail propose une nouvelle approche d'analyse de la sûreté de fonctionnement des systèmes mécatroniques. Son objectif est d’extraire les scénarios redoutés minimaux qui conduisent un système vers un état de défaillance, à partir des arbres de preuves de la logique linéaire et établir les liens de causalité entre les événements redoutés et les fonctionnements normaux. Les arbres de preuves de la logique linéaire contiennent des événements qui sont la conséquence d’événement inclus dans le scénario, mais qui ne sont pas strictement nécessaires à l’obtention de l’état critique redouté final. La taille de l’arbre de preuve est proportionnelle au nombre de franchissement des transitions dans le séquent prouvable. L’approche proposée est basée sur la notion de coupe minimale de la méthode des arbres de défaillances appliquées aux arbres de preuves de la logique linéaire du modèle réseau de Pétri dans un contexte inconnu. L’objectif est de réduire la taille des arbres de preuves de la logique linéaire et de générer un nombre minimal de scénarios redoutés.

Mots clés: Sûreté de fonctionnement - Systèmes Mécatroniques - Réseaux de Petri - Logique linéaire - Scénarios redoutés minimaux - Coupe minimales