Auswahl der wissenschaftlichen Literatur zum Thema „Manifestability“

Le diagnostic de pannes est une tâche cruciale et difficile dans le contrôle automatique des systèmes complexes, dont l’efficacité dépend d’une propriété du système appelée diagnosticabilité. La diagnosticabilité décrit la propriété du système permettant de déterminer dès la phase de conception si un défaut donné se produisant en ligne sera identifiable avec certitude sur la base des observations disponibles, ce qui est une alternative aux tests qui ne peuvent que montrer la présence de défaillances sans garantir leur absence. Le problème de diagnosticabilité des systèmes à événements discrets a reçu une attention considérable dans la littérature, mais peu nombreux sont les travaux qui prennent en compte des contraintes de temps explicites lors de cette analyse. Or de telles contraintes sont naturellement présentes dans les systèmes réels et ne peuvent être négligées compte tenu de leur impact sur cette propriété. Nous avons proposé dans notre travail de master une nouvelle approche à base de SMT (Satisfiability Modulo Theories) pour vérifier la diagnosticabilité en temps borné sur les automates temporisés. Afin d’améliorer l’efficacité de notre méthode (le problème est PSPACE-complet), nous en proposons à présent une extension incrémentale fondée sur l’utilisation de sur- et sous-approximations paramétrées dans une généralisation de la méthode CEGAR (raffinement d’abstraction guidé par un contre-exemple). Nous montrons l’amélioration apportée au travers de résultats expérimentaux. Néanmoins, la diagnosticabilité est une propriété assez forte, qui nécessite généralement un nombre élevé de capteurs. Par conséquent, il n’est pas rare que le développement d’un système diagnosticable soit trop coûteux. Afin de garantir dès la conception un certain niveau de sûreté de fonctionnement de manière économique et efficace, nous proposons deux approches. La première consiste à concevoir des systèmes à événements discrets diagnosticables en utilisant des blocs de retard. En effet, que se passe-t-il si un système se révèle comme non diagnosticable ? Une manière classique est d’ajouter des capteurs. Nous proposons une nouvelle manière non intrusive de rendre diagnosticable un système non diagnosticable en ajoutant simplement des blocs de retard sur certains événements observables, reportant ainsi leurs observations. Notre approche est codée dans une formule SMT, dont l’exactitude et l’efficacité sont démontrées par nos résultats expérimentaux. La seconde consiste à analyser une nouvelle propriété du système appelée manifestabilité, qui est une exigence plus faible sur les observations du système pour avoir une chance d’identifier l’occurrence des défauts en ligne et peut être vérifiée au stade de la conception. Intuitivement, cette propriété garantit qu’un système défectueux ne peut pas toujours apparaître sain, c’est-à-dire qu’il a au moins un comportement futur après l’apparition d’un défaut qui se distingue par l’observation de tous les comportements normaux. Nous définissons d’abord la manifestabilité des automates à états finis pour les systèmes à événements discrets et proposons un algorithme de complexité PSPACE pour la vérifier automatiquement et prouvons que le problème de vérification de la manifestabilité lui-même est PSPACE- complet. Les résultats expérimentaux montrent la faisabilité de notre algorithme d’un point de vue pratique. Ensuite, nous définissons la manifestabilité des systèmes temps-réel modélisés par des automates temporisés en tenant compte des contraintes de temps, et étendons notre approche pour vérifier la manifestabilité de ces systèmes, prouvant qu’elle est indécidable en général mais, sous certaines conditions restreintes, devient PSPACE- complet. Enfin, nous encodons cette propriété dans une formule SMT, dont la satisfaisabilité témoigne de la manifestabilité, avant de présenter des résultats expérimentaux montrant le passage à l’échelle de notre approche
Fault diagnosis is a crucial and chal- lenging task in the automatic control of complex systems, whose efficiency depends on a system property called diagnosability. Diagnosability describes the system property allowing one to determine at design stage whether a given fault occurring online will be identifiable with certainty based on the available observations, which is an alternative to testing that can only show the presence of failures without guaranteeing their absence. The diagnosability problem of discrete event systems has received considerable attention in the literature, but little work takes into account explicit time constraints during this analysis. However such constraints are naturally present in real-life systems and cannot be neglected considering their impact on this property. We proposed in our master work a new SMT (Satisfiability Modulo Theories)- based approach to verify bounded time diagnosability on timed automata. The idea is to encode in SMT the necessary and sufficient condition for diagnosability. In order to improve the efficiency of our method (the problem is PSPACE- complete), we propose now an incremental extension of it based on the use of parameterized over- and under-approximations generalizing the CEGAR (CounterExample-Guided Abstraction Refinement) method. We show the improvement provided through experimental results. Nevertheless, diagnosability is a quite strong property, which generally requires a high number of sensors. Consequently, it is not rare that developing a diagnosable system is too expensive. In order to guarantee from design an adequate level of safety in an economical and efficient way, we propose two approaches. The first one consists in designing diagnosable discrete event systems by using delay blocks. Indeed, what if a system is revealed as non- diagnosable? One classical way is to add sensors. We propose a new non-intrusive way to make diagnosable a non-diagnosable system by merely adding delay blocks on some observable events, thus deferring their observations. As far as we know, this is the first attempt to remove non- diagnosability with delay blocks without using controllable events or changing the structure of systems. Our approach is encoded into an SMT for- mula, whose correctness and efficiency are demonstrated by our experimental results. The second one consists in analyzing a new system property called manifestability, that is a weaker requirement on system observations for having a chance to identify online fault occurrence and can be verified at design stage. Intuitively, this property makes sure that a faulty system can- not always appear healthy, i.e., has at least one future behavior after fault occurrence observably distinguishable from all normal behaviors. We first define the manifestability of finite state automata for discrete event systems and propose an algo- rithm with PSPACE complexity to automatically verify it and prove that the problem of manifestability verification itself is PSPACE-complete. The experimental results show the feasibility of our algorithm from a practical point of view. Then we define the manifestability of real-time systems modeled by timed automata by taking into account time constraints, and extend our approach to verify manifestability for these systems, proving that it is undecidable in general but, under some restricted conditions, becomes PSPACE-complete. Finally we encode this property into an SMT for- mula, whose satisfiability witnesses manifestability, before presenting experimental results showing the scalability of our approach

