en fr Synthesis for a Weak Real-Time Logic Synthèse pour une Logique Temps-Réel Faible Report as inadecuate




en fr Synthesis for a Weak Real-Time Logic Synthèse pour une Logique Temps-Réel Faible - Download this document for free, or read online. Document in PDF available to download.

1 LaBRI - Laboratoire Bordelais de Recherche en Informatique

Abstract : In this dissertation, we consider the specification and the controller synthesis problem for real-time systems. Our models for systems are kinds of Event-recording automata. We assume that controllers observe all the events occurring in the system and can prevent occurrences of controllable events. We study Event-recording Logic ERL. We propose new algorithms for the model-checking and the satisfiability problems of that logic. Our algorithms are similar to some algorithms proposed for the same problems in the setting of the standard $\mu$-calculus. They also correct earlier proposed algorithms. We define disjunctive normal form formulas and we show that every formula is equivalent to a formula in disjunctive normal form. Unfortunately, ERL is rather weak and can not describe some interesting real-time properties, in particular some important properties for controllers. We define a new logic that we call WTmu. The logic WTmu is a weak real-time extension of the standard $\mu$-calculus. We present an algorithm for the model-checking problem of WTmu. We consider a fragment of WTmu called WT\mu for control C-WTmu. We show that the satisfiability of C-WTmu is decidable. The algorithm that we propose for deciding whether a formula of C-WTmu, has a model does not need to know the maximal constant used in models and it enables the construction of a witness model. Using C-WTmu, we present algorithms for a centralised controller synthesis problem and a centralised $\Delta$-controller synthesis problems. The construction of witness controllers is effective.

Résumé : Dans cette thèse, nous nous intéressons à la spécification et à la synthèse de contrôleurs des systèmes temps-réels. Les modèles pour ces systèmes sont des Event-recording Automata. Nous supposons que les contrôleurs observent tous les évènements se produisant dans le système et qu-ils peuvent interdirent uniquement des évènements contrôlables. Tous les évènements ne sont pas nécessairement contrôlables. Une première étude est faite sur la logique Event-recording Logic ERL. Nous proposons des nouveaux algorithmes pour les problèmes de vérification et de satisfaisabilité. Ces algorithmes présentent les similitudes entre les problèmes de décision cités ci-dessus et les problèmes de décision similaires étudiés dans le cadre du $\mu$-calcul. Nos algorithmes corrigent aussi des algorithmes présents dans la litérature. Les similitudes relevées nous permettent de prouver l-équivalence entre les formules de ERL et les formules de ERL en forme normale disjonctive. La logique ERL n-étant pas suffisamment expressive pour décrire certaines propriétés des systèmes, en particulier des propriétés des contrôleurs, nous introduisons une nouvelle logique WTmu. La logique WTmu est une extension temps-réel faible du $\mu$-calcul. Nous proposons des algorithmes pour la vérification des systèmes lorsque les propriétés sont écrites en WTmu. Nous identifions un fragment de WTmu appelé WTmu pour le contrôle C-WTmu. Nous proposons un algorithme qui permet de vérifier si une formule de C-WTmu possède un modèle. Cet algorithme n-a pas besoin de connaître les ressources horloges et constante maximale comparée avec les horloges des modèles. En utilisant C-WTmu comme langage de spécification des systèmes, nous proposons des algorithmes de décision pour le contrôle centralisé et le $\Delta$-contrôle centralisé. Ces algorithmes permettent aussi de construire des modèles de contrôleurs.

en fr

Keywords : Real-time systems formal methods real-time logic $\mu$-calculus satisfiability model-checking controller synthesis.

Mots-clés : synthèse de contrôleurs Systèmes temps-réel Event-Recording automata logique temps-réel satisfaisabilité Event-Recording Logic méthodes formelles vérification synthèse de contrôleurs.





Author: Omer Landry Nguena Timo -

Source: https://hal.archives-ouvertes.fr/



DOWNLOAD PDF




Related documents