Synthesis for a weak real-time logic

Synthèse pour une logique temps-réel faible 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é ci-dessus et les problèmes de décision similaires étudiés dans le cadre du µ-calcul. Nos algorithmes corrigent aussi des algorithmes présents dans la litté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 WTµ. La logique WTµ est une extension temps-réel faible du µ-calcul. Nous proposons des algorithmes pour la vérification des systèmes lorsque les propriétés sont écrites en WTµ. Nous identifions deux fragments de WTµ appelés WTµ bien guardé (WG-WTµ) et WTµ pour le contrôle (C-WTµ). La logique WG-WTµ est plus expressif que C-WTµ. Nous proposons un algorithme qui permet de vérifier si une formule de WG-WTµ possède un modèle (éventuellement déterministe). Cet algorithme nécessite de connaître les ressources (horloges et constante maximale comparée avec les horloges) des modèles. Dans le cadre de C-WTµ l'algorithme que nous proposons et qui permet de décider si une formule possède un modèle n'a pas besoin de connaître les ressources des modèles. En utilisant C-WTµ comme langage de spécification des systèmes, nous proposons des algorithmes de décision pour le contrôle centralisé et le ∆-contrôle centralisé. Ces algorithmes permettent aussi de construire des modèles de contrôleurs. Lorsque les objectifs de contrôle sont décrits à l'aide des formules de WG-WTµ, nous montrons également comment synthétiser des contrôleurs décentralisés avec des ressources fixées à l'avance et ceci, lorsqu'au plus un contrôleur est non déterministe.