L'argument anti-réaliste propose par Michael Dummett doit nous permettre de conclure que nous sommes incapables de manifester une connaissance des conditions de vérité des phrases pour lequelles nous ne possédons pas, au moment présent, de procédure de décision. Cette conclusion est d'abord rejetée dans le cas de la formule indécidable de Gödel. Deux types de manifestation sont ensuite envisages pour les phrases indécidées de facto : par l'énonciation et par la décision. La manifestation du premier type est rejetée pour cause évidente de circularité et de régression. Ce rejet conduit à des conclusions moins évidentes qu'il n'y parait sur les conditions générales de la manifestabilité et la pertinence du critère de décidabilité. L'analyse de la manifestation par la décision montre que, soit l'argument dummettien est une réduction à l'absurde de la défense du principe de vériconditionnalité, soit le partisan du principe peut défendre le réalisme en attribuant aux usagers compétents la capacité à rechercher des procédures de décision sans pour autant risquer l'accusation de transcendance par rapport à la manifestabilité. Une modification substantielle de la conception du débat est ensuite proposée : si la question du réalisme se pose, elle ne peut manquer de se poser également pour les phrases décidables de facto relativement à des exigences non sceptiques. Finalement, puisque le choix des conditions de justifiabilité comme concept central de la théorie de la signification est incompatible avec le rejet radical du holisme propose par Dummett, le défi de manifestabilité est retourné contre l'anti-réaliste
Michael Dummett's anti-realist argument urges us to conclude that we cannot manifest a knowledge of the truth-conditions of sentences for which no decision procedure is at present available. I begin with a rejection of that conclusion in the case of godel's undecidable formula. Two types of manifestation are then considered for de facto undecided sentences : by stating and by effectively deciding. The first type is rejected on grounds of circularity and regression. This rejection leads to conclusions concerning the general conditions of manifestability and the relevance of the criterion of decidability. The analysis of manifestation by means of decision shows that, either Dummett's argument is a reductio ad absurdum of the defense of the truth-conditional principle, or the advocate of the principle may vindicate realism by ascribing to speakers a capacity to look for decision procedures. Since this may be done by avoiding the transcendance objection, the realist meets the manifestation requirement. A substantial modification of the conception of the debate is then proposed : the realism vs. Anti-realism debate also covers the case of sentences that are decidable relative to unskeptical standards. Finally, since the choice in favour of justifiability conditions as the central concept of the theory of meaning is incompatible with dummett's wholesale rejection of holism, the manifestation challenge is turned against the anti-realist

Anti-realists about the past claim that no one has yet manifested a knowledge of the truth of tensed instances of the realist schema '‡ (s is true · there is no evidence for s),' instances such as '‡ ('Caesar crossed the Rubicon' is true · there is no evidence for 'Caesar crossed the Rubicon'). It is true that we cannot decide specific instances of the realist schema and that, consequently, neither our understanding of these instances, nor our knowledge of their truth may be constituted by the recognitional and executive capacities which, according to Michael Dummett's antirealism, constitute grasp of meaning. Although we cannot decide these issues, we can meet Dummett's anti-realist's manifestability challenge by arguing for them from contingency. While no recognitional and decisional skills may constitute our knowledge that their truth-conditions are satisfied, we can, without begging the question, derive that knowledge from our folk and scientific theories of the workings of nature. The evidence we have in favor of the fact that evidential relations between us and past facts are naturally contingent allows us to infer tensed instances of the fundamental realist modal claim. The joint possibility of truth and undecideability pro tempora is a natural possibility and, thereby, a logical and metaphysical possibility.