PROCEDE ET DISPOSITIF PERMETTANT DE GENERER UN SYSTEME DE CONTROLE A PARTIR DE COMPORTEMENTS REDOUTES

SPECIFIES

L'invention concerne un procédé et un dispositif permettant, à partir de la spécification en un langage formel d'un comportement redouté, de générer automatiquement un agent observateur ou détecteur de comportement redouté, appelé moniteur, capable, en ligne, pendant une durée arbitraire et sans perte de performance, de signaler toute occurrence dudit comportement redouté spécifié lors du fonctionnement d'un système susceptible de produire ce comportement. Elle permet la génération automatique de détecteurs de comportements spécifiés en logique temporelle linéaire métrique, ayant une mémoire bornée, capable de fonctionner en ligne et pendant un temps arbitrairement long.

Elle est notamment utilisée pour le contrôle et la surveillance de systèmes simulés ou encore de systèmes physiques. Elle permet aussi d'effectuer des diagnostiques en ligne de systèmes de contrôle-commande, des surveillances d'environnements en domotique ou robotique. Elle est aussi mise en oeuvre pour la preuve de propriétés sur des exécutions/simulation finies.

Différentes industries sont concernées par l'invention, comme : les industriels du transport, des télécoms, des services Internet, de la robotique ou encore de la domotique.

Dans l'art antérieur if existe principalement deux approches de gestion formel « monitoring formel » connues du Demandeur.

Une première approche est due à Presanna Thatï et Grigore Rosu Cette approche est décrite dans l'article intitulé « Monitoring Algorithme For Metric Temporaî Logic Spécifications » décrit dans le document « electronic notes in theorical computer » march 2004. Cette approche propose de générer un moniteur pouvant fonctionner en ligne, à partir d'une logique métrique linéaire. Le procédé de Thati et Rosu est basé sur la réécriture et l'évaluation dynamique de formules et engendre de fait plusieurs limitations. Le principe de cette approche consiste à exploiter l ^' expression même du problème du monitoring à savoir « est-ce qu ^' un comportement observé satisfait Φ » où Φ est une formule qui spécifie un comportement redouté. Problème que l ^' on peut noter plus brièvement :

C \= <\> ?

(Lire : est-ce que le comportement observé C valide Φ ?)

Avant d'avoir observé le système, le problème se pose donc comme suit :

0\= Φ ? où ø dénote le comportement vide Le procédé de Thati et Rosu fonctionne ainsi : il maintient l ^' expression du problème de la satisfaction à mesure que les observations arrivent, en tenant compte de celles-ci. Si, à un certain stade, le problème du monitoring s'exprime sous la forme « C |= Φ _η ? » et qu ^' une nouvelle observation o est disponible, il calcule Φ _η+1 , une nouvelle formule, telle que l ^' on ait :

C | = Φ -, C.o |= Φ _η+ ι

où C.o est le comportement défini comme le comportement C suivi de l ^' observation o.

Par transitivité :

0 \= Φ ... ,- C \ = Φ _η <:-> C. O \ = Φ _η . ι

Le principe consiste donc à réécrire l ^' expression du comportement redouté en fonction des événements déjà observés du système, tout en maintenant la problématique initiale, à savoir « 0 |= Φ ? », Ce que les auteurs « appellent résoudre le passé et dériver le futur ». Pour prendre un exemple intuitif de la vie courante, la validité de l'assertion « il fera beau dans 8 jours » prononcée aujourd ^' hui, est la même que celle, le lendemain, de l'assertion « il fera beau dans 7 jours » et encore la même que celle, 8 jours plus tard, de l'assertion « il fait beau aujourd'hui » (qui pourra être décidée par observation directe).

Pour ne pas stocker la trace d'exécution (afin que le moniteur garde une mémoire bornée), il est nécessaire de maintenir en permanence une table de vérité de toutes les formules qui peuvent potentiellement apparaître lors du procédé de réécriture. De la sorte, il est possible de calculer la valeur de vérité de la formule principale en utilisant les valeurs contenues dans la table. Mais, pour que le moniteur ait une mémoire bornée, il faut que cette table soit finie et par conséquent que l'ensemble des sous-formules pouvant apparaître soit lui-même fini. Or ceci n'est possible que si les pas d'exécution permis sont en nombre finis et connus à l'avance. Ainsi ce procédé présente notamment les inconvénients suivants :

• La logique de spécification ne supporte que des intervalles dont les bornes sont des entiers naturels,

· Les pas d'exécution permis pour le système doivent être en nombre finis et connus à l'avance. Dans l'article précité, les pas d'exécution permis sont des entiers naturels (ainsi que l'indiquent les définitions de Γ(Φ) et F (Φ)),

• Enfin, l'algorithme est très consommateur de temps puisque la complexité estimée est de l'ordre de m ³ 2 ^3m où m est le nombre total de sous-formules obtenues à partir de la formule principale (l'ordre de grandeur de m par rapport à la formule principale n'étant quant à lui pas donné dans l'article).

Une deuxième approche connue du Demandeur est décrite dans le document intitulé « Monitoring Temporal Properties of Continuous Signais » de Oded Mater et Dejan Nickovic. Le moniteyr d'Oded Maler et Dejan Nickovic se base sur te calcul des intervalles de validité d'une formule. Pour une formule donnée, et un comportement donné, le procédé de Maler et Nickovic calcule un ensemble d ^' intervalles de temps qui dénotent les dates où la formule est vraie et en dehors desquels la formule est fausse. Le calcul est fait d ^' abord pour les formules de base (propositions) puis pour les formules plus complexes. Pour cela, les auteurs définissent une correspondance entre les opérateurs de la logique de spécification et les opérations classiques sur les ensembles d'intervalles (intersection, union ...). Par exemple, en connaissant les intervalles de validité de deux formules Φ1 et Φ ₂ il est possible de déduire qu'un intervalle / est dans l ^' ensemble des intervalles de validité de la formule Φι Λ Φ ₂ si et seulement s ^' il existe un intervalle j de Φι et un intervalle k de ₂ tels que i = j n k. Cette technique permet le calcul des intervalles pour une logique temporelle qui supporte des intervalles dont les bornes ne sont plus limitées aux entiers et l ^' analyse d'exécutions dont le pas est libre. Outre le fait qu'il n ^' existe pas d ^' opérateurs sur le passé dans la logique présentée, l ^' approche souffre d'un défaut essentiel, indiqué par les auteurs. Le moniteur d'Oded Maier et Dejan Nickovic travaille hors ligne, sur une exécution enregistrée. Ceci représente une limitation importante car, sur un temps d'exécution long, le stockage de l ^' exécution peut ne pas être praticable (système autonome, embarqué ...). Ceci limite donc les temps de surveillance et de fait aussi les applications. Dans la plupart des documents de l ^' art antérieur, lorsqu'il existe un objectif de synthèse de contrôleur, c'est la synthèse d ^' automates qui est choisie. Pour exemple, il est possible de citer les documents suivants: S.FIake, W.Mueller : « Past and future oriented time-bounded temporal properties with OCL », Proceedings of the second international conférence on software engineering and formai methods. XP010733319, ou S.J.Konrad "Model- driven development and analysis of high assurance Systems, volume 1 , Michigan State University, XP 055001797 La Demande de brevet WO2010/026150 du Demandeur décrit un procédé et un système permettant de générer un dispositif de contrôle à partir de comportements redoutés spécifiés. Malgré tous les avantages qu'elle présente, l'invention décrite dans ce document repose sur un langage souffrant plusieurs limites :

o ses expressions de bases sont limitées à des variables booléennes, o il ne permet pas de référer aux instants singuliers où une formule change de valeur de vérité (interdisant par exemple l'expression de propriétés portant sur la durée),

o il ne permet pas de translater dans le temps la valeur d'une expression,

o il ne permet pas de compter les événements,

o il ne permet pas de spécifier des équations complexes.

L'objet de la présente invention concerne un procédé permettant, à partir de la spécification d ^' un comportement redouté en un langage de logique temporisèe, de générer automatiquement un détecteur à mémoire borné adapté à signaler par la génération d'un signal représentatif toute occurrence dudit comportement redouté d'un système en fonctionnement, ledit système étant équipé de capteurs adaptés à déterminer la valeur de paramètres donnés, ledit système étant relié audit détecteur muni d'un processeur et d'une mémoire, ledit procédé étant caractérisé en ce qu'il comporte au moins les étapes préalables suivantes :

• définir des variables caractéristiques du système à surveiller {xi, ... x _m }, et/ou des propositions { i, p _n } sur ces variables,

· allouer en mémoire du détecteur un espace suffisant pour mémoriser un instantané relatif à ces propositions et à ces variables de signaux c ^' est-à-dire allouer pour le temps une variable réelle notée l.t, pour chaque proposition p une variable l.p et pour chaque variable de signal x une variable l.x,

* définir une formule principale , construite sur les propositions {pi, p _n ) et les variables {x _t . ... x _m > traduisant un comportement redouté ou une propriété du système en utilisant un tangage composé d'opérateurs logiques et d ^' opérateurs temporels portant sur îe futur et le passé et dont les termes τ et les formules Φ sont donnés par les grammaires BNF suivantes :

Γ ::= c | x | (r,. ..,r) | f(r) Τ := Γ | Γ, ... , τ ) | V _[a | _ί Φ ΐ Τορ | Bot " ! X _W Γ | f( ^T )

i : := Ο(Γ) 1 (E )

Φ ::= Ë

i or ) i v _[al

I X[n] É

1 Φ u _i+ Φ i Φ s + Φ

I Φ S( _d ,k) Φ

I Τορ Φ I Bot Φ

Ι (φ)

où f est un symbole de fonction, O un symbole de prédicat, a est un réel non nul, d un réel positif ou nul, n un entier relatif non nul, i+ tout intervalle dont les bornes sont positives ou nulles, i un intervalle standard quelconque ou un intervalle infini seulement à gauche, et dont la sémantique est la suivante :

• si c est une constante alors le terme c, dans le langage, dénote la fonction constante c(t) qui vaut toujours c,

• si x est un signal alors à la date t le terme x (dans le langage) vaut l.x où I est le plus proche instantané situé avant t, on notera x(t) cette valeur.

• à la date t un n-uplet de termes (σι, ..., σ _η ) vaut (oi(t), o _n (t)) où a _k (t) dénote la valeur du terme σ _κ en t,

• à la date t le terme f(o) vaut f(o(t)),

• l ^' opérateur V _[a] est un opérateur de translation temporelle ;

Ν [ ₃ ] Φ vaut en t ce que vaut Φ en t+a, le terme Ν,Φ vaut l'entier n à la date t si n est le nombre d ^' intervalles de validité de Φ qui ont une intersection non vide avec i©t,

• X _[n] est un opérateur de décalage , Le terme X[ _N] σ vaut en t ce que vaut le terme σ selon l'instantané Ι _; ¾+ _η ; où l _k est Se plus proche instantané situé ayant t, • l'opérateur Top est appelé opérateur de front montant. Top Φ vaut la valeur v en t si Φ passe de la valeur u à v (u≠ v) en t,

• l ^' opérateur Bot est appelé opérateur de front descendant, Bot Φ vaut u à la date t si Φ passe de la valeur u à la valeur v (u≠ v) en t, · Ο(σ) est en vraie en t si o(t) e O.set.

• l'opérateur Ui+ porte aussi sur le futur, la formule Φι υ,+ Φ ₂ est vraie en t si et seulement s'il existe une date t' de (i+)©t où Φ ₂ est vraie et que Φ ₁ est partout vraie dans l ^' intervalle [t. t'[,

• l ^' opérateur S, ₊ porte aussi sur le passé, la formule Φι Sj ₊ Φ ₂ est vraie en t si et seulement s'il existe une date t' de (rev(i+))®t où Φ ₂ est vraie et que Φ ₁ est partout vraie dans l ^' intervalle ]t\ t],

• l'opérateur Sj _d . _k ) porte aussi sur le passé, Φιβ^.κιΦ^ signifie : « Φ? sera vraie vers le passé au-delà de -d et Φ ₁ sera partout vraie entre temps ». Φ1 S, _d , _k) Φj- est vraie en t s ^' il existe une date t ^' au delà de t- d (t-d comprise si k = 1 et t-d non comprise si k = 0) dans le passé où Φ ₂ est vraie et que Φι est partout vraie sur ]t',t].

Une étape d ^' émission d'un signal Se sur au moins une des sorties dudit processeur lorsque le détecteur de comportement redouté détecte un comportement redouté ou lorsque la propriété du système spécifiée en logique temporelle linéaire métrique est observé.

D ^' autres caractéristiques et avantages du dispositif selon l ^' invention apparaîtront mieux à la lecture de la description qui suit d'un exemple de réalisation donné à titre ilitistratif et ntiilement limitatif annexé des figures qui représentent 1

• La figure 1A, un synoptique du procédé selon l ^' invention et la figure 1 B un exemple d'architecture du système permettant sa mise en œuvre,

• La figure 2, une représentation de la notion de processus, • La figure 3, un algorithme de calcul de la liste de validité d'une proposition ou d'une formule dite purement booléenne,

• Les figures 4A et 4B. représentent la sémantique pour certains opérateurs utilisés dans le procédé selon l'invention,

• Les figures 5A, 5B, 5C, 5D illustrent le calcul de la liste de validité d'une formule en fonction de celles de ses sous-formules,

• La figure 5E, illustre un calcul de listes de validité associé à un l'opérateur Top{@}, permettant de parler du nombre d'instants où une formule passe de faux à vrai,

• La figure 5F, illustre un calcul de listes de validité associé à l ^' opérateur X[n] et 5G à l'opérateur étendu X{f}[ _n ,m],

• La figure 6 illustre l'intervalle de définition pour l ^' opérateur N, du langage,

• La figure 7, illustration de la définition d'une zone d ^' influence prise en compte pour la mise en œuvre du procédé selon l'invention,

• La figure 8, illustration de l'inutilité des sous-formules directes d'une formule étant donnée la date d ^' inutilité fixée pour celle-ci,

• Les figures 9A et 9B illustrent un cas d'étude pour la surveillance d'un signal et de sa conformité à un signal de référence pour le diagnostic embarqué, et

• La figure 9C illustre l ^' interfaçage entre une réalisation du procédé et l ^' environnement d'ingénierie industrielle Simulink de MathWorks connu de l ^' Homme du métier.

L ^' idée de la présente invention consiste notamment à générer automatiquement un moniteur capable d'observer le comportement d'un système dans un environnement donné et plus particulièrement l'évolution d'un processus au sens qui sera défini plus loin la présente description. Au préalable un utilisateur définira notamment des variables caractéristiques du système à surveiller et/ou des propositions sur ces variables comme il sera explicité ci-après. La figure 1A est un synoptique d'un exemple du procédé selon l'invention comprenant un système 1 dont le comportement est à observer, une horloge temporelle H permettant de déterminer la date à laquelle un instantané a été acquis, un processeur 13 qui va traiter les données issues du système à surveiller, par exemple une variable observée à un instant donné et qui va être capable d ^' évaluer la valeur des propositions où cette variable apparaît, de calculer ensuite les listes de validité attachées à ces propositions puis les listes de validité des formules plus complexes jusqu'à la liste de validité de la formule principale spécifiant le comportement redouté. Sur la figure 1 B est représenté un exemple de système comprenant un moniteur ou détecteur de comportement redouté selon l ^' invention qui comporte, le système 1 dont le comportement est surveillé. Le système comprend un ou plusieurs capteurs 10 permettant de déterminer la valeur de chaque paramètre représentatif du comportement surveillé. Par exemple, il est possible d'avoir un capteur de température et de vérifier si une proposition portant sur la température est vraie. Des exemples sont donnés ci-après. Le ou les capteurs de paramètres équipant le système 1 sont reliés à un détecteur 1 1 de comportement redouté à mémoire bornée comprenant une entrée 12 et un processeur 13 qui va traiter les différentes données ainsi qu ^' une mémoire 14 stockant l'instantané courant et les listes de validité de chaque formule. Le dispositif 1 1 comprend aussi une entrée 15 recevant une horloge spécifiant une date associée à un paramètre mesuré. Le processeur 13 va délivrer via une ou plusieurs sorties 16t . 16 _?. 16 _3, un signal Se contenant des données permettant, par exemple :

Soit l'affichage des résultats sur un dispositif d'affichage 17,

• Soit la génération d'un signal à un dispositif de régulation du système,

• Soit la génération d'un Signal d'alarme.

Le signa! obtenu est transmis à un dispositif de génération d'une alarme et/ou à un système de contrôle ou de régulation du système collaborant avec le moniteur généré par le procédé selon l'invention. Le système dont le comportement est surveillé peut être un modèle exécuté en simulation. Ce modèle peut parfaitement être très complexe et/ou de grande taille étant donné que le moniteur généré selon l'invention ne dépend pas de la structure interne de ce modèle. Dans ce cas, le procédé peut être considéré comme une technique de débogage de modèles.

Le système peut aussi être un dispositif ou un système physique dont on souhaite contrôler le comportement en fonctionnement et notamment vérifier son comportement. Le procédé peut alors être considéré comme une sous-partie d'un système plus vaste de contrôle-commande.

Ainsi, le système selon l'invention peut être appliqué comme dispositif permettant de détecter des erreurs dans le fonctionnement d'un système, plus connu sous l'expression « débogueur » de systèmes simulés, ou comme moniteur de systèmes physiques pour en détecter les disfonctionnements ceci dans tout domaine industriel (transport, domotique, robotique).

Un moniteur selon l'invention est constitué notamment de plusieurs éléments qui vont être explicités ci-après. Fondamentalement son fonctionnement consiste à maintenir sur certaines plages temporelles une représentation en fonction du temps de la valeur prise par chaque expression constituant l'expression du ou des comportements redoutés. A cet égard un des éléments entrant dans la génération du moniteur est la notion de liste de validité qui est représentée par exemple dans les figures 5A, 5B, 5C et 5D et 5 E, 5F, 5G.

Avant d'aborder la génération d'un moniteur dans toute sa généralité il est possible de l'illustrer sur un exemple. Supposons que le procédé soit utilisé pour détecter le passage en négatif du solde d'un compte bancaire. Le comportement redouté s'exprimerait ainsi: solde < 0. Cette expression est en fait une variable booléenne qui vaut 0 (faux) ou 1 (vrai). Elle est composée de la variable solde qui est un nombre décimal (à deux chiffres après la virgule), du prédicat < et enfin de la constante 0. En notant ί ^Λ ν pour signifier que solde vaut v sur l'intervalle temporel i nous pouvons représenter la valeur de solde au cours du temps par une LV liste d intervalles et ce au fur et à mesure que se produisent les mouvements de compte :

o date 0, solde = 100. LV = ([0,0] ^A 100)

o date 1 , solde = 50. LV = ([0, 1 [ ^Λ 100, [1 .1 [ ^Λ 50)

o date 2, solde = 50. LV = ([0, 1 [ ^Λ 100, [1 ,2[ ^Λ 50)

o date 3, solde = -20. LV = ([0, 1 [ ^Λ 100, [1 ,3[ ^Λ 50, [3,3] ^Λ -20)

La logique de construction de cette liste est la suivante: tant que l'information sur la valeur de solde n ^' est pas changée elle est conservée. Ainsi la valeur de solde à une date est celle que cette variable avait lors du plus proche mouvement de compte antérieur.

De la même manière pour la constante 0 la liste représentant sa valeur au cours du temps sera représentée par la liste: ([0,3] ^Λ 0)

Et enfin la liste de la variable (solde < 0) sera calculée en « composant » celles de solde et celle de 0 :

([0, 1 [ ^Λ (100<0), [1 .3[ ^Λ (50<0). [3,3] ^Λ (-20<0))

En réduisant les expressions prédicatives à leurs valeurs booléennes nous obtenons la liste finale de l ^' expression (solde < 0), qui caractérise son évolution temporelle : ([0, 1 [ ^Λ 0, [1 ,3[ ^Λ 0, [3,3] ^A 1 ).

On peut voir qu ^' en [3.3] la valeur attachée est 1 ce qui signifie que l ^' expression (solde < 0) est vraie sur l'intervalle [3,3]. Autrement dit le comportement redouté est arrivé en 3. Pour construire un détecteur de passage du solde en deçà de 0, il suffit donc de construire des listes comme décrit ci-dessus pour chaque sous-expression et de tester si ia liste de l ^' expression principale (solde < 0) possède un intervalle de la forme

Le procédé selon ('invention repose sur une généralisation de cette approche. Au préalable, plusieurs définitions sont introduites.

Etats et comportements et variables d un système

Le comportement d'un modèle de système ou d'un système physique est représenté par l'évolution dans le temps d'un certain nombre de variables caractéristiques. Par exemple, le comportement d'un corps en physique des solides est caractérisé par l ^' évolution de ses variables caractéristiques que sont sa position, sa vitesse, son accélération, son moment cinétique, etc. Une assignation des variables caractéristiques d ^' un système décrit un état de ce système. Un comportement est alors une fonction qui à toute date de la vie du système associe un unique état de ce système.

Signaux et Propositions.

A l'égard d ^' un système le terme « proposition » désigne toute expression faisant référence aux variables caractéristiques du système et pouvant être vraie ou fausse. Par exemple « la vitesse du corps k vaut 10 m/s », « la vitesse du corps k est strictement positive », sont des propositions classiques en physique des solides. Mathématiquement, ces propositions seraient notées « v _k = 10 », « v _k > 0 ». Nous voyons que ces expressions peuvent être vraies ou fausses. Par exemple, si la vitesse observée du corps k est de 5m/s, alors la proposition « v _k = 10 » est fausse puisque « 5 = 10 » est fausse.

En prenant la convention que la valeur 1 représente « être vrai » et que 0 représente « être faux » nous pouvons assimiler les propositions à des variables de domaine {0, 1}.

Ainsi il sera considéré que les propositions définies relativement à un système sont elles-mêmes des variables du système. Néanmoins, dans le discours, pour distinguer entre les variables du système et les propositions constituées sur ces variables, on parlera de propositions ou de variables booléennes pour les premières et de signaux pour les secondes.

Notons qu'il n ^' est pas exclu qu'un système possède nativement des propositions.

hTstantané

Lorsqu'on observe un système il n ^' est pas concevable d ^' enregistrer son comportement réei au sens défini plus haut. Le temps théorique étant continu cela supposerait une infinité d'observations. En revanche on peut observer l'état d'un système de façon ponctuelle et répétée, selon un pas fixe ou variable. Aussi, cela peut être le système lui- même qui prenne l'initiative de livrer à un observateur, à son rythme, ses changements d'états. Quel que soit le cas de figure, nous appellerons instantané le résultat d'une observation, soit la donnée :

• de l'état actuel du système observé (c'est-à-dire d'une assignation de ses variables caractéristiques),

• de la date à laquelle cette observation a été faite.

Un instantané donne donc, à une certaine date, la valeur des variables du système observé.

Si I est un instantané et x une variable du système (proposition ou signal) on notera l.x la valeur que I donne à x ; la variable t sera réservée au temps, ainsi on réservera la notation l.t pour dénoter la date indiquée par l'instantané I.

Relativement à un système sys, l _sys dénote l'ensemble des instantanés possibles du système sys.

Rafraîchissement de l'instantané

Dans la mise en œuvre du procédé selon l'invention on considérera une structure allouée en mémoire du calculateur capable de stocker les informations contenues dans un instantané, à savoir la valeur du temps et la valeur des variables. Ces valeurs seront actualisées (réécrites dans la même zone mémoire) à chaque observation du système, phénomène que nous appellerons rafraîchissement de l'instantané. Une seule structure de ce type est nécessaire au procédé car, comme nous le verrons, son fonctionnement ne requiert la mémorisation que d'un seul instantané.

Pour cette structure, seront employées les notations introduites ci- dessus. En outre cette structure sera souvent appelée I, et une variable l.x dénotera la valeur de la variable x selon cette structure dans son état actuel. La variable réelle I. t dénote la valeur du temps enregistrée dans cette structure. Processus.

Dans le contexte de la présente invention le terme processus est utilisé pour désigner toute suite d'instantanés indicée par une section initiale des entiers naturels. Pour rappel une section initiale des entiers naturels est tout sous-ensemble H des entiers naturels vérifiant :

• 0 e H

• pour tout i G H, si i > 0 alors i -1 e H

Mathématiquement un processus π est donc toute application de H dans l _sys telle que :

· H est une section initiale des entiers naturels

• si i et i+1 sont dans H alors 7t(i).t < jr(i+1 ).t (la date portée par un instantané est strictement supérieure à celle de l ^' instantané qui le précède)

La Figure 2 donne une illustration d'un processus. Il est défini sur le segment initial [0,3]·

Soit π un processus sur [0,n] et k e [0, n]. Alors 7t(k) dénote l'instantané de rang k de π.

Soit π un processus de [0,n] dans l'ensemble des instantanés possibles l _sys .

• ji.first dénote π(0),

· n.last dénote π(η).

jt.first.t est donc la date d'origine du processus π.

rr. last.t est donc la dernière date du processus π.

Le domaine temporel d'un processus π est l'intervalle [n.first.t, idast.t].

Prolongement d'un processus selon un instantané.

Soit π un processus de [0,n] dans l _8ys et I un instantané de l _sy8 tel que l.t > n. last.t alors on note π·( le processus π' de [0,n+1 ] dans lsys égal à π sur [0,n] (c'est-à-dire π ^' ί¥) = n(k) pour k e [0,ri]) et tel que ji'(k+1 ) = I.

·ί sera appelé le prolongement de ii selon L Encadrements d'un processus

Soit π un processus de [0,n] dans ! _{s s} . Nous dirons que le processus π' de [0,m] dans l _sys est un encadrement de π si :

• m > n et

* il existe un entier k > 0 tel que jt'(k+i) = π(ί) pour tout i de [0,n]

En somme un encadrement d'un processus π est le processus π auquel on a ajouté des instantanés avant ou après ou les deux à la fois.

Dans la mise en œuvre du procédé un processus n ^' a pas besoin d'être mémorisé en tant que tel. Les définitions introduites ici sur la notion de processus visent donc principalement à être utilisées pour la description de ce procédé. Notons cependant que le processus peut être mémorisé par le procédé lui-même en ce sens que la mesure du temps et le numéro d'un instantané peuvent aussi être considérés comme des variables du système. Cet aspect sera utilisé plus loin pour un opérateur particulier du langage de description des comportements redoutés (l'opérateur X[ _n] ),

Intervalles

Dans la suite il sera question d'intervalles dans l'ensemble des nombres réels noté 91, Pour noter un intervalle deux notations seront utilisées :

Â1 .la notation usuelle telle:] 4,32, 6.21 ]

A2. la notation sous forme de quadruplet (I, Ib, ub, u) où:

A2.1 . Ib : borne inférieure

A2.2. ub i borne supérieure

A2 3. I et u sont éléments de {0,1}. Ils dénotent l'ouverture ou la fermeture de l'intervalle sur les bornes Ib et ub. Si î vaut 0 l'intervalle est ouvert sur sa borne inférieure Ib, fermé si I vaut 1. Idem pour u qui spécifie l ^' ouverture/fermeture sur la borné supérieure ub.

Exemple i le quadruplet (0, 4.32, 6.21 , 1 ) représente le môme intervalle que celui noté ]4.32, 6.21 ] .

Si i est un intervalle alors i.l, i.lb, i.ub et i.u dénotent les paramètres ci-dessus mentionnés. Donc, par exemple, si i est ] 4.32, 6.21 ] alors i • i.lb est 4.32

• i.ub est 6.21

• i.u est 1

• i.l est 0

Pour qu'un intervalle i soit bien formé il faut soit que i.lb < i.ub soit que cet intervalle soit de la forme [x,x] où x est un réel. Quand un intervalle n'est pas bien formé il est considéré comme égal à l'intervalle vide (on dira aussi « Nil »).

Soit i un intervalle, on notera rev(i) l'intervalle (i.u, - i.ub, - i.lb, i.l). L'intervalle rev(i) peut être vu comme le symétrique de i par rapport à la date 0.

Comme les paramètres de fermeture d'intervalle sont des variables de {0,1} on pourra indifféremment les combiner selon les opérateurs arithmétiques usuels ou selon les opérateurs booléens usuels. Les principales équivalences sont données ci-dessous :

· -i U = (1 - U)

• U Λ V = U X V

• U V V = u + v - (u x v)

• u => v = -iU v v = ((1 - u) + v) - ((1 - u) x v)

Soient i et j deux intervalles on notera j J i l'intervalle suivant :

(i.l => j.l, j.lb - i.lb, j.ub - i.ub, i.u => j.u)

Exemple :

[5,8[ J ]3,4] = (0=>1 , 5-3. 8-4, 1=>0) = (1 ,2,4,0) = [2,4[

Si i et j sont deux intervalles, î est strictement inférieur à j et noté i < j si :

• leur intersection est vide ( i n j = 0 ) et

· i.ub < j.lb.

Si i est un intervalle alors :

• L'intervalle noté i] , appelé fermé à droite de î, est (i.l, i.lb, i.ub, 1 ) ou bien encore, de façon équivalente est i u [i.ub, i.ub].

• L'intervalle noté p, appelé fermé à gauche de î, est (1 , i.lb, i.ub, i.u) ou bien encore, de façon équivalente est [i.lb, i.lb] u i. * L'intervalle noté i[ , appelé ouvert à droite de i, est (i.l, i.lb, i.ub, 0)

* L'intervalle noté ]i, appelé ouvert à gauche de i, est (0, i.lb, i.ub, Lu) Si i et j sont deux intervalles on dira que :

* i chevauche j à gauche si i n j ≠ 0 _» (i n j).lb = j.lb et (s n j).l = j.l (autrement dit i couvre j et le dépasse éventuellement dans le passé).

Exemple [0.4[ chevauche [2,5] à gauche car [0,4[ n [2,5] = [2,4[≠ 0 et [2,4[.lb = [2.5].lb = 2. Le chevauchement est stricte s ^' il existe une date t de i telle que. quelle que soit la date t' de j, alors t < t ^' (i dépasse j dans le passé)

· i chevauche j à droite si i j ≠ 0, i n j.ub = j.ub et i n j.u = j.u (autrement dit i couvre j et le dépasse éventuellement dans le futur). Le chevauchement est stricte s'il existe une date t de i telle que, quelle que soit la date t' de j, alors t ^' < t.

* i jouxte j à gauche si i.ub = j.lb et i.u + j.l = 1. Exemples : [0, 1 [ jouxte

[1 ,2] à gauche ; [0,3] jouxte ]3,8] à gauche.

* i jouxte j à droite si j jouxte i à gauche. Exemple :]8,9] jouxte [4,8] à droite car [4,8] jouxte ]8,9] à gauche.

Soit (a.b) un couple de réels et i un intervalle. Alors i Φ (a, fa) dénote l'intervalle (i.l, i.lb + a. i.ub + b, i.u).

Par abus de notation on notera i Φ t, où t est un scalaire, comme abréviation de : i Φ (t,t)

Exemples :

* [5,8[ Φ (1 _ί 2) = [6,10[

* [5,8[ φ (-3,-2) = [2,6[

· [5,S[ § 3 = ί5,8[ Φ (3,3) - 18,11[

Différencie! d'intervaties

Soient i et j deux intervalles tels que :

i.l = j.l

i.lb = j.lb

j.ub > i.ub alors la notation j\i dénote (1 - i.u, i.ub _» j.ub, j.u)

Exemples :

[0,4[ \ [0,4[ = (1 - 0,4.4,0)= [4,4[ = 0

[0.4] [0,4[ = (1 - 0,4,4, 1 )= [4,4]

[0.5] \ [0,4[ = (1 - 0,4,5.1 ) = [4,5]

Intervalle à compteur

Un intervalle peut éventuellement être muni d'un compteur. Il s ^' agit d ^' un attribut de type entier positif ou nul attaché à un intervalle. Nous noterons ixn pour dénoter que la valeur du compteur de i vaut n.

Intervalle valué

Un intervalle peut éventuellement être muni d ^' une valeur appartenant à un type de donnée propre au système. Par exemple cette valeur peut être d'une nature quelconque, un nombre réel, un n-uplet de réels ou d'éléments d'un autre type. Nous utiliserons la notation i ^A y pour indiquer que l ^' intervalle i porte la valeur y. Exemple : ]6.3,8.2] ^Λ (2.3, 4.45) est un intervalle dont la valeur est le couple (2.3, 4.45).

Intervalles non standards

Un intervalle non standard est un intervalle dont la borne supérieure est la valeur symbolique °° ou dont la borne inférieure est la valeur symbolique -∞ (ou les deux). Rappelons que∞ est tel que x <∞ quel que soit x un entier ou un réel et que -∞ est tel que y > -« quel que soit y un entier ou un réel. Comme ces valeurs ne peuvent être comprises, l ^' intervalle sera forcément ouvert sur de telles bornes. On dira que l ^' intervalle i est infini à gauche (resp. à droite) si borne inférieure (resp. supérieure) est -« (resp. ∞).

Liste de validité

Une liste de validité possède un domaine de définition qui est un intervalle. C'est par ailleurs une liste dont les éléments sont des intervalles bien formés de l'ensemble des réels tous disjoints, rangés dans l'ordre croissant {chronologique). La notation (h, i ₂ , . , y sera utilisée pour désigner une liste de validité contenant les intervalles h, , ... i _n . L'ordre chronologique signifie que si i _k et i _k+ i sont deux intervalles consécutifs d ^' une liste de validité nous avons toujours i _k < k+i.

Par exemple : ([1 , 2.43 [, [3.27. 5.04] ) est une liste de validité qui contient deux intervalles, [1 , 2.43[ et [3.27, 5.04], Ils sont bien rangés dans l ^' ordre croissant ou chronologique.

Pour mettre en évidence le premier ou le dernier élément d'une liste de validité on utilise les notations :

• (i | L) pour dénoter une liste dont le premier élément est i. L est aussi une liste de validité (celle des éléments qui suivent i dans (i | L)). L peut éventuellement être vide.

• (L I i) pour dénoter une liste dont le dernier élément est i. L est aussi une liste de validité (celle des éléments qui précèdent i dans (L | i)). L peut éventuellement être vide.

II sera exposé par la suite qu ^' une liste de validité est par destination attachée à une expression et permet de définir, sur une plage temporelle donnée, les dates où cette expression est vraie et les dates où elle est fausse, en se conformant à la convention suivante : les dates qui sont à l ^' intérieur des intervalles de la liste de validité sont les dates où l'expression est vraie ; en dehors de ces intervalles l ^' expression est fausse. Elle peut aussi être attachée à des expressions non booléennes pour caractériser leur évolution temporelle comme dans l'exemple introductif du suivi d ^' un solde bancaire.

Interstices d'une liste de validité

Dans une liste de validité on appelle interstice tout intervalle contenant toutes les dates situées entre deux intervalles consécutifs ou situées entre le premier intervalle et la borne inférieure du domaine temporel de la liste de validité ou situées entre le dernier intervalle et la borne supérieure du domaine temporel de la liste de validité. Formellement un interstice dans une liste de validité L de domaine D est donc soit i

• (1 - îiç. u, ik.ub, ! _¾ k+i ₎ .lb, 1 - i _(k +i ,,Î) si i et sont deux intervalles consécutifs de L

• (D.l, D.lb, i.lb, 1 - i.l) si i est le premier intervalle de L.

• (1 - j.u, j.ub, D.ub, D.u) si j est le dernier intervalle de L.

Exemple : soit ([1 , 2.43 [, [3.27, 5.04[) une liste de validité de domaine [0,6]. Ses interstices sont [0,1 [, [2.43, 3.27[ et [5.04, 6].

Liste de validité d'intervalles à compteurs

Une liste de validité d'intervalles à compteurs est une liste de validité au sens défini précédemment telle que :

• Tous ses intervalles sont munis d'un compteur (resp. d'une valeur)

• Elle ne possède aucun interstice.

Exemple ;

La liste ([0,1 [xO, [1 ,2[x3, [2,4[x0, [4,5[x2, [5,6] xO) de domaine [0,6] est une liste de validité d'intervalles à compteurs.

Adjonction d'un intervalle dans une liste de validité.

Le résultat de cette opération est une liste de validité. Nous distinguons entre adjonction â gauche et adjonction à droite. Néanmoins, pour chacune, si L est une liste de validité vide, l'adjonction dans L d'un intervalle i est la liste (i).

Adjonction à gauche de l'intervalle i à la liste de validité ( j I L) i

• si i est vide alors le résultat est la ( j | L).

• Si i < j alors le résultat est (i | (j j L)). Autrement dit on ajoute i en tête de ( j | L).

• si i jouxte j â gauche, alors le résultat est ((i.l, i.lb, j.ub, j.u) | L).

Autrement dit on étend le premier élément j dans le passé jusqu'à la borne inférieure de i,

• Dans tout autre cas le résultat n'est pas défini.

Adjonction à droite de l'intervalle i à (L | j) :

• si i est vide alors jltat est la liste (L j j).

• si j < i alors le résultat est ((L j j) | i). Autrement dit on ajoute i en fin de (L | j). • si i jouxte j à droite, alors le résultat est (L | (j.l, j.lb, i.ub, Lu)). Autrement dit on étend le dernier élément j dans le futur jusqu'à la borne supérieure de i.

• dans tout autre cas le résultat n ^' est pas défini.

Adjonction avec compteur

Cette opération ne s'applique qu'avec un intervalle à compteur et une liste d'intervalles à compteurs. L ^' adjonction avec compteur de l ^' intervalle ixn à la liste de validité d ^' intervalles à compteurs L répond aux règles suivantes ;

B.1. Si jxm est un intervalle de L inclus dans i son compteur est incrémenté de n. Autrement dit le compteur de j devient (m+n).

B.2. tout intervalle jxm partiellement couvert par i ( j <t i, jni≠ 0) est remplacé dans L par deux intervalles adjacents k et g (kng = 0, k g = j), de sorte que les dates de l'un, disons k soient toutes dans i (k c i) et qu'aucune date de l'autre, disons g, ne soit dans i (gni = 0); le compteur de k est fixé à m+n ; le compteur de g est fixé à m.

Exemples d'adjonction avec compteur i

Soit L = ([0,1 [xO, [1 ,2[x3, [2,4[x0. [4,5[x2, [5∞[x0) une liste de validité de d ^' intervalles à compteurs de domaine [0,∞[.

L'adjonction avec compteur de [0,3[x1 à L donne :

([0, 1 [x1 , [1 ,2[x4, [2,3[x1 , [3,4[x0, [4,5[x2, [5,∞[x0)

L ^' adjonction avec compteur de [3,∞[x2 à L donne :

([0,1 [xO, [1 ,2[x3, [2,3[x0. [3,4[x2, [4.5[x4, [5 _» ∞[x2)

Raccordements de liste? de validité

Raccordement à droite. Soient (Ll | j) et (i | L2) deux listes de validité. Le raccordement de (i ) L2) à droite de (Ll [ j) a pour résultat :

• si j < i alors {(Ll J j) , (i j L ₂ ) ). Autrement fa liste (i 1 12) est placée â la fin de (L1 | j)

• si i jouxte j à droite alors (M. L2) où M est le résultat de l'adjonction à droite de i à (L l j j) * non défini dans les autres cas

Exemple de raccordement à droite. Soit L = ([1 ,2[) et L' = ([2,3[, [8,12[). Le raccordement à droite de L' à L est la liste : ([1 ,3[, [8, 12[). Ce résultat est du au fait que [2,3[ jouxte [1 ,2[ à droite.

Raccordements de listes de validité d ^' intervalles values

Raccordement à droite. Soient (L1 I j ^A y) et (i ^A x | L2) deux listes de validité_d ^' intervalles valués. Le raccordement de (i ^A x ] L2) à droite de (L1 I j ^A y) a pour résultat :

• si i jouxte j à droite et que :

o x = y alors le résultat est la liste (L1 , (j.l, j.lb, i.ub, i.u) ^A x, L2) o x≠ y alors le résultat est (L1 , j, i, L2)

* si i ne jouxte pas j à droite et j < i alors le résultat est (L1 , j, i, L2)

• non défini dans les autres cas

Raccordement à gauche. Le raccordement d'une liste de validité L ^* à gauche d'une liste de validité L est le résultat du raccordement de L à la droite de L'.

Suite à ces définitions il est possible de formaliser le calcul de la liste de validité d'une variable

Algorithme de calcul de la liste de validité d'une variable

Soit x une variable et x.LV sa liste de validité. Soit I une structure de mémorisation d'un instantané.

C.1 înitialiser à vide la liste de validité x.LV

C.2 Pour chaque rafraîchissement de I

C 2.1 Si x.LV est vide alors x.LV devient la liste (i) où i = [l.t,l.t] ^A (l.x). C.2.2 Si x.LV = [L|j ^A y]

C.2.2.1 Si l.x = y alors x.LV devient [L|(j.l, j.lb, l.t, 1 ) ^A y]

C.2.2 2 Si I x≠ y alors x.LV devient

[(1 i OJJ.lb, Lt O y)) i [LtJ.ÎJ ^A <t,x)J

Pour des applications industrielles un langage restreint aux simples variables de base est naturellement trop limité. La suite de la description introduit un langage permettant de décrire des expressions plus évoluées, faisant intervenir plusieurs propositions, plusieurs variables, et permettant de décrire des notions complexes d'ordre, de concomitance, d'occurrence dans des délais stricts, de décalages temporels, de changement de valeur.

Définitions

Dans la suite de la description, certains termes seront utilisés pour mieux comprendre et définir l'objet de l'invention, certaines définitions sont données ci-dessous.

Quelques notions sur les ensembles et les prédicats

Produit en croix d'ensembles: Le produit en croix des ensembles E et F, noté ExF, est l'ensemble des couples de la forme (x,y) où x est un élément de E et y un élément de F. Puisque ExF est aussi un ensemble, si G est un troisième ensemble, alors (ExF)xG est également défini et est le produit en croix de E,F et G. Plus généralement le produit en croix s'étend à n ensembles : soit Ei ... E _n des ensembles leur produit en croix noté Eix ... xE _n est (Ειχ , . ,χ E _(n ι ,)χΕ _π .

n-uplet: Un élément de Eix ... xE _m n > 0. qui est de la forme (x _{1 f} x _n ) avec x, G E, est appelé un n-uplet.

Prédicat : Un prédicat sur un ensemble E est un sous-ensemble de E.

Exemple : le sous-ensemble {0. 2, 4, 6 ...} des entiers naturels est appelé prédicat de parité. Un entier est pair s'il appartient à cet ensemble.

Symbole de prédicat : un prédicat est souvent dénoté par un symbole. Si O est un symbole de prédicat, on notera O.set l ^' ensemble qu ^' il dénote.

Par exemple le symbole < dénote le prédicat de 9vx3î (où Sx dénote l'ensemble des nombres réels) qui contient tous les couples (x,y) e ΊχΊ tels que x est strictement plus petit que y. Le prédicat d'égalité sur les réels, de symbole =, est l'ensemble des couples de Sa forme (x,x) de 9îx9i

La notation usuelle x < y signifie, en notation ensembliste, (x,y) e < set. La notation usuelle x = y signifie, en notation ensembliste, (x,y) e - set Suivant le contexte on utilisera les notations usuelles ou les notations ensemblistes.

Ârité d'un symbole de prédicat : Si O est un symbole de prédicat dénotant un sous-ensemble d'un produit en croix de n ensembles (O.set c E tx ... xE _n ), ce symbole est dit d'arité n ou encore n-aires. On dira aussi unaire pour 1- aire et binaire pour 2-aires

Satisfaction d'un prédicat i Un élément satisfait un prédicat s'il appartient à ce prédicat.

Exemples :

· 3 ne satisfait pas le prédicat de parité car 3 e {0,2,4,8 ...}.

• (3,23, 2.02) < set

• (2.02. 3.23) e < set

Dans la suite de la présente description, le problème de la satisfaction d'un prédicat par un élément est supposé résolu par une procédure de décision existante, externe au procédé. Par exemple le problème de savoir si (2,3)€ <.set (à savoir si 2 < 3, en notation usuelle) est implanté par un algorithme externe au procédé.

Spécification formelle des comportements redoutés

Considérant les variables du système à surveiller nous supposons que ces variables viennent avec un domaine, des fonctions et des prédicats canoniques qui leurs sont propres. Par exemple, dans l'exemple du compte bancaire, nous pouvons supposer que la variable « solde » a pour domaine l'ensemble des entiers relatifs Z lequel vient avec ses prédicats classiques dont les symboles sont <,>,= et des fonctions classiques dont les symboles sont +,-. En premier lieu le langage se compose de termes.

Langage noyau :

On décrira en premier un langage dît « noyau » composé d'opérateurs fondamentaux. En second lieu nous donnerons un langage plus étoffé et plus proche des applications pratiques. Le langage se compose de termes et de formules. Les formules se distinguent des termes en ce que les formules sont des expressions qui ne peuvent avoir pour valeur que 0 (faux) ou 1 (vrai). C'est pourquoi, pour les formules, nous dirons indifféremment « est vrai » pour « vaut 1 » et « est faux » pour « vaut 0 ».

Termes du langage noyau

Les termes du langage de la présent invention sont :

• Tout symbole de constante est un terme

• Si x est le nom d'une variable (signal ou proposition) alors x est un terme

• Si 01 , _n sont des termes alors le n-uplet (a, , ... ,σ _η ) est un terme

• Si σ est un terme et a un réel différent de 0 alors V _[a ] σ est un terme

• Si f est un symbole de fonction et σ un terme alors f(o) est un terme

• Si Φ est une formule au sens défini plus loin, i un intervalle standard ou non-standard mais infini seulement à gauche alors N. Φ est un terme

• Si σ est un terme alors Top a, Bot a et X[ _n j σ sont des termes

En notation BNF l ^' ensemble des termes est donné par la grammaire

^T donnée ci-dessous:

r ::= c | x | (r,...,r) | f(T)

^■ · = ! Ί σ.-. ^T ) i V _!a] ^Ύ I N, Φ I Top ^T | Bot | χ _[η] Γ | ffr )

où f est un symbole de fonction, Φ une expression au sens de la grammaire définie ci-après. La sous-grammaire Γ de ^T dénote l'ensemble des termes dits non-décalés.

Sémantique intuitive des termes du langage noyau:

• Si c est une constante alors le terme c (dans le langage) dénote la fonction constante c(t) qui vaut toujours a

• Si x est un signal alors à la date t le terme x (dans le langage) vaut l,x où I est le plus proche instantané situé avant t. On notera x(t) cette vaîeur,

• A la date t un n-uplet de termes (oi , ... , σ„) vaut (oi(t), o _n (t)) où Ok(t) dénote la valeur du terme a _k en t.

« A la date t le terme f(o) vaut f(o(t)). • Le terme V[ ₈ ]0 dénote la valeur du terme σ décalée de a dans le temps c'est-à-dire qu'en t le terme V _[a jo vaut o(t+a) pour tout date t.

» Le terme Ν,Φ vaut l'entier n à la date t si n est le nombre d'intervalles de validité de Φ qui ont une intersection non vide avec ίφ t.

• X _t n] est un opérateur de décalage. Le terme X _[n] σ vaut en t ce que vaut le terme σ selon l'instantané l _(l(+ n) où l« est le plus proche instantané situé avant t,

• L'opérateur Top est appelé opérateur de front montant. Top Φ vaut la valeur v en t si Φ passe de la valeur u à v (u ≠ v) en t (sachant que u peut être « nil » la valeur non définie)

• L'opérateur Bot est appelé opérateur de front descendant. Bot Φ vaut u à la date t si Φ passe de la valeur u à la valeur v (u≠ v) en t.

Formules du langage noyau

La syntaxe du langage formel de spécification des comportements redoutés selon l'invention est la suivante :

• Si σ est un terme, que O est un symbole de prédicat alors Ο(σ) est une expression du langage selon l'invention

• Si Φ est une expression dudit langage, a un réel non nul, b un réel, alors sont aussi des expressions de ce langage :

Μ

Top Φ

Βοί Φ

• ( )

Xfni Φ (avec Φ purement booléenne, concept défini ci-dessous) Si Φι et Φ ₂ sont deux expressions dudit langage, i+ un intervalle tel que i.ub > i.ib > 0, d un réel tel que d > 0, que k e {0, 1 } alors sont aussi des expressions de ce langage :

• Φι S _(d,k) ?

En notation BNF le langage noyau est donné par la grammaire Φ suivante:

Γ ::=ο | χ| (Γ,...,Γ)|ί(Γ)

^T := Γ I r,..., T ) 1 v _[a] ^T I Η,Φ ITop" I Bot- | Χ, _η] Γ [ f ( )

§ ::= Ο(Γ)

1(B)

Φ ::= i.

|0(τ )

I X[n] B

| Φ S ₍ c Φ

| Top Φ | Bot Φ

Où a est un réel non nul, d un réel positif ou nul, n un entier relatif non nul. Exemple de formule (qui sera écrite plus lisiblement lors de l'introduction d'opérateurs dérivés)

=((N,o _f Top i=(P,D)),1)

Nous verrons plus loin que, avec le langage dérivé, cette expression peut être rendue plus lisible et plus intuitive. La sous-grammaire E de Φ désigne l ^' ensemble des formules dites purement booléennes. Comme on peut te voir une formule de £ n ^' est en réalité qu ^' une composition de prédicats, donc un prédicat. L ^' union des expressions des grammaires E et Γ forment l ^' ensemble des expressions que nous appellerons « non décalées ». Sémantique intuitive des formules du langage noyau :

• Ο(σ) est vraie en t si a(\) e O.set. Par exemple prenons l'expression >σ où σ est le couple ((x + 1 ), y) ; supposons qu'à la date 10 nous ayons x(10) = 2 et que y( 10) = 1 , Donc en 10 l'expression >( (x + 1 ), y) est vraie puisque ((x + 1 )( 0), y(10)) = (2+1 , 1 ) = (3, 1 ) e >.set (>.set désigne l ^' ensemble associé au symbole >).

• L ^' opérateur V _W est un opérateur de décalage (le « V » vient de l'expression anglo-saxonne « Value »). _!aj Φ est vraie (vaut 1 ) en t si et seulement si Φ est vraie (vaut 1 ) en t+a

• X _j n] est un opérateur de décalage (le « X » vient de l'expression anglo-saxonne « neXt »). La formule X _[n] Φ est vraie en t si la formule purement booléenne Φ est vraie selon l'instantané l^+n) où l _k est le plus proche instantané situé avant t.

• L'opérateur Ui ₊ porte aussi sur le futur (le « U » vient de l'expression anglo-saxonne « Until »). Par exemple Φι U[ _a ,b] Φ2 signifie intuitivement ; « ? sera vraie entre a et b et Φι sera partout vraie entre temps », Plus rigoureusement la formule Φι Uj ₊ Φ2 est vraie en t si et seulement s'il existe une date t ^' de (i+)©t où Φ ₂ est vraie et que Φ1 est partout vraie dans l ^' intervalle [t, t'[. Son intervalle de portée, i+, possède des bornes positives ou nulles. En revanche la fermeture sur les bornes de i+ est libre.

• L'opérateur S _Î+ porte aussi sur le passé (le « S » viens de l'expression anglo-saxonne « Since »). Par exemple Φ1 S[ _a , ] Φ2 signifie « Φ ₂ sera vraie vers le passé entre b et a et ι sera partout vraie entre temps ». Plys rigoureusement la formule Φ< S,+ Φ2 est vraie e t si et seulement s'il existe une date t' de (rev(i-*-))®t où Φ2 est vraie et que Φ ₁ est partout vraie dans l'intervalle Jf, t]. Son intervalle de portée, i+, possède des bornes positives ou nulles. En revanche la fermeture sur les bornes de i+ est libre.

• L'opérateur S _{c ) porte aussi sur le passé,

signifie intuitivement : « Φ ₂ sera vraie vers le passé au-delà de -d et Φι sera partout vraie entre temps ». ι S _(d>k) Φ ₂ est vraie en t s'il existe une date t' au delà de t-d (t-d comprise si k = 1 et t-d non comprise si k = 0) dans le passé où Φ? est vraie et que Φ1 est partout vraie sur ]t',tj.

• L ^' opérateur Top est appelé opérateur de front montant. Top Φ est vraie à la date t si Φ passe de faux à vraie en t.

• L ^' opérateur Bot est appelé opérateur de front descendant. Bot Φ est vraie à la date t si Φ passe de faux à vrai en t.

Langage dérivé

Dans le langage dérivé nous ajoutons des opérateurs qui ne sont pas fondamentaux en ce sens qu'ils ne font qu ^' abréger des formules pouvant s ^' écrire avec seulement les opérateurs fondamentaux. Par exemple la formule E, Φ n ^' est qu ^' une abréviation de ((Ni Φ) > 0). L ^' ajout explicite de ces opérateurs présente néanmoins un double intérêt :

• Ergonomique : ces opérateurs supplémentaires sont plus intuitifs lors de la mise en pratique du langage, ils rendent les expressions plus facile à relire et à comprendre

• Calculatoire : pour chacun nous pouvons définir un mode de calcul qui sera plus efficace que le mode de calcul tiré de l ^' opérateur fondamental (par exemple pour Ei il existe un calcul dédié plus efficace que serait celui de ((N, Φ) > 0»

Les éléments de langage additionnels sont fes suivants:

• Tout symbole de proposition est une expression du langage selon l'invention (p abrège la formule i =(p, 1 ) )

• Si Φ est une expression dudit langage, i un intervalle, a un réel, k @ une symbolique de prédicat unaire sur les entiers naturels (sous-ensemble des entiers naturels), alors sont aussi des expressions de ce langage :

o Ε« Φ

o G, cl>

o -ι Φ

o Φι Λ Φ _?

o Φ) V #2

o ΐ > Φ?

₀ Φ, ? Φ : Φ; _Ϊ

o B ₍ e, _k) Φ

ο Β{@} _(θΛ) Φ

o B0t{@}: Φ

La symbolique de prédicat @ peut par exemple être donnée sous les formes suivantes :

o = r

o < r

o > r

o [r,q]

Avec r > 0 et q > r (où r, q sont des entiers naturels)

Sémantique intuitive des éléments additionnels de langage

Pour faciliter la lecture on utilise les notations usuelles z-y pour - (z,y) et zxy pour x(z,y).

• Si p est un symbole de proposition, p est vraie à la date t si l.p = 1 où I est le plus proche instantané situé avant t. Ainsi p abrège la formule =(p, 1 ) du langage noyau.

• L'opérateur — est la négation, -Φ abrège (1 - Φ), Elle vraie à une date t si et seulement si Φ est fausse a cette date t. L'opérateur Λ est appelé conjonction. La formule ι Λ Φ2 n'est vraie à une date t que si Φι et Φ ₂ sont toutes deux vraies à cette date t. Elle abrège Φι x 2.

L ^' opérateur v est appelé disjonction. La formule est vraie à une date t si Φ1 ou Φ ₂ est vraie à cette date t. La formule Φι v Φ ₂ abrège ((Φ1 + Φ ₂ ) - (Φ¾ x Φ ₂ )) du langage noyau.

L'opérateur → est appelé implication. La formule Φ ₁ → Φ? est fausse en t si nous avons Φ _\ vraie en t et Φ _? fausse en t ; elle est vraie dans les autres cas. Elle abrège - Φι v Φ ₂ soit =((1 - Φ1 ) + Φ _? - ((1 - Φι ) x Φ ₂ ), 1 ) du langage noyau.

L ^' opérateur tripartite ? : est l'opérateur si-aiors-sinon. Φι ? Φ ₂ : Φ ₃ est vraie en t si Φ1 et Φ2 sont vraies en t ou bien si Φι et Φ ₃ sont vraie en t. Φ1 ? Φ _? : Φ ₃ abrège donc ( 1 Λ Φ ₂ ) V (-1Φ1 Λ Φ ₃ ).

L ^' opérateur E, est appelé opérateur existentiel. La formule E Φ est vraie à une date t s'il existe au moins une date t ^* de l'intervalle i Φ t où Φ soit vraie. Ainsi elle abrège l ^' expression ((Ν,Φ) >0) du langage noyau. Une représentation est donnée à la figure 4A, sur laquelle E, Φ est vraie en t car il existe des dates où Φ est vraie dans î Θ t (celles représentées par l'intervalle j). L ^' opérateur E, peut adresser simultanément le futur et le passé car les bornes de i, son intervalle de portée, peuvent être positives, négatives ou nulles. Cet intervalle de portée n'est pas nécessairement fermé sur ses bornes.

L'opérateur G, est appelé opérateur universel. La formule G, Φ est vraie â une date t si en toute date f de l ^' intervalle i®t alors Φ est vraie en f. Elle abrège ~,(Ej (~ )) soit 1 -«N _« (1- ))>0). L'opérateur G, peut adresser simultanément le futur et le passé car les bornes de i, son intervalle de portée, peuvent être positives, négatives ou nulles. Cet intervalle de portée n'est pas nécessairement fermé sur ses bornes.

• L'opérateur B _(ejk > porte sur ie passé (le B vient de Before). Cet opérateur signifie intuitivement : « antérieurement à e». B _(e, k) Φ abrège (N ₍ o _∞,e ,k) Φ)>0. B _¾e . _K! Φ est vraie en t si Φ est vraie dans

(û,- ^∞ t+e,k).

• L'opérateur B{@}, _t . _ik! porte sur le passé. Cet opérateur signifie intuitivement : « le nombre d'intervalles antérieurs à e satisfait @». B(e,k){@} Φ abrège @(N ₍₀ ,- _∞ . _e ,k) Φ). B{@} _(e>k) Φ est vraie en t si le nombre d'intervalles la liste de validité de Φ ayant une intersection non vide avec (Q,-∞,t+e,k) satisfait @.

• Enfin Top{@} ₍ Φ et Bot{@} _i Φ sont des contractions de @(Ν,(Τορ Φ)) et de @(Ni(Bot Φ)). Ainsi Top{@}, Φ est vraie en t si le nombre de transitions à vrai de Φ dans i®t satisfait @. Ceci est illustré par exemple en figure 4B.

Au final, en notation BNF, ie langage complet est le suivant :

r;;=c | x|(r,...,r) | f(r)iX _[nl r

T := Γ | (T,..., - ) ) V _[a] I ,Φ i Top T | Bor | ffr )

E ::= p

| -■ E

|Ε Λ E|E v E|Ë→ Ê | E ? E :£ ^■

! Ο(Γ)

l (E )

Φ :: = E

l Φ l Φ Λ Φ l Φ v Φ| Φ→ Φ l Φ ? Φ : Φ

0( T)

i m I B{@} _{i9 kl}

I Ε Φ I G <I>

1 Top Φ I Bot Φ

| (Φ)

où c est tout symbole de constante, x tout symbole de variable, O tout symbole de prédicat, f tout symbole de fonction, p tout symbole de proposition, i un intervalle, i+ un intervalle de bornes positives ou nulles, @ une symbolique de prédicat unaire sur les entiers naturels, a tout réel différent de 0, e tout réel, d tout réel positif ou nui.

Exemples de formules.

Avec les éléments additionnels la formule donnée en exemple pour le langage noyau peut s'écrire plus lisiblement :

(Top{=1 } _[0 ,4[ P)

« p ne passe à vraie qu'une seule fois sur une fenêtre ouverte de longueur 4 » (c'est une pré-condition pour que p soit de période 4} (Top (temp > 100))→ E _{0i2] (Âlarm > 3)

« Si la variable temp franchit le seuil de 100 degrés alors une Alarme de niveau supérieure à 3 est déclenchée dans les deux secondes »

Quelques autres exemples de formules du langage complet:

O 3 Upj, 12] (H (E(1.43,5.84] (P1 Α~ι P2 )) Λ (~ ⁱ Eg.43, 7.85] Pz))

o (< (+(Xi , 1 ), V[2] Xi )) v (= ( x ₁ , 0))

La grammaire Γ permet, à partir de Signaux de base et de constantes, de construire des signaux plus complexes, des signaux décalés dans le temps, ou encore des n-uplets de signaux. Par exemple à partir du signai x et de la constante 1 nous pouvons construire le terme +(x, 1 ) (que l'on écrit plus communément (x+1 )). Les termes dénotent donc des valeurs. Les termes ne sont donc pas des expressions valides (valant 1 ) ou non valides (valant 0). La comparaison de termes, comme l'expression > (+(x,1 ), 2 ^* y) (notée plus communément (x+1 ) > 2*y), en revanche, est une expression pour laquelle la notion de validité s ^' applique.

En fait, seules les expressions de la grammaire Φ sont des expressions auxquelles la notion de validité s ^' applique. C'est pourquoi un comportement redouté spécifié au sens de l'invention sera nécessairement une expression selon la grammaire Φ donnée ci-dessus.

Dans la suite de la description, une expression de la grammaire Φ sera appelée une formule. Les parenthèses sont utilisées pour désambiguïser une formule. En effet, si l'on écrit Φι Λ Φ ₂ U[ _a ,b] Φ;¾ on ne sait s'il faut lire (Φι Λ Φ ₂ ) U[ _a ,b] 3 ou bien lire Φ1 Λ (Φ ₂ U _[a ,b] Φ3). Or ces formules ne sont pas équivalentes, d'où l'importance des parenthèses.

Par ailleurs, dans la suite de la description, nous pourrons nous contenter, pour certaines définitions et concepts, de les poser uniquement sur le langage noyau, sachant que l ^' on peut toujours s ^' y ramener.

L'ensemble des sous-expressions d ^' une expression Φ (formule ou terme) est donné par la fonction SE définie de la façon suivante ;

• SE(O) = {Φ} si Φ est une proposition, un signal ou une constante

• SE((oi, .... σ _η )) = {(σ ₁ , .... ¾)} u SE(o,) u ...u SE(o„)

» SE(* Φ) = {* Φ} u 5Ε(Φ) si * est un symbole d'opérateur, de prédicat, de fonction

• βΕ(Φι * Φ ₂ ) = { ι * Φ ₂ } u 3Ε(Φι ) u 5Ε(Φ _? ) si * est un des opérateurs binaires du langage (tels : Λ, U[ _a ,b]■·■)·

• SE((#)) = SE(#)

• SE(X _(n3 Φ) = { Xfni Φ} u SEtfr.O)} La définition de SE présente uniquement une particularité pour X; _n ] Φ qui possède une sous-expression « cachée » qui est le couple (r, Φ) où r est un signal de type entier (destiné à recevoir le numéro de l ^' instantané). Exemple 1 :

SE( -,(=(x, 0)) ) = H=(x, 0)) } u SE(=(x _« 0))

= { <(=(*. 0)) } {= (x, 0) } u SE((x,0))

= H=(x, 0)) , = (x, 0) } {(x,0)} u SE(x) u SE(0)

= { -(=(x. 0)) }, =(x. 0), (x,0) } {x} {0}

= H=(x, 0)), =(x. 0), (x.O), x, 0}

Exemple 2:

SE( E 43, 7,85] (Ρ1 Λ(-, p ₂ ))) = { E _[2 .43, 7.85] (Pi Λ(- p ₂ )), (Pi A(-, p ₂ )), ~-,p ₂ . Pi , P ₂ }

Les sous-expressions directes d'une formule sont celles placées directement sous son opérateur. Par exemple, pour -Φ il s ^' agit de Φ. Pour Φ1 U[a,b] Φ2 il s'agit de Φ< et Φ ₂ ,

Pour une formule on dira aussi sous-formules pour désigner ses sous-expressions.

Hauteur d'une expression

La hauteur d ^' une expression Φ (formule ou terme) du langage défini ci-avant est donnée par une fonction h définie de la façon inductive suivante :

• π(Φ) = 0 lorsque Φ est une proposition, un signal ou une constante

• h((oi , ... , σ _η )) = sup(h(oi), , , . , π(σ _η )) +1 où (σι , .... σ _η ) est un n-uplet de termes

• h(* Φ) = ^' ηίΦ) + 1 si * est un symbole préfsx du langage (tels Ε,, f, O, etc)

• h(#i * #2) = sup (h(#i), Η( ₂ )) + 1 où * est un des symboles binaires du langage

Exemples :

h(-, E _{[1 >2} ] ( i Λ p ₂ )) = h(E[t _.2 , ( i A p ₂ )) + 1 = h((pi Λ p ₂ )) + 1 + 1 = (sup'MPi ) Mp-iï) + 1 ) + 2 = sup(0,0)+1 +2 = 0 + 3 = 3 h( <(x, V _[2] x)) = sup(h(x), h(V _[2] x)) + 1 = sup(1 , (h(x) + 1 )) = sup (1 ,2) +1 = 3 h((-x)) = h(x) + 1 = 1 +1 = 2 (où x est une variable)

Sémantique formelle :

L'objet de la sémantique formelle est de définir mathématiquement la valeur que prend une expression selon un processus π à une date t. La notation (π,ί)(Φ) désigne la valeur de l'expression Φ en t selon π (rappel : jt(k) désigne l'instantané de rang k de π) :

• ( ,t)(c) = c

• ( ,t)(x) = ;r(k).x où x est un signal et jt(k) le plus proche instantané précédent t, c'est-à-dire que k satisfait : n(k).t≤ t < 7r(k+1 ).t (ou bien satisfait seulement n(k).t≤ t si jt(k+1 ) n ^' est pas défini)

. (π,ί)((σι σ _η )) = ((π,1)(σ,), ... , (πΜ°η))

• (π,ί)(ί(σ)) = ί((π,ί)(σ))

• (n,t)(V _[a] σ) = (π,ΐ+a) (σ)

• (ît,t)(p) = n(k).p (où p est un symbole de proposition) où n(k) est le plus proche instantané précédent t, c'est-à-dire que k satisfait : 7c(k).t≤ t < 7t(k+1 ).t (ou bien satisfait seulement n(k).t≤ t si 7t(k+1 ) n'est pas défini)

• ( ,t)(Nj Φ) vaut le cardinal de l'ensemble (j e Φ.ΐν tels que (j n.

(i®t))≠ 0 }

• (n,t)(0(a)) = 1 si ((π,ί)(σ)) e O.set et 0 sinon

• (K,t) (V _[a] Φ) = (7t,t+a)(#)

• (w,t)(Xfn _] σ) = v si 7t(k+n)(o)=v où n(k) est le plus proche instantané précédent t,

• (ît,t)(#i U - Φ2) = 1 s'il existe une date t ^* de (i*)®t telle que (π, )(Φ ₂ ) = 1 et que pour toute date t" de [t,f [ nous avons ( , !")(#,) - 1 , sinon (π,1)(Φ% Un- Φ2) = 0 • (π,!)(Φι S, , Φ ₂ ) = 1 s'il existe une date t' de (rev(i+))£&t telle que (πΧ){Φ ₂ ) = 1 et que pour toute date t" de ]t ^' ,t] nous avons (π,Ο(Φι ) = 1 ; sinon (π )( ι S _i+ Φ ₂ ) = 0

• (π,ί)(Φι S ₍ d,k) Φ2) = 1 s'il existe une date t ^' de (0,-∞.t-d,k) telle que ίπ,1')(Φ ₂ ) = 1 et pour toute date t" de ]t',t] nous avons (π,Γ)(Φι ) = 1 ; sinon (π,1)(Φι S _(d>k) Φ ₂ ) = 0

• (n,t)(Top Φ) = v si il existe r > 0 tel que (π,.')(Φ)≠ v pour toute date t'e ]t-t-,t[ et tel que (π,ί")(Φ) = v pour toute date t"e ]t,t+e[

• (n,t)(Bot Φ) = v si il existe r > 0 tel (π,ί')(Φ) = v pour toute date t'e ]t-f,t[ et que (π,Γ)(Φ)≠ v pour toute date t"e ]t,t+e[

Bien que cela soit déductible de la sémantique du langage noyau qui vient d'être donnée, nous donnons ci-dessous la sémantique de certains opérateurs dérivés :

• (κ,\)(Φ, Λ Φ ₂ ) = (τΜ)(Φ, ) χ (π,ΐ)(Φ ₂ )

• (πΛ)(Φ , ν Φ ₂ ) = (n,t)h ( ,Φ, A -,Φ ₂ ))

• (π,ί)(Φ ₁ → Φ ₂ ) = (π,1)(-π(Φι Λ -,Φ ₂ ))

• (π,1)(Ει Φ) = 1 s'il existe une date t' de i®t telle que (π,ί')(Φ) = 1 et ( 7T.t)(E, Φ) = 0 sinon

• (7c,t)(Gi Φ) = 1 si pour toute date t" de i@t nous avons (π,Ο(Φ) = 1 et (%,t)(Gi Φ) = 0 sinon

• (îi,t)(B( _e> k ₎ Φ) = 1 s'il existe une date t' de (0, -∞, t+e, k) telle que (π,ί'ΜΦ) = 1 , sinon (jt,t)(B _{e>k) Φ) = 0.

La notion de liste de validité exposée plus haut était limitée aux propositions et aux signaux. Sans sortir du cadre de l'invention, cette approche peut être étendue à toute expression de notre langage (les propositions et les signaux ne formant qu'une partie de ce langage). Pour cela nous avons besoin d'établir la façon dont les opérateurs du langage se traduisent en termes d'opérations sur les listes de validités. Bien que pour les termes la notion de validité ne soit pas applicable, nous attribuerons néanmoins aux termes du langage des listes de validité, car elles seront nécessaires pour le calcul des listes de validité des formules exprimant les comportements redoutés.

Correspondance entre éléments de langage et opérations sur les listes de validité

Il a été précédemment exposé (avec l'exemple du solde bancaire) comment se constituait une liste de validité pour une variable. Comme les formules complexes sont construites à partir des variables du système et des opérateurs du langage, pour calculer les intervalles de validités des formules complexes, il est nécessaire d'établir une correspondance entre les opérateurs du langage et des opérations sur les listes de validité. Par exemple, la liste de validité de la formule Φι Λ Φ ₂ résulte de la combinaison (particulière à l'opérateur Λ) des listes de validité de Φι et de Φ ₂ Nous allons donc établir une sorte d ^' algèbre sur les listes de validité.

Dans ce qui précède on a distingué termes et formules en mentionnant que les formules sont des expressions qui ont la particularité de ne prendre pour seules valeurs 0 ou 1 . Leurs listes de validité seront ainsi constituées d'intervalles assignés soit de la valeur 0 ou soit de la valeur 1 . A des fins d'efficacité le procédé ne stockera, pour les formules, que les intervalles de valeur 1 . Les intervalles de valeur 0 seront implicites (dénotés par les interstices).

Dans la liste de validité d ^' un terme, un interstice s ^' interprète comme une plage temporelle où le terme n'a pas de valeur définie. C'est notamment le cas pour un terme comme Top x qui n'aura de valeur que sur des intervalles de forme [t,t] où t est une date de changement de valeur de x.

A des fins d'efficacité encore, deux types de calcul vont être explicités, Le premier sera un calcul dédié aux formules purement booléennes. Le second sera un calcul valable pour n'importe quelle formule du langage. Premier calcul des listes de validité (valable uniquement pour les formules purement booléennes) figure 3:

Pour calculer la liste de validité des formules purement booléennes l ^' algorithme définit et utilise deux variables notées Φ val et Ι.Φ pour toute formule purement booléenne Φ. Comme dans ce cas Φ appartient à la grammaire E elle est de la forme Ο(Ψ) avec Ψ e Γ. Nous posons alors simplement :

• Φ-val est une variable booléenne associée à Φ.

• Φ. Ι_ν est une liste d'intervalles

· Ι.Ο(Ψ) = 1 si Ι .Ψ e: O.set et Ι .Ο(Ψ) = 0 sinon.

La première étape, étape 20, est une étape d'initialisation des valeurs de Φ,νβΙ et de Φ-LV. La variable Φ-va! est initialisée à faux (soit 0) et la variable Φ- LV est initialisée par la liste vide. L ^' étape qui suit, étape 21 , est un état d ^' attente de rafraîchissement de l'instantané I . Lorsque ce rafraîchissement intervient l ^' algorithme passe à l'étape 22 où la valeur de Ι.Φ est testée Si la valeur de vérité de Ι.Φ est à vrai (vaut 1 ) le procédé teste, étape 23. la valeur de Φ.νβΙ. Si Φ-val est à vrai alors, étape 24, le procédé prolonge le dernier intervalle de #.LV jusqu'à l.t compris (intervalle fermé sur la valeur l.t). Si la valeur O.val est à faux (vaut 0) alors, étape 25, le procédé ajoute à la fin de Φ-LV le nouvel intervalle [l.t, l.t].

Si au contraire, à l'étape 22, Ι.Φ est faux (vaut 0), alors le procédé teste Φ-val. Si Φ val est à vrai (vaut 1 ), étape 26, alors le procédé prolonge le dernier intervalle de #,LV jusqu ^' à l.t non compris (ouvert sur l.t ) (étape 28), Si .vai est à faux, alors te procédé laisse ΦΙ,ν ^* inchangée (étape 27). A îa suite des étapes 24, 25, 27 et 28, le procédé affecte à O.val îa valeur de Ϊ.Φ (étape 29). Puis le procédé retourne à l'étape 21 d'attente de rafraîchissement de I, le calcul se prolongeant tant que le procédé est maintenu en fonctionnement.

En tant que tel, il n ^' existe pas de condition d'arrêt pour cet algorithme de calcul puisqu'il se met en attente d'un nouvel instantané. Il peut néanmoins être facilement modifié si l'indication qu'un instantané est le dernier est disponible. Dans ce cas le retour à l'étape 21 serait soumis à la condition que l'instantané soumis ne soit pas le dernier. La condition d ^' arrêt sera déterminée par une stratégie d'utilisation du procédé complet c ^' est-à- dire par une stratégie d ^' exploitation des listes de validité.

Exemples de calculs de Ι.Φ:

Exemple 1 : considérons pi v p ₂ . Supposons un instantané I tel que l.p< = 0 et l.p ₂ = 1. Alors l.(pi v p ₂ ) vaut 1 si + p ₂ - pi x P2),1 ) est vraie soit si

soit si (l.pi + l.p ₂ )~ (l.pi x l.p ₂ ) = 1

soit si 1 - 0 = 1 .

Comme c'est le cas on a l.(pi v p ₂ ) = 1 lorsque l. i = 0 et l.p ₂ = 1.

Exemple 2 :

Considérons la formule (=(-(x,1 ),0)) dont la notation usuelle est ((x-1 ) = 0) . Supposons un instantané I tel que l.x = 2. Alors l,(=(-(x,1 ),0)) vaut 1 si (l.(-(x,1 )), I.0) e =.set, soit si ((-(l.x.1,1 ), 0) e =.set soit si ((2 -1 ), 0) e =.set soit si (1 , 0)€ =.set. Comme ce n'est pas le cas alors l.(=(-(x,1 ),0)) vaut 0. Second calcul des listes de validité (valable pour toute expression mais moins efficace que le premier si appliqué à une formule purement booléenne)

Le calcul des listes de validité des formules non purement booléennes est maintenant abordé. Contrairement aux formules purement booléennes qui peuvent être calculées simplement en considérant la valeur que leur attribue un instantané I (soit Ι.Φ) et la valeur qu ^' elle avait auparavant (soit Φ val), pour une formule non purement booléenne le calcul de sa liste de validité repose sur une composition des listes de validité de ses sous- expressions directes, composition qui est fonction de la nature de la formule. Nous allons donner ci-dessous quelques intuitions de cette composition propre à chaque opérateur. Ces intuitions ne présagent pas que le calcul est fait « en ligne » ou « hors ligne ». Cette distinction sera envisagée plus loin lorsque l'on abordera les principes de certitude, de définition, de continuation et de zone d'influence. Nous faisons l ^' hypothèse implicite que le calcul est fait sur une certaine plage temporelle (qui n'a pas besoin d ^' être précisée pour exposer les principes). Une description formelle et prenant en compte tous les aspects du procédé est en revanche donnée en Annexe 1.

Cas du terme c

Si c est un symbole de constante alors c.LV est (Dom ^A c) c ^' est-à- dire la liste contenant pour unique intervalle son propre domaine avec c pour attribut de valeur.

Cas d'un signa! x

L'algorithme a été donné plus haut dans le cas de l'Algorithme de calcul de la liste de validité d ^' une variable.

La liste de validité de ν _[3ΐ Φ s ^' obtient en décalant de (-a) tous les intervalles de la liste de Φ. Autrement dit i Φ (-a) appartient à la liste de validité de V _iaj O si et seulement si i appartient à la liste de Φ.

Cas de X _[n] σ

Comme vu dans la définition de SE l ^' expression X _[ri] Φ possède une sous-expression cachée qui est (r, σ). Le signal r reçoit le numéro de l ^' instantané (le numéro d'un instantané peut très bien être une variable).

Si i ^A (k,x) et j ^A (k+n,y) sont des intervalles de (r, σ) alors on adjoint i ^A y dans la liste de X _[n j σ.

Cas d'un n-uplet de termes a ·■· , σ _η

Supposons que i ^A (si , .... s _k ), k > 0, soit un intervalle pour le k- uplet de termes σι, ... ,a _k et j ^A s _M un intervalle pour le terme o _k+1 . Alors l'intervalle (i n j) ^A (si, ... ,Sk+i ) est un intervalle pour le (k+1 )-uplet de termes ai , ... ,0k A+i* Puisque nous savons calculer pour les termes de base c, x, V[ _a] 0, Xt _n }0 et que nous savons passer du calcul d'un k-uplet à celui d ^' un (k+1 )-uplet, par induction nous sommes donc en mesure de calculer un intervalle pour n'importe quel n-uplet de termes σι, ..., σ _η avec n > 1 , Exemple : supposons que i = [1 ,3] ^Λ (5.8) soit un intervalle pour (σι, σ ₂ ) et que j = [2.4] ^Λ 63 soit un intervalle pour σ ₃ . Alors [2,3] ^Λ (5.8, 63) est un intervalle de validité du 3-uplet de terme (σι, 02, 03).

Cas du terme f(o).

Soit i ^A s, un intervalle du terme σ. Alors i ^A f(s) est un intervalle de la liste de validité du terme f(o).

Exemple : prenons le terme +(x, y). Supposons que ([1 .3[ ^Λ 0.5,[3,5] ^Λ 1 ) soit la liste de validité de x et que ([1 ,2[ ^Λ 0.3,[2,5] ^Λ (-2)) soit celle de y.

Alors la liste de validité de (x, y) sera :

ί[1 ,2[ ^Λ (0.5,0.3). [2.3[ ^Λ (0.5,-2), [3.5] ^Λ (1 .-2))

Et celle de +(x, y) sera :

([1 ,2[ ^Λ (0.8), [2,3P(-1.5), [3,5] ^Λ (-1 ))

Cas d'une formule de type Ο(σ).

Soient i ^A s un intervalle du terme σ. Alors i est un intervalle de la liste de validité de la formule Ο(σ) si se O.set.

Exemple : soit la formule <(σι , 02) et supposons que i = [1 ,3] ^Λ 5 soit un intervalle pour σι et que j = [2.4] ^Λ 8 soit un intervalle pour 5 ₂ - Donc [2,3] ^A (5,8) est un intervalle de validité du terme (σ-ι , σ ₂ ). Comme (5,8) e <.set, il suit que [2,3] est à adjoindre à la liste de validité de <(θι , σ ₂ ).

Cas de l'opérateur

La figure 5A illustre le calcul de la liste de validité de Φ connaissant celle de Φ. Le principe est le suivant : deux intervalles successifs i et i+1 de Φ donnent lieu à un intervalle pour Φ qui s'insère entre i et i+1 (Voir Annexe 1 pour une description plus détaillée).

Cas de l'opérateur

La liste de validité de Φι Λ ? est fonction de celles de Φι et de Φ ₂ . Le principe est ie suivant 1 si ii est un intervalle de Φι et i ₂ un intervalle de Φ2 et que H n i ₂ ≠ 0, alors n i ₂ est un intervalle de Φι Λ Ζ Pour générer la liste de validité complète à partir de celles de Φ1 et Φ ₂ nous pouvons procéder comme suit. On choisit par exemple un parcours antichronologique. Soit il le dernier intervalle de d>i ,LV et i2 celui de Φ .Υλ/. Tant que i2 n'est pas inférieur à il adjoindre ii n et réitérer en remplaçant t2 par son prédécesseur ; si t2 est inférieur à i l réitérer en remplaçant il par son prédécesseur (Voir Annexe 1 pour une description plus détaillée). On obtient ainsi un algorithme linéaire en temps (le nombre d ^' éléments parcourus est proportionnel à celui contenus dans les listes de Φι et Φ ₂ ).

Cas de l'opérateur v.

La liste de validité de Φτ Φζ est fonction de celles de et de Φ ₂ .

Il est possible d'utiliser le calcul de ,(-^Φι Λ --.Φ?). Néanmoins il est aussi possible de suivre une méthode plus directe en se basant sur le fait que Φι νΦ ₂ est vraie si et seulement au moins l'une des listes Φι ou Φ ₂ est vraie. Tout d ^' abord le procédé fait un choix de sens de parcours des listes de validité des listes de Φι et de Φ ₂ . Il semble plus judicieux de partir de la fin des listes. Soient h et i ₂ les derniers intervalles de respectivement <î .LV et de Φ ₂ LV.

Un premier choix entre il et i2 consiste à choisir l'intervalle qui va le plus loin dans le futur (où i « va plus loin dans le futur que » j signifie que soit nous avons i. ub > j.ub soit nous avons si i.ub = j.ub et i.u = 1 et j.u = 0). Si ce choix n ^' est pas possible car ils vont tous deux aussi loin dans le futur (c ^' est- à-dire if .ub = i ₂ .ub et H .U = i ₂ .u) alors on prend des deux celui qui va le plus loin dans le passé. Prenons, sans perte de généralité, le cas où ii serait choisi selon ces critères. On fait entrer h dans la liste de validité («ÎM V # ₂ ).LV de <t>fv #2 par adjonction à gauche. Ensuite on recherche dans les prédécesseurs de i ₂ ¾ compris) te premier intervalle i qui soit tel que i < i- _s ou bien qui chevauche ι ·, à gauche. On l'assigne à i ₂ (môme si i vaut Nil). On assigne le prédécesseur de u à H . Puis on réitère le procédé en refaisant un choix entre les nouveaux ii et h et ainsi de suite jusqu'à épuiser les listes i . LV et Φ ₂ .ί\ , Ainsi, de proche en proche, et selon un algorithme linéaire en temps, on construit la liste de validité de ΦινΦ ₂ .

Cas de l'opérateur Ej

Pour le calcul de Ej Φ on propose un algorithme plus efficace que celui qui consisterait à calculer (Ν,Φ > 0). Ce calcul est illustré en figure 5B,

Considérons la formule E, Φ. Supposons que j soit un intervalle de validité de

Φ. D'après la sémantique de E, Φ on déduit que toute date t telle que (t ® i) n j≠ ø est une date de validité de E, Φ engendrée par j.

Il suit que Q.\ x i.u, j.lb - i.ub, j.ub - i. lb, j.u x i.l) est un intervalle à adjoindre à la liste de validité de E, Φ.

Justification : considérons la borne inférieure j.lb - i.ub. on obtient i

(j.lb - i.ub) Φ i = (i.l, j. lb - i.ub + i.lb, j.lb - i.ub + i.ub, i.u)

= (i.l, j.lb - i.ub + i.lb, j.lb, i.u)

Or (i.l, j.lb - i.ub + i.lb, j.lb, i.u) n j≠ 0 si et seulement si i.u = 1 et j.l = 1 . D'où la borne inférieure et sa fermeture dans l'intervalle engendré (j.l x i.u, j.lb - i.ub, j.ub - i.lb, j.u x i.l). Le même raisonnement conduit à justifier la borne supérieure et sa fermeture.

Exemple : supposons que [4,9] soit dans la liste de validité de Φ. Considérons la formule E ₍ . , .; _¾ [. Alors (1 x0, 4 - 3, 9 - (-1 ), 1 x1 ) soit ]1 , 10] sera à adjoindre à la liste de validité de Ε _ι3ί .

Cas de l'opérateur G,

Considérons la formule G, Φ. Supposons que j soit un intervalle de validité de Φ. Alors j J i est un intervalle à adjoindre à la liste de validité de G _< Justification : ceci découle de la sémantique selon laquelle G, Φ est vraie en t si (i.l, i.lb + t, i.ub + t, i.u) est inclus dans j. Donc au maximum on peut avoir i.ub _* t = j.ub. Donc au maximum t = j.ub - i.ub et ia borne supérieure est j.ub - i.ub. Maintenant la fermeture i si j.u = 1 alors (i.l, i.ib + j.ub - i.ub, i.ub + j.ub - i.ub, i.u) = (11, i.lb + j.ub - i.ub, j.ub, Lu) peut-être inclus dans j quel que soit Lu. En revanche si j.u = 0 il n'y a inclusion que lorsque i.u = 0. Finalement H n ^' y a pas inclusion que lorsque j.u = 0 et Lu = 1 . La fermeture sur la borne supérieure est donc la fonction logique (-1 i.u) v j.u qui ne vaut 0 que lorsque j.u = 0 et i.u = 1. De façon plus concise on peut écrire cette fermeture i.u => j.u en vertu de l'équivalence logique : ((--1 a) v b) = (a => b). Exemple 1 ; supposons que [4,9] soit dans la liste de validité de Ψ ou Φ ?. Considérons la formule Θ _[~ ι _, ¾. Alors (1 = 1 , 4 - (-1 ), 9 - 3, 0= 1 ) soit [5, 6] sera à adjoindre à la liste de validité de G^^. Vérification : si l'on prend n'importe quelle date de [5, 6], par exemple 6 on voit que l'on a bien [-1 ,3[ Θ 6 - (1 ,6+(-1 ),6+3.0) = [5,9[ inclus dans [4,9].

Exemple 2 ; supposons que [4,7] soit dans la liste de validité de Ψ. Considérons la formule G[. i _,3[ . Alors 4 - (-1 ), 7 - 3, 0= 1 ) soit [5, 4] est équivalent à 0 (car la borne supérieure est supérieure la borne inférieure).

En effet G[. i . _3[ demande la validité continue sur un intervalle de longueur 3 - (-

1 ) = 4 ce qui n ^' est pas le cas sur [4,7] qui n'est que de longueur 3.

Cas de l'opérateur Top

Considérons la formule Top Φ. Supposons que (l,lb,ub.u) ^A s soit un intervalle de validité de Φ Alors [lb,lb] ^A s est à adjoindre à la liste de validité de Top Φ.

Cas de l'opérateur Bot

Considérons la formule Bot Φ. Supposons que (l,lb,ub.u) ^A s soit un intervalle de validité de Φ. Alors [ub,ub] ^A s est à adjoindre à la liste de validité de Bot Φ.

Cas de l'opérateur N ₍

Considérons la formule N, Φ On suppose que l'on calcule la liste de validité de cette formule sur un domaine D En premier lieu la liste de validité de N; Φ est initialisêe avec l'intervalle à compteur DxO. Autrement dit, en toute date te compteur est mis à zéro. Puis on considère les intervalles de Φ les uns après les autres. Supposons que ] soit un intervalle de validité de Φ qui n'ait pas été encore considéré dans le calcul de Ν. . Considérons les dates de l'intervalle ftxlu _» j.lb - i.ub, j.ub - i.lb, 1xU) obtenues sur le modèle de E, Φ. Pour chaque date t de cet intervalle par construction i© t possède une intersection non vide avec j lequel n ^' avait pas été encore considéré. Donc si le compteur de t était k alors il doit devenir k+ 1 en raison de j. Autrement dit j contribue à incrémenter de 1 le compteur de toute date de (1 xi. u, j.lb - i.ub, j.ub - i.lb, 1 xi.l). Ceci revient donc à former l'intervalle à compteur (1 xi.u, j.lb - i.ub, j.ub - i.lb, 1 i.l)x1 puis à l'adjoindre à la liste de validité de N, Φ selon l ^' adjonction avec compteur (On se reportera à l'Annexe 1 pour un algorithme de calcul détaillé).

Remarque : quand i est non standard, soit de la forme (0, - a,k) on adjoint des intervalles non standard de la forme (I, Ib, + ∞, Q). En pratique ces intervalles seront coupés par l'intervalle de définition, notion qui sera vue plus loin.

Cas de l'opérateur U _i+ . Nous distinguons selon que 0e i+ ou 0 ί i+.

Cas 0 i+

Rappelons que Φι Uj ₊ #2 est valide en une date t si Φ2 est vraie à une date t' de (i+)®t et que Φ ₁ est vraie partout sur [t,t'[. Il résulte de ceci qu'un intervalle de Φι et un intervalle i ₂ de Φ ₂ tels que ii] n i ₂ = 0 (rappel ; ii] est le fermé à droite de h ) ne peuvent donner lieu à un intervalle pour Φ1 LU Φ ₂ . En effet si h] n i ₂ = 0 cela signifie qu'il existe une séparation entre h] et i ₂ par conséquent que Φι ne peut être partout vraie à partir d ^' une date de h] est jusqu'à une date de i ₂ . Donc h] n i ₂ ≠ 0 est une condition nécessaire pour que et i ₂ génèrent un intervalle pour Φι U _j+ Φ ₂ . Considérons donc, deux intervalles et i ₂ tels que ii] n i ₂ ≠ 0. Appelons r cet intervalle i-i] n i ₂ . Considérons l ^' intervalle q = (r.lx(i+).u, r. lb - (i+).ub, r.ub - (i+).lb, r.ux(i+).l). D'après ce que nous avons vu précédemment pour l ^' opérateur E,, si nous choisissons une date t dans q il est clair qu'il existe une date t ^' de (î+)© t qui soit dans r. Comme toutes les dates de r sont aussi des dates de i ₂ (puisque r = ii] . t ₂ ), cela signifie qu'en t' ₂ est vraie. Nous en déduisons que si t est choisie clans q alors il existe une date t ^" de (ϊ+)Φ t où «i½ est vraie. Choisissons maintenant t dans q n h]. Alors la date t, en tant que date de q, nous garantit comme vu ci-dessus qu'il existe une date t' de (ϊ+)Φ t où Φ ₂ est vraie. Rappelons que de plus t' est aussi une date de r. Ceci implique que t' est une date de H] (puisque r = h] n i ₂ ). Par ailleurs en tant que date de q n h] la date t est aussi une date de h]. Finalement, pour synthétiser, t et t' sont toutes deux des dates de H] et t' est dans (Ϊ+)Φ t.

Comme 0 e i+ alors t < t'. Donc t est dans et t' dans h]. C'est-à-dire que t' est ou bien dans ou bien n'est pas dans h mais est alors dans h.ub. Dans les deux cas l'intervalle (qui est continu) assure donc une continuité de validité de Φι sur [t, t'[. Comme ₂ est vraie en t' (car f est une date de r), il s'en suit que ( ι U _i+ Φ _? ) est valide en t.

Pour conclure, quand 0 c i+, l'intervalle h] n q dénote les dates où (Φι U _i+ Φ ₂ ) est vraie d'après la donnée de et i ₂ (il est éventuellement vide si q < h ). Cet intervalle sera donc à adjoindre à la liste (Φ U » Φ?).Ι de validité de Φ _ΐ U Φ ₂ .

(Une illustration est donnée en figure 5C dans le cas particulier où i+ = [a.b] avec a > 0.)

Cas 0 e i+ (donc cas de : Φι U(i _>0 , _b .i )%)

Donc i+ est de la forme (1 ,0,b,k) avec k e {0,1}, Dans ce cas l'ensemble k est lui-même un ensemble de dates qui valident Φι U|+ # ₂ . L'intervalle k doit donc aussi être adjoint à (Φι U♦ Φ ₂ ). Ι_ν. Mais si par ailleurs il existe de Φι .ί_ν qui chevauche i ₂ par la gauche comme sur la figure 5D _» les dates de qui sont aussi dans j = (ia.lxk, i^Jb - b, i ₂ .ub, i ₂ .u) valident Φ ₍ U(i,o.b } #2. Finalement s'il existe un tel qui chevauche ½ par la gauche c'est donc l'intervalle (h n j) u i ₂ que nous devons adjoindre au lieu de i ₂ seulement.

Dans l'Annexe 1 un calcul précis et formalisé est donné pour le calcul de Φι U _i+ Φ Cas de l'opérateur Sj+. Symétrique de U, ₊ dans le passé.

Cas de l'opérateur B _(a,k) .

La liste de validité de , _Λ1 φ ne dépend que du premier intervalle de la liste de validité de Φ, Supposons que i soit le premier intervalle de la liste de validité de Φ alors B _{ie k)} <t> est valide sur (i.uxk, i.ub - e, «, 0). En pratique on limitera la borne supérieure de cet intervalle suivant l'intervalle de définition, notion qui sera vue plus loin.

Cas de l'opérateur S _(d,k) .

Considérons la formule Φι S^ _k ^ . Là encore pour que de Φι et i ₂ de #2 produisent un intervalle pour Φ S _(d , _k ) Φ ₂ il faut que i ₂ n [H≠ 0. Supposons que ce soit le cas. Posons j = (i.uxk, i.ub+d,∞,0). Alors j n ^" , est un intervalle de validité pour Φι S _!d.k ^.

Dans les descriptions ci-dessus un seul exemple d'intuition a été donnée pour chaque opérateur, des bases du calcul. Il existe de multiple façon de composer des listes de validité avec un résultat identique. L'essentiel est que le calcul soit conforme à la sémantique donnée pour le langage. Dans l'Annexe 1 une description précise et complète (en pseudo-code) est donnée d'un mode de calcul possible pour chaque opérateur.

Relation entre le procédé et le calcul de la liste de validité de la formule principale

Dans ce qui précède on a décrit une version simple du procédé où te comportement redouté se réduisait à une proposition, soit « solde <0 ». Le procédé reposait sur le constat que détecter l'occurrence du comportement redouté « solde <0 » équivaut à calculer la liste de validité attachée à la formule « solde < 0 » et à tester si cette liste contient un intervalle de valeur 1. Avec la convention qui consiste à ne représenter que les intervalles de valeur 1 pour les formules, ce test revient â tester si la liste est non. Si elle ne l'est pas, cela signifie que « solde <0 » est vraie à certaines dates et donc que le comportement redouté a eu lieu. Ensuite nous avons introduit un langage plus riche pour exprimer des propriétés plus évoluées. Pour étendre le procédé à ce langage il fallait alors disposer d ^' un calcul permettant de calculer la liste de validité de n'importe quelle formule exprimable dans ce langage de sorte que l'on puisse appliquer le même principe à savoir : « détecter le comportement redouté c ^' est tester que la liste de validité de la formule qui l ^' exprime est non vide ». Or nous avons montré, au travers de deux types de calcul, que ce calcul peut être fait, pour n'importe quelle formule du langage. La seule contrainte à respecter est que lorsqu ^' on calcule la liste de validité d'une formule il faut que l ^' on ait traité d ^' abord ses sous-formules directes. Ceci n'a rien d'inhabituel : par exemple, en arithmétique élémentaire, si l'on demande de calculer a+b, il faut bien que les termes a et b soient définis et aient été calculés avant que l'on procède au calcul de a+b. Cette contrainte laisse supposer au moins deux modes de calcul pour le procédé :

· Un calcul de type récursif (reposant sur un algorithme qui s'appelle lui- même)

• Un calcul suivant la hauteur des formules

Schématiquement l'algorithme récursif est le suivant (il prend en argument une formule, nommons là Φ) :

D.1 - Si Φ est formule purement booléenne, calcul de la liste de validité selon l'algorithme propre à ce type de formule.

D.2 - Sinon identification de l'opérateur de la formule Φ.

D.2.1 - Appel (récursif) du présent algorithme sur les sous-expressions directes de Φ

D.2.2 - Selon la nature de Φ calcul de sa liste de validité en fonction de celles de ses sous-expressions.

D.3 - FIN

Le procédé, à chaque rafraîchissement de l ^' instantané I, appelle cet algorithme avec comme argument la formule principale Φ. Selon un autre mode de réalisation, le calcul de la liste de validité fait appel à un algorithme non récursif se basant sur la hauteur des formules. Schématiquement l'algorithme est le suivant (Φ est la formule principale) : E.1 - soit k = 0

E.2 - « tant que » k < Η(Φ) faire

E.2.1 - pour toute sous-formule ψ de Φ telle que h( ^l F) = k faire :

a) Si Ψ est formule purement booléenne, calcul de sa liste de validité selon l'algorithme propre à ce type de formule b) Sinon calcul de la liste de validité de Ψ en fonction de sa ou ses sous-expressions directes (qui ont forcément été déjà traitées puisque de hauteurs inférieures)

E.2.2 - k = k + 1

E.2 3 - retour du « tant que » 2.

E.3 - FIN.

Pour le procédé cet algorithme est appelé à chaque rafraîchissement de l'instantané I, sans argument.

D'un point de vue de l'efficacité on privilégiera ie calcul reposant sur la hauteur des formules. En pratique on rangera les sous-formules de la principale Φ dans une liste croissante selon la fonction h (c'est-à-dire de sorte que si Φ _; et Φ ₂ sont deux formules consécutives de cette liste on ait soit h( < ^η (Φ ₂ ) soit η(Φ = h(0 ₂ )). Ensuite, à chaque rafraîchissement de l'instantané on parcoure cette liste à partir du début et pour chaque formule rencontrée on procède au calcul de ses intervalles de validité. A chaque formule rencontrée nous sommes sûrs que les sous-formules ont déjà été calculées puisque, de hauteurs inférieures, elles ont été parcourues avant la formule courante.

Dans ce qui précède ors a présenté un calcul des liste de validité sans nous préoccuper de la plage temporelle qu'il était nécessaire ou possible de calculer. Les principes du calcul rigoureux, optimisé et en ligne vont être exposés ci-après. Comme il va être vu, ii s'agit de conserver les résultats déjà obtenus lorsque le procédé est assuré qu'ils ne seront plus modifiés et de ne faire, à chaque nouveau rafraîchissement de l'instantané, que les calculs nécessaires au prolongement de ces résultats. De sorte que le calcul peut être vu comme une suite de calculs locaux qui prolongent des résultats acquis antérieurement.

Principes du calcul en ligne (définition, continuation et zone d'influence)

Le procédé de calcul selon l'invention efficace, en ligne, et à mémoire bornée, des intervalles de validité repose sur des principes originaux qui vont être exposés. Ce sont les principes de certitude, de définition, de continuation et de zone d'influence. Corollaire de la notion de zone d'influence, la notion de date d'inutilité permet de doter le procédé d'un mécanisme essentiel à son fonctionnement sans limite de durée, à savoir l'élimination des intervalles devenus non pertinents du point de vue de la problématique de détection du comportement redouté.

Intervalle de certitude : un intervalle i est un intervalle de certitude pour l'expression Φ si pour tout encadrement π' de π alors la validité de cette expression Φ selon π' et π est identique sur cet intervalle i c'est-à-dire que pour toute date t de i alors (π',ί) |= Φ si et seulement si (π,ί) |= Φ.

Exemple : soit le processus π composé de deux instantanés π(0) et π(1 ) tels que

π(0).ρ = 1 , π(0).ί = 2.8

π(1 ).ρ = 0, 7i(1 ).t = 3.4

alors par exemple [2.8,3] est un intervalle de certitude pour la proposition p en vertu de la définition de la sémantique des propositions. Car en effet si nous prenons n'importe quelle date t de [2.8,3], la validité de p dépend du plus proche instantané qui précède cette date t, qui est π(0) de date π(0).Ι = 2.8. Donc si nous considérons n'importe quel encadrement π' de n, la validité selon ι' de p sera inchangée sur [2,8,3]

Intervalle de définition i l'intervalle de définition d'une formule Φ selon un processus π, noté def-ίΦ), est le plus grand intervalle (au sens de l'inclusion) de l'ensemble de ses intervalles de certitude. Exemple : pour reprendre l'exemple précédent, l'intervalle de définition de p est [2.8.3.4] (soit le domaine temporel de π).

Une autre manière de voir l'intervalle de définition d ^' une formule Φ selon un processus π est de le voir comme l ^' intervalle où la validité de Φ est non seulement certaine mais aussi ne dépend que de π.

Il est aisé de donner un sens concret à ce concept pour les propositions (et par extension aux formules purement booléennes). En effet un processus π. en tant que suite finie d'instantanés, possède un premier et un dernier instantané. Appelons les π first et jt.last de dates respectives ( K.first).t et (Ti. last).t. Il est alors clair que la validité de toute proposition et plus généralement de toute formule purement booléenne est complètement définie sur l'intervalle [(π. first). t, (7i.last).tj et que sur cet intervalle la validité de cette classe de formule ne dépend que de π.

Pour généraliser à toutes les formules nous allons définir une fonction def,. qui associe à toute formule, relativement à un processus, son intervalle de définition. On pose : def _E (p) = [(jt.first).t, (mlast).t]

Détermination de i def^N, Φ)

Selon la sémantique de l'opérateur N, la validité de N, Φ en une date t dépend de la validité de Φ dans l'intervalle t ® i. Donc, étant donnée def^). les dates où la validité de N, Φ est définie et dépend uniquement de Φ (donc uniquement de π) sont les dates où t Θ i ç def^t»). Ceci est illustré par la figure 6.

Selon cette figure 6, nous voyons qu'en ¾ et ta la validité de N, Φ dépend de dates qui ne sont pas dans def-^î>) (celles figurées par les lignes en pointillés). Elles ne seront donc pas dans def-(N. Φ), En revanche ti et t ₂ seront dans def _T:: ( N, Φ). On peut voir également que t, et ta sont les bornes de def _rt (N, Φ).

En formalisant ces idées on obtient :

def _K f N, Φ) = { t / 1 Θ î c def,(#) } Comme t © ί = (i.l, i.lb + t, i.ub + 1 _» i.u) la date maximum t _max de def-( N, Φ) est telle que : i.ub + t _max = de¾¥).ub, soit t _max = def^( F).ub - i.ub.

Ceci signifie que la borne supérieure de deL(N, Φ), soit (def.(N, #)),ub est : def _n ( ).ub - i.ub.

Déterminons maintenant la fermeture de def _K (N, Φ) sur cette borne supérieure. Il s'agit en fait de déterminer, en fonction de i.u et def _K (#).u si la date def;-^l>).ub - i.ub est ou non dans def„( N, Φ).

Cas 1 : i.u = 1 et def^).u = 1

Donc (def _TC (#).ub - i.ub) Φ i est un intervalle de la forme suivante (le X remplace les valeurs non pertinentes pour le raisonnement) :

(X, X, def _s (d>).ub - i.ub + i.ub, i.u)

soit (X, X, def^.ub, 1 )

Comme def^) est aussi de la forme (X, X, def-^>).ub, 1 ), cela signifie que l'inclusion est assurée sur la borne supérieure, donc que def _K (Nj Φ).υ = 1 lorsque i.u = 1 et def _r ^).u = 1.

Les autres cas sont résumés par le tableau suivant :

D'après ce tableau il ressort que :

de j #).u = (-i Lu) v αβί _Ε (Φ).ο

= i.u => def _K ( ).u

(Rappel : => est l'implication logique donnée dans les notations préliminaires)

et de la même manière: ûei ( Ni Φ).Ι = (-, i.l) v def^*),! = i.l => detrt»).! Finalement on a :

def,( Ν _; Φ) = (i.i => def^).i, def _s (0).lb - i.lb, def,( ).ub - i.ub, i.u -> def-(O).u) Avec les notations introduites nous pouvons écrire plus simplement :

def (N, Φ) = def _K (<î>) J i

Exemple : posons def»^) = [2,6[. Alors :

def„( N^.5,1] Φ) = ((- 1 ) 1 , 2-(-0.5), 6 - 1 , 1 ) v 0)

= (1 , 2.5, 5, 0)

= P.5,5[

Détermination de : def _a (Bot Φ) et de eyTop Φ)

Sachant qu ^' un processus croît à droite, l'intervalle de définition d'une formule croît lui aussi à droite. La valeur de Top Φ ou de Bot Φ en

[def _s ( Φ).ι , def _re ( #).ub] n'est de fait pas certaine. Par exemple, en supposant que Φ soit vraie sur l'intervalle (I, Ib, def _K ( #).ub, def _n ( Φ).υ) et en supposant qu'un nouvel instantané I arrive déterminant que (selon le processus p.l) Φ devient fausse (ou prend une nouvelle valeur) sur (1- def.( Φ).υ, def^ 0).ub, ub, u), dans ce cas Bot Φ est vraie en [def-( Φ).u , def _K ( J.ub] ce qui ne pouvait être déterminé en def _r ( Φ).ub. De la même manière, on montre que la valeur de Top Φ n'est pas certaine en [def-( Φ).υ^ def-( OJ.ub], d'où def _n (Bot Φ) = def^Top Φ)= def,( Φ)[.

Détermination de i def _r (X^ Φ). La figure 5F permet de soutenir l'idée de son calcul. Sur cette figure le dernier instantané, disons Ι , attribue la valeur 16 à Φ. D'après la sémantique de X _[ri j la validité de X _[n j Φ (avec n = 2) peut être déterminée jusqu'à 1< ₎ .ί (ouvert) soit jusqu'à l _(k - < _n -D).t ouvert. Quand n est négatif, par exemple n = -1 , puisque Φ est définie à partir de π(0) il suit que X _[n i Φ est définie à partir de π(1 ) (soit π(-η)) puisque la liste de validité de X^ _j Φ s ^' obtient en décalant une fois à droite les valeurs des intervalles.

La généralisation de def _T à toutes tes expressions est donnée par la définition suivante :

• €ίβ¾(Φι, ... , „)) ~ def _» ( s) n ... n deL( _n ) où (Φι, ... , Φ _η ) est un n-uplet de termes • < ( ) = [(î£.first).t, (Tî.last).t] si Φ est purement booléenne ou bien un terme non décalé (Φ est une expression de Γ ou de E)

• de¾¥ _[a] Φ) = def„(#) Φ (-a)

• Φ) = [(Tî.first).t, (7t.(last-(n-1 ))).t [ si n > 0 où last est l'indice du dernier instantané de π

• def~(X _N Φ) = [π(-η)Λ, (n.last).t] si n < 0

• def^f^)) = βί _Π (Φ) où f est un symbole de fonction

• def^N; Φ) = de1 _n ( t») J i

• def _re (A{f}i Φ) = def,^) J i

· def _r (0^)) = άβί _π (Φ) où O est un symbole de prédicat

• def,(Top i>) = def _s ( )[

• de¾Top{ } ) = de¾ )[

» def,(Bot Φ) = def _n (0)[

» def^Bot^ O^ def^).

· def^, U _i+ Φ ) = ((def^ , )] n def^î> _: )) J i+) n (def^ , ))]

• def«( , S; . Φ. ) = ([(def^DO n def,(<ï> _: )) J rev(i+)) n [(def,( , ))

. n άβί _π (Φ ₂ )) J (k,-d,-d,k)) n

• deULW) = def,^ ⁾ )

D'après cette définition il est possible de montrer qu'étant donné un processus % seuls un nombre fini de dates doivent être mémorisées pour calculer def.. Nous avons en outre Tt.first.t et Tt.last.t et pour chaque sous- expressions de forme Χ[ _Π ] Φ un nombre fini de dates. Ces dernières peuvent être mémorisées clans une liste de validité (c'est pourquoi X _rn] Φ possède une sous-expression cachée qui est le couple (Γ,Φ)). Su le plan opérationnel le procédé n'aura donc pas besoin de stocker le processus π mais seulement un nombre fini de dates relatives à π. Algorithme de calcul de l'intervalle de définition

A chaque formule est associée un nouvel attribut de type intervalle. Pour la formule Φ cet intervalle est noté O.def. A l'initialisation du procédé, #,def est initialisé à l ^' intervalle vide (dénoté par nil ou 0).

Calcul de l'intervalle de définition basé sur la fonction deL :

Pour chaque rafraîchissement de l'instantané I (dont l'indice est k):

F1 ) Cas de base :

a. Si Φ est une proposition, un terme non décalé ou une formule purement booléenne .def devient [jt.first.t, l.t]

b. Si Φ est de la forme X _ln j Ψ. Par hypothèse (r, Ψ) est une sous- expression non décalée de Χ[ _Π ] Ψ dont l'intervalle de définition est donc [Ti.first.t, l.t]. On peut donc considérer établie la liste de validité de (r, Ψ) sur [n.first.t, l.t].

i. Si n >0 il suit que (X _[n] P).def = [π(0) , j.lb[ où j ^A (k-(n-1 ),s) est un intervalle de la liste de validité de (r, Ψ)

ii. Si n < 0 il suit que *F).def = [j.lb, l.t] où j ^A (-n,s) est un intervalle de la liste de validité de (r, Ψ)

F2) Induction ι Φ est un autre type de formule, on utilise la fonction def-.

Autre mode de calcul de l'intervalle de définition : par offset.

Selon un autre mode de réalisation (plus efficace) on pourra précalculer l'intervalle de définition en utilisant une logique d'offset par rapport à - first.t et n.last.t en utilisant des variantes la définition de def.,. Néanmoins ce mode de calcul n'est possible complètement que s'il n'existe aucune occurrence de l'opérateur dans les sous-expressions. Pour chaque formule Φ il s'agit de pré-calculer un quadruplet noté Φ.δ de fa môme forme qu'un intervalle (ainsi nous utiliserons les notations propres au intervalles pour cet attribut), de telle sorte qu'ensyîte, lors du fonctionnement, on ait toujours:

def* ( ) = (Φ.δ.Ι, K.fîrstt + #Jib, jt astt + Φ.δ-ub, Φ.δ-u). Si Φ est purement booléenne ou bien un terme non décalé, ce quadruplet est

(1 ,0,0, 1 ).

En effet (1 , Tt.first.t + 0, idast.t + 0, 1 ) = [Tt.first.t, Tt.last.t] = def, (Φ).

Pour calculer Φ δ dans le cas général on a besoin d'introduire des intersections particulières sur les intervalles. Ce sont n> et <n. L ^' intersection n> n ^' agit que les bornes supérieures tandis que <n n'agit que sur les bornes inférieures des intervalles. Les données non pertinentes seront remplacées par un point d'interrogation :

(?, ?,ub, , u n> ( ?, ?,ub ₂ , u ₂ ) = ( ?, ?,ub,u) où :

• u = inf(ui , u ₂ ) si ubi = ub ₂

( h, Ib, , ?, ?) <n ( l ₂ , lb ₂ , ?, ?) = ( I, Ib, ?, ?) où :

• l = inf(li , l ₂ ) si Ibi = lb ₂

Mode de calcul de l ^' offset :

Etant données ces définitions, pour calculer Φ.δ, il suffit d ^' utiliser deux variantes de la fonction def-.

• Dans la première variante, qui permet de calculer Φ δ.Ι et Φ δ Ib on posera :

o def*( E>} ⁼ (1 ,0, ?. ?) si Φ est purement booléenne ou bien un terme non décalé

o tes autres cas sont repris de def ^ en remplaçant partout n

par <n

» Dans la seconde variante, qui permet de calculer Φ.δ.ιΑ et Φ.δ.υ on posera : o defjr(#) = ( ?, ?,0, 1 ) si Φ est purement booléenne ou bien un terme non décalé

o les autres cas sont repris de def» en remplaçant partout n par n> .

Exemple i calculons Φ.δ pour Φ = (p Λ E[i _i2 i q) i

p.ô = (1 ,0,0, 1 ) = [0.0]

q-δ = [0,0]

E _n ,2i q = def,(q) J [1 ,2] = [0,0] J [1 ,2] = [-1 ,-2]

(Φ.δ.Ι, O.Ô.Ib, ?, ?) = [0,0] _< n [-1 ,-2] = (1 ,-1 , ?, ?)

(?, ?, Φ.δ-ub, Φ.δ.υ) = [0,0] n _> [-1 ,-2] = (?,?,-2, 1 )

En agrégeant (1 ,-1 , ?, ?) et (?,?,-2, 1 ) on obtient ;

Φ.δ = (1 ,-1 ,-2, 1 ).

Remarque : ce mode de calcul anticipé nous permet notamment de précalculer les deux fermetures de l'intervalle de définition.

Ces modes de réalisation du calcul de Φ.άβί étant posés on revient maintenant au principe de continuation que nous redéfinissons à partir du concept d'intervalle de définition.

Principe de continuation

Du principe de définition précédemment développé, découle le principe de continuation qui gouverne les algorithmes de calcul des listes de validité de proche en proche. Supposons que la liste de validité d'une formule Φ ait déjà été établie selon un processus π sur son intervalle de définition def _K (#).

Par définition ceci assure que la liste de validité de Φ sur def _s (#) ne peut être modifiée par la suite. La validité de Φ sur αβί-(Φ) est donc un résultat acquis qui ne doit plus être recalculé par la suite. Si donc arrive un nouvel instantané ! qui prolonge π en ie processus π · l le calcul des intervalles pour Φ ne doit porter que sur l ^' intervalle qui par définition de la fonction de définition représente la plus grande portion certaine mais non encore calculée du domaine de définition de Φ selon π · l Pour toute formule Φ cet intervalle sera stocké dans une variable de type intervalle attribuée à Φ que l'on notera Φ.νν et que l'on nommera fenêtre de continuation de Φ.

La fenêtre de continuation Φ.νν de Φ est ainsi une zone de certitude, qui n ^' empiète pas sur des zones déjà calculés, et qui au surplus ne contient que des dates qui dépendent du nouveau processus π · I prolongement de π.

Sur le plan calculatoire Φ.νν est la partie de l'intervalle de définition qui excède ce qu'il était lors de l'instantané précédent.

Algorithme de calcul de la continuation

Lors du rafraîchissement de la structure mémorisant l'instantané pour chaque formule Φ l'actualisation de Φ.νν se fait avant l ^' actualisation de Φ-def et répond donc aux étapes suivantes :

Exemple : Evolution des fenêtres de continuation avec pour principale Ερ. p suivant un processus dont les premiers instantanés ont pour dates 0.1 .2,3.

En l'absence d ^' expression de la forme Χ _[Γ1 ]Φ, le mode de calcul précédent peut aussi être complété, à des fins d ^' optimisation, par un second calcul plus rapide, dès lors que Φ.νν est non vide. E effet on peut facilement montrer que si Φ.νν- est la fenêtre de continuation de Φ calculée pour le processus π, alors la fenêtre de continuation Φ.νν,·-. de Φ calculée pour le prolongement π·Ι de π est :

(1 - (Φ.νν-).υ, ^.w^.ub, ^,sN _n ),ub + A, (Φ .) u) où Δ = (l.t - it.Iast.t).

En effet les fenêtres de continuation sont adjacentes, donc la borne supérieure devient la borne inférieure à l'instantané suivant (de fermeture inversée). Et la borne supérieure se voit augmentée de l'écart entre le nouvel instantané et le précédent. Selon ce mode de calcul les étapes sont alors :

Si Φ-w est vide :

• Φ.νν = def-^t>) \ Φ-def

• Φ-def = def _ît (#)

Si H'.w n'est pas vide :

• Poser k = Φ w

· Puis poser Φ.νν = (1 - k.u, k.ub, k.ub + Δ, k.u)

De sorte qu'à partir d'un certain stade, selon ce mode de calcul, il n'est plus nécessaire d'utiliser la fonction def, _T mais simplement l'écart entre

Δ la date courante et la date précédente.

Notion de zone d'influence

Cette notion intervient dans l'objet de l'invention, à deux titres i

• Elle définit, pour une formule Φ, quels intervalles des sous-formules de Φ ont une influence sur la fenêtre de continuation Φ.νν de Φ définie précédemment,

• Réciproquement, elle définit, pour une formule Φ, quels intervalles des sous-formules de Φ n'ont plus d'influence que sur la zone déjà certaine de Φ

• Ceci permet donc :

o D'optimiser le calcul en ligne des intervalles de validité, en ne ciblant que les intervalles qui influent sur la fenêtre de continuation. o De manière duale, ceci permettra de définir les intervalles qui ne peuvent plus avoir d ^' influence sur les fenêtres de continuation, et donc d'éliminer ces intervalles.

Analysons la zone d ^' influence pour la formule Ε,Φ. La figure 7 en est une illustration . Considérons la fenêtre de continuation (E, Φ).νν de E, Φ. La validité en t e (Ε, Φ).νν dépend des dates i ^' 0t de Φ En d'autres termes les dates qui influences la validité de (Ε, Φ) sur (Ε, Φ).νν sont données par l ^' union des intervalles i®t pour t e (E, Φ).νν. Or cette union n'est autre que :

((Ε, Φ).νν.Ι x i.l, (Ei #),w,lb + i.lb, (Ej #).w.ub + i.ub, (Ε, Φ).νν.υ x i.u). Ainsi, tout intervalle de Φ ayant une intersection non vide avec cet intervalle influence le calcul de E, Φ sur E, Φ.νν.

Considérons maintenant le calcul de Bot Φ sur (Bot Φ ι.νν. Supposons que Φ-LV contienne un intervalle i jouxtant (Bot Φ).νν à gauche. Alors, bien que d ^' intersection vide avec (Bot Φι.νν, il influence la validité de (Bot Φ) sur (Bot Φ).νν puisque précisément (Bot Φ) est vrai en [w.lb.w.lb]. Dans ce cas la condition pour qu ^' un intervalle i de Φ ait une influence sur le calcul de (Bot Φ) est que i] (fermeture à droite de i) ait une intersection non vide avec (Bot Φ).νν.

Ces idées peuvent être synthétisées sous la forme d'une fonction qui admet en arguments deux formules et qui renvoie un intervalle. Si Ψ est une formule sous-formule directe de Φ. ΖΙ(Ψ,Φ) est la plage temporelle de la liste de validité de Ψ à considérer dans le calcul de la continuation de Φ. Par plage temporelle nous entendons tout simplement un intervalle. Finalement nous dirons qu'un intervalle î de la liste de validité de Ψ a une influence sur la fenêtre de continuation de Φ si sa fermeture à droite i] (pour tenir compte de !a spécificité de Bot) à une intersection non vide avec ΖΙ(Ψ,Φ).

Conformément à ces analyses pour Ε,Φ on aura donc i + i.ub, (Εΐ Φ).νν.υ. x i.u). Pour simplifier l'écriture nous noterons i ΖΙ(Φ,Ε _ί Φ) = (w.lxi.l, w.lb + i.lb, w.ub + i.ub, w.u x i.u) où w dénote la fenêtre de l'argument gauche de la fonction ZI, soit Ε Φ ici.

Définition de la fonction ZI :

• ZliOi , (σι , ... , σ _η )) = w avec σ; e {σι , ..., σ _π }

· ΖΙ(σ, f(o)) = w

• ΖΙ(σ, Ο(σ)) = w

• ΖΙ(σ, V _[a] σ) = w Θ a

• ΖΙ(Φ,* Φ) = w avec * parmi -,, Top, Bot, Τορ{β}, Βοί{β}, L, ou un symbole de fonction ou de prédicat

· ΖΙ(Φ,Ν, Φ) = (w.lxi.l. w.lb + i.lb, w.ub + i. ub, w.uxi.u)

• ΖΙ(Φ,Α{τ}, Φ) - (w.lxi.l, w.lb + i.lb, w.ub + i.ub, w.uxi.u)

• ΖΙ(Φι , (Φι υ, ₊ Φ ₂ )) = (1 , w.lb + (i+).lb, w.ub + (i+). ub, 1 )

• ΖΙ(Φ ₂ , (Φι U,. Φ ₂ )) = (w.lx(i+).l, w.lb + (i+).lb, w.ub + (i+).ub, w.ux(i+).u)

• ΖΙ(Φι, (Φι S, ₊ Φ ₂ )) = (1 , w.lb - (i+).ub, w.ub - (i+).lb, 1 )

· ΖΙ(Φ ₂ , (Φι S _l+ Φ ₂ )) = (w.lx(i+).u, w.lb - (i+).ub, w.ub - (i+).lb, w.ux(i+).l)

• ΖΙ(Φ, , (Φ, S _(d,k) Φ ₂ )) = (1 , w.lb - d, w.ub - d, 1 )

• ΖΙ(Φ?, (Φ% Stf ) ®? )) - (w.lxk, w.lb - d, w.ub - d, w.uxk)

• ΖΙ(Φ, Β( _θ ,!< ₎ Φ) = (w.lxk, w.lb - e, w.ub - e, w.uxk)

Remarque 1 : en réalité les zones ΖΙ(Φι , (Φι U _l+ Φ ₂ )) et ΖΙ(Φι, (Φι S _i+ Φ ₂ )) ne sont pas vraiment utiles, comme l'atteste, pour les opérateurs Uj ₊ et S.+ , les exemples de réalisation du calcul de la continuation donnés en Annexe 1. De même cette notion n'est pas utile pour le calcul de X _in ] Φ.

Calcul en ligne, par continuation, des listes de validité

Le principe de la continuation en ligne est le suivant. Pour chaque formule le procédé ne produit de nouveaux intervalles que sur sa fenêtre propre de continuation Ces nouveaux intervalles sont calculés à partir des listes de validité des sous-formules, mais en ne considérant que les intervalles dont l'intersection est non vide avec la zone d'influence calculée au moyen de la fonction ZI . Ces restrictions étant faites, le calcul proprement dit est alors réalisé selon les principes du calcul hors ligne (ainsi que décrit dans la section "Correspondance entre opérateurs logiques et opérations sur les listes de validité"). Pour synthétiser : le calcul en ligne est une succession de calculs hors ligne locaux restreints pour chaque formule à sa fenêtre de continuation propre.

Remarque ; pour que ce calcul soit correct il est nécessaire que, pour toute formule, quelle que soit la zone d'influence qui lui est attribuée, celle-ci soit incluse dans sa zone de certitude propre, comme cela est illustré figure 7 (la zone d'influence pour Φ est bien dans sa zone de certitude). Or cela est toujours le cas. Ceci se démontre à partir des définitions des fonctions def^ et ZI.

Le calcul par continuation peut là encore être facilement illustré pour Ε Φ. Il s'agit de ne considérer que les intervalles de la liste de validité de Φ situés dans la zone d'influence calculée pour Ε Φ. Etant donné que ces intervalles ont plus de chance d'être à la fin de la liste de validité de Φ l'algorithme procède par marche arrière. Il remonte la liste de validité de Φ à partir de la fin jusqu'à déterminer le dernier et ie premier intervalle ayant une intersection non vide avec la zone d'influence. Ceci définit une sous liste de la liste de validité de Φ qui est exploitée selon l'algorithme hors ligne décrit plus haut pour le calcul de nouveaux intervalles de la liste de validité de Ε,Φ. Pour chaque production nous calculons son intersection avec la fenêtre de continuation Ε,Φ.νν de Ε,Φ. Si cette intersection n'est pas vide elle est adjointe à gauche dans une liste temporaire. Puis quand tous tes intervalles de la zone d'influence ont été parcourus, la liste temporaire est raccordée à la droite de (E Φ) LV (Voir l'Annexe 1 pour un calcul détaillé de E0),

Le principe de continuation présente néanmoins des particularités pour les opérateurs B _(e , _h) et S,¾,k ₎ . Pour une formule de type B _(e ,k ₎ Φ il suffit que Φ soit vraie une seule fois à une date t pour que B _(e , _k) Φ soit vraie sur (k ₍ t-e,«>,0). Le procédé peut donc être simplifié. Dès que Φ est vraie, c est-à- dire Φ.ί.ν possède un premier i, on créé l'intervalle (i.lxk, i.lb - e, ((B _(e, i _<) 0).w).ub _> ((B _(e , _k ) #),w).u) que l'on ajoute à la liste de validité vide de (B _(B , _k ) Φ: ensuite la borne supérieure de cet unique intervalle est réajustée à la borne supérieure de (B _{e,k ) #).w à chaque rafraîchissement, sans se préoccuper de la valeur de Φ. Pour S ₍ d _,k) , d ^' après la sémantique de cet opérateur, le procédé doit examiner la valeur de vérité de Φ ₂ arbitrairement loin dans le passé et donc aussi celle de Φ _Ί . Mais cette approche obligerait à conserver en mémoire tous les intervalles de Φ ₂ et de Φ,. De sorte que la mémoire requise par le moniteur pourrait croître indéfiniment. Or un des objectifs principaux de la présente invention est que la mémoire requise par le moniteur soit bornée. En réalité l'information que Φ ₂ a été vraie est conservée dans la liste de validité de ι S.d. _k) Φ ₂ · En effet, considérant le calcul de Φι S _{0X! Φ ₂ sur sa fenêtre de continuation, si le dernier intervalle de la liste de validité de Φι S _(d, k) Φ ₂ jouxte (Φι S _(d, k ₎ Φ ₂ ).νν alors cela signifie nécessairement qu ^' il a existé dans la ou les fenêtre(s) précédente(s) de continuation, un intervalle i de Φι ayant intersecté un intervalle de Φ ₂ dans le passé et qui se prolongeait continûment de sorte à couvrir chaque fois ces fenêtres de continuation. La mémoire que Φ _? a été vraie et que Φι l ^' est continûment depuis est donc contenue dans le rapport topologique du dernier intervalle de la liste de validité de Φι S ₍ d _, k ₎ Φ _? avec Φι S( _d , _k ) Φ ₂ νν : ils sont adjacents. C'est pourquoi nous serons en mesure d'éliminer les intervalles de Φ _? et de maintenir une mémoire bornée. Ceci sera vu plus loin avec la notion de date d ^' inutilité.

Pour synthétiser ce qui a été vu précédemment :

• Grâce à la fonction def~ nous sommes en mesure de délimiter, pour chaque formule :

o une plage temporelle ou la validité est certaine

o une plage temporelle jouxtant la plage certaine, appelée fenêtre de continuation, qui limite la plage de calcul à effectuer chaque fois que l'instantané est rafraîchi

• Grâce à la fonction ZI. nous sommes en mesure, quand nous effectuons le calcul de nouveaux intervalles de validité sur la fenêtre de la continuation, de restreindre, au sein des listes de validité des sous-formules, les intervalles à prendre en compte pour ce calcul. Elimination des intervalles inutiles (limites d'inutilité et dates d'inutilité)

Il a été exposé ci-dessus comment calculer la liste de validité de la formule principale. Ce calcul repose sur le calcul préalable des listes de validité de toutes ses sous-formules. Ce calcul sur les sous-formules apparaît donc comme un moyen nécessaire au procédé mais non comme une fin en soi puisque seule la liste de validité de la formule principale est déterminante pour le procédé (car c'est la non vacuité de cette liste qui témoigne de l'occurrence du comportement redouté).

Nous avons également la valeur d'une expression qui peut être déterminée de façon certaine jusqu'à une certaine limite donnée par la borne supérieure de son intervalle de définition. Supposons que le procédé ait terminé les calculs des listes de validité et soit attente d ^' un nouvel instantané. Supposons que la liste p.LV de la formule principale Φ soit toujours vide ou bien que les intervalles calculés aient déjà été exploités (pour l ^' écriture d ^' un rapport ou l ^' émission d'un signal). Il est donc clair que les intervalles des listes de validité des sous-expressions de Φ qui n ^' ont d'influence que sur O.def ne pourront plus contribuer à générer d ^' autres intervalles à exploiter pour Φ sur O.def car sur Φ.άβί la valeur de Φ est désormais certaine (de par la définition de O.def). Ces intervalles sont donc devenus inutiles vis-à-vis de la problématique d ^' ensemble que est de déterminer si Φ est vraie à un moment donné et d ^' exploiter cette information. Nous pouvons donc les éliminer de la mémoire de la machine qui réalise le procédé. C'est ce mécanisme qui permet notamment de garantir que la ressource mémoire requise par le moniteur est bornée assurant de ce fait le fonctionnement sans limite de durée du moniteur généré par le procédé.

Pour connaître exactement les intervalles à éliminer dans les sous expressions de la principale, il faut être capable de déterminer, pour chacune d'elle, en deçà de quelle limite les intervalles sont devenus inutiles. Nous allons donc établir, pour chaque sous- expression Ψ de la formule principale Φ, un couple de la forme (ub,u) de ¾x{0, 1 }, appelé limite d'inutilité relative de Ψ et notée H'.reMi, de telle sorte qu'on puisse éliminer, sans nuire à la détection du comportement redouté, tout intervalle i de la liste de validité de Ψ s'il est tel que (i.ub, Lu) (dvdef.ub + ub, u) où est le prédicat défini ainsi : (ubi, Ui ) (ub _? , ι- ) si et seulement si ub, < ub ₂ ou bien si ubi = ub ₂ et Ui < U2. Le couple ( .def.ub + ub, u) est appelé limite d'inutilité absolue de Ψ et est notée ¥.absji. Au final, pour Ψ une sous-expression de la principale Φ nous avons :

.absji = (O.def.ub + OF.relJ .ub, (¥.relji),u)

Remarque i un intervalle ayant pour limite supérieure la limite absolue d'inutilité ne doit pas être éliminé puisqu'il est susceptible d'être prolongé lors d'un nouvel instantané. Or ceci est bien garanti par notre critère d'élimination et le prédicat .

Conformément à ce que nous avons dit précédemment pour la formule principale Φ, .absji = (<J .def.ub, O.def.u). Ceci implique donc que O. reIJi = (0, O.def.u).

Le cas de la conjonction est particulièrement intuitif (Figure 8). Dans cette figure considérons les intervalles de Φι et de Φ ₂ . D'après leurs positions ils ne peuvent contribuer à former des intervalles de validité pour (Φι Λ Φ ₂ ) sur (Φι Λ 2).def. Désormais ils sont donc inutiles pour décider de la validité de (Φι Λ Φ ). H en serait de même de tout autre intervalle antérieur à la limite supérieure de (Φ , Λ 0 ₂ ).def. Autrement dit, si (Φι Λ 02).abs_li est la limite d'inutilité absolue de (Φι A Φ ₂ ) alors la limite d'inutilité absolue de Φ. et de #2 est aussi (Φι Λ 0 ₂ ).abs_li. Cependant, si (Φ . Λ Φ ) n'est pas la formule principale, il se peut que Φ ·, et Φ soient aussi sous-formules d'autres formules. Il se peut donc que d'autres formules leurs imposent une limite d'inutilité antérieure à (Φι Λ #2).abs_li. Ainsi, ce qui peut être affirmé à partir de (€>i Λ #a) et de sa limite d'inutilité (Φ-, Λ # ₂ ).abs_Ii est que les limites d'inutilité de Φι et de Φ ₂ doivent être antérieures ou égales à (Φι Λ # ₂ ).absji. Une généralisation de ceci à toutes les formules du langage est explicitée ci- après.

Pour généraliser ce principe à toutes les expressions du langage, nous définissons un système de contraintes sur fonction appelée Ll, qui doivent toutes être satisfaites pour que cette fonction Ll soit une fonction d ^' inutilité exploitable par le procédé. Cette définition fait appelle au prédicat entre deux limites. On a (ubi , Ui ) <- (ub ₂ , Ua) si et seulement si : ou bien

Cette fonction d ^' inutilité prend en argument une formule Φ _π supposée être une sous-expression d ^' une formule principale Φ, et renvoi une limite relative Ι_Ι(Φ _η ) de la forme (ub _n , u _n ), de telle sorte que la limite absolue d ^' inutilité de Φ _η soit ( .def.ub + ub _n , u _n ). Ll nous permet de calculer un offset par rapport à la limite d'inutilité de la principale.

Etant donnée une formule principale Φ et l'ensemble {Φι , ... , Φ _π } de ses sous-expressions une fonction Ll de {Φι , ... , Φ _π , Φ}→ (9vx{0, 1 }) est une fonction d ^' inutilité si elle satisfait des contraintes de la forme LI(H') = Ll(#) où Ψ et Φ sont toutes les deux des sous-expressions de la principale Φ et où Ψ est une sous-expression directe de Φ. Ces contraintes sont les suivantes :

» ΙΙ(Φ) - (0, u) où u est la fermeture de l ^' intervalle de définition de Φ.

Et pour i,j e [1 ,n]

• ίΙ(Φ ^, ) ~ Ll(* Φ,) où * parmi ~ Top, Bot, Τορ{β}, Βοίίβ}, L, ou un symbole de fonction ou de prédicat

• U(#i) Lf((#i Φ„)) où (Φ-ι , ... , Φ _η ) est n-uplet de termes

• Ll( i) « = ((U(¥ _t ai i)).ub + a, (LI(V _[a] Φί)).υ)

• Ll( i) ((LI(N _k #i)).ub + k.lb, k.l => (LI(N _k #i)).u)

• Ll(#i) ((Ll(#i Uc j)).ub + (i+)Jb, (i+) .I => (LI(#Ï U,* #j)),u)

· Li( ₎ ) ((υ(Φί U* #j)).ub + (i+)Jb, (!+). ï => (LÎ( _T U _i+ Φ,)).υ) • ϋ(Φ,) ((Ll(#i S _i+ #j),ub) - (i+).ub, (i+).u => (LI(O _f S _i+ #j),u) )

• Ll(<£» _j ) = ((Ll( i S, ₊ #j),ub) - (i+).ub, (i+).u => (Li(O _s S _i+ Oj).u) )

• Ll( i) ^« « = ((LI(Oi S _(d .k, j)).ub - d. k ..> Li(0 S _(d , _k) Φ,). ι.)

• Ll(O _j ) ^< « = ((1_Ι(Φ| S _(d , _k) j)),ub - d, k > ϋ(Φ, S _(d , _k) Oj).u)

· ίΙ(Φι) ^« «= (LI(B _{e , _k) 0.).ub - e. k L!(B _(e , _k) Φ ).ϋ)

« ίΙ(Φί) <« = ((LI(A{f} _k Oj)).ub + k.lb, k.l ::.-> (Li(A{f} _k Oj)).u)

• ίΙ(Γ,Φ ) ^= (ζ, 1 ) où ζ satisfait les conditions suivantes:

o avec j ^A (k,v) le plus grand (selon l'ordre sur les intervalles) intervalle de (r, j).LV tel que (0,

LI(X{g}[ _n, m _] i).u) Π j ≠ 0, autrement dit l ^' intervalle contenant

LI(X{g}[ _n _ _m ] i) est de rang k, issu du k ^ieme instantané, alors:

^■ Si n < 0 et qu'il existe h ^A (k-n.v ) e (r,Oi).LV,h est un intervalle de rang k-n, alors z = h.lb

^■ Si n > 0, z = j.lb

o z = def(Oi).lb dans les autres cas X{g} _{|n m} ] Φ, demande encore une conservation totale de (Γ,Φ,) et donc de _;

Exemple : Supposons que l'ensemble de contraintes qui pèsent sur l'expression Ερ^ p soient :

LI(E _{t1 ,2(} p) ^ = ( 1 0.0).

LI(E ₍₁ , _2[ p) ^ = (9, 1 ).

On pourra choisir : (E[ _{1 i2} [ p).relji = (9, 1 ) soit la plus grande limite permise par la contrainte la plus forte. Par ailleurs la fonction Ll devra donc aussi satisfaire cette contrainte : Ll(p) (9+1 , 1 => 1 ) soit Ll(p) = (10,1 ).

Remarque : pour une expression Ψ considérée le choix de Ψ.ΓΘΜΪ qui élimine le plus grand nombre d'intervalles possibles est celui qui attribue àF.reMi la limite de la contrainte la plus forte.

Remarque : si l'opérateur X[ _f , _j n ^' est pas présent dans Ses sous-expressions la limite d'inutilité peut être pré-calcuiée â ï'avance et une fois pour toute. En effet pour tous les autres opérateurs la définition de Ll ne réfère qu ^' aux valeurs de leurs intervalles de portée. A contrario la définition de Ll impliquant X _[nJ réfère à une liste de validité. Si cet opérateur est présent, comme les contraintes qu'il impose varient en fonction du processus il faut donc refaire le calcul de Ll à chaque rafraîchissement (du moins pour les sous-expressions de X _[n j).

Un mode de calcul possible de la limite d ^' inutilité relative

Ci-dessous on présente un mode de calcul possible de la limite relative d'inutilité de chaque sous-formule de la formule principale.

1. Pour chaque sous-formule Ψ de la principale Φ (y compris Φ elle- même) créer une variable de type limite Ψ.ΓΘΜΪ et lui assigner la limite symbolique (∞,0) ((∞,0) est telle que z <= (<*>,()) est toujours vraie pour une limite z standard)

2. Assigner (0, Φ.δ.υ) à .rel ji

3. Appel de calculji( , O.reIJi) où calcul rel li est l'algorithme récursif présenté ci-dessous.

calcul_rel_di^,lim) :

D1 - Si lim = O.reIJi alors Φ. ΓΘΜΪ = lim

D2 - Pour chaque sous-formule Φ, de Φ calculer sa limite relative lirrii en appliquant la définition de la fonction Ll et appeler calcul rel di^Jim.)

Etant donné ce mode de calcul, pour toute sous-formule Ψ de la formule principale Φ, il est possible de calculer sa limite absolue d'inutilité propre, notée ¥,absji :

Ψ-abs li = ( J>.abs_li.ub + ¥.reIJLub, Ψ.ΓΘΜΪ.ΙΙ)

Remarque i la date d'inutilité de la demande de brevet WO201 0/0261 50 est une version dégradée de la limite d'inutilité, La date d'inutilité s'obtient en ne gardant de la limite que la valeur, c'est-à-dire en ignorant la fermeture associée. D'où que, dans cette demande, l'élimination consistait â éliminer les intervalles strictement inférieurs à cette date. Dans ce cas dégradé la date d'inutilité d'une formule Ψ est noté Ψ abs di et elle vaut (Ψ abs li).ub. Le mécanisme d'élimination des intervalles inutiles qui vient d'être décrit peut parfaitement être combiné au mécanisme de calcul par continuation décrit plus haut. Il sera appelé après achèvement du calcul de la continuation. Nous obtenons ainsi un procédé qui non seulement ne fait pas de calculs redondants mais aussi élimine les intervalles inutiles au fur et à mesure. Algorithme général du procédé

• définir des variables caractéristiques du système à surveiller {x-t, ...

Xm},

• définir un certain nombre de propositions { i, p _n } sur ces variables,

• allouer en mémoire du détecteur un espace suffisant pour mémoriser un instantané relatif à ces propositions et à ces variables c ^' est-à-dire allouer pour le temps une variable réelle notée l.t, pour chaque proposition p une variable l.p et pour chaque variable de signal x une variable l.x

• allouer les variables réelles, ît.first.t et n.last.t pour stocker la date du premier et du dernier instantané

• définir une formule principale Φ,

• pour chaque sous-expression Ψ de Φ (y compris Φ elle-même), créer une variable notée M'.LV de type liste d'intervalles, et l'initialiser à vide,

• pour toute sous-formule Ψ de Φ (y compris Φ elle-même) créer une variable booléenne ¥.val, et l'initialiser à 0,

• pour chaque sous-expression Ψ de Φ (y compris Φ elle-même) créer une variable notée '.w de type intervalle, appelée fenêtre de continuation de Ψ et l'initialiser à vide

• pour chaque sous-expression Ψ de Φ (y compris Φ elle-même) créer une variable notée Ψ def de type intervalle, appelée intervalle de définition de Ψ et l'initialiser à vide

« de façon régulière ou périodique faire l'acquisition de la valeur des variables caractéristiques du système observé et de la date courante et rafraîchir l ^' instantané I en fonction de cette acquisition, • Au premier rafraîchissement de l ^' instantané I assigner l.t à n.first.t

• pour chaque rafraîchissement de l'instantané (y compris le premier), assigner l.t à jt.last.t, et pour chaque sous-expression Ψ de Φ (y compris Φ elle-même), et selon un ordre qui soit tel que toute formule soit traitée après ses sous-expressions directes,

o Actualiser sa variable P.def et sa fenêtre de continuation Ψ.νν selon les étapes :

■ M'.w = def,( ) \ M .def

^■ .def = def^P) o effectuer le calcul de la continuation c'est-à-dire calculer de nouveaux intervalles de validité pour Ψ sur sa fenêtre de continuation M'.w (en exploitant éventuellement ZI pour limiter le parcours des listes de validité des sous-formules aux plages temporelles pertinentes)

o exploiter les informations contenues dans la liste de validité de la formule principale Φ et émettre un signal associé. o De façon optionnelle (pour limiter la consommation mémoire) calculer M'.abs li et éliminer de M'.LV les intervalles i tels que \ M'.abs_ li

o Attendre un nouveau rafraîchissement de l'instantané Méthodologie générale d'utilisation du procédé

Le procédé permet de détecter l'occurrence d'un comportement redouté exprimé dans son langage d'entrée tel que détaillé ci-avant. Le procédé permet notamment de générer automatiquement un détecteur à mémoire bornée adapté à signaler par ia génération d'un signa! représentatif toute occurrence du comportement redoute d'un système en fonctionnement La génération de ce détecteur fera appel à la mise en œuvre d ^' étapes préalables mises en œuvre par un utilisateur, notamment la définition des variables caractéristiques du système à surveiller et/ou de propositions sur ces variables. Pour exprimer un comportement redouté deux approches sont possibles.

• Soit l'utilisateur exprime directement un comportement Φ redouté.

* Soit au contraire il exprime d'abord une propriété Ψ attendue du système (un invariant qui doit être vrai tout le temps) et dans ce cas le comportement redouté à analyser sera Φ = ~ιΨ.

Dans l'exemple qui suit immédiatement nous optons pour la seconde approche qui consiste à exprimer d'abord une propriété attendue. Analyse simultanée de plusieurs principales

Le procédé peut être directement étendu pour analyser simultanément et en parallèle plusieurs formules principales Φι , ..., Φ _η . Tout se passe comme s'il s'agissait d'analyser une formule virtuelle constituée de l'ensemble { Φι , ..., Φ,, } de ces formules. L'ensemble des sous-expressions de cet ensemble est naturellement l'union des sous-expressions de chacune des principales. La hauteur de cet ensemble est la hauteur du plus grand élément de {η(Φι), ..., η(Φ _η )}. Ainsi pour le calcul basé ordonné par la hauteur des expressions on fera le calcul de la hauteur 0 jusqu'à la hauteur sup{h( ₁ ), ..., η(Φ _η )} _. Lors du calcul des listes de validité on pourra tirer partie du fait que certaines sous-expressions sont partagées ; si Ψ est partagée par Φ et Φ. le calcul de la liste de validité effectué pour Φ, n'est donc pas à refaire pour Φ,. La seule adaptation véritable concerne le calcul de la limite d'inutilité. Si Ψ est une sous-expression de plusieurs principales Φ _: , .. , Φκ on cumulera sur Ll(¥) l'ensemble des contraintes venant de Φ, , .... Opérateurs étendus, exemple décrit en relation avec ia figure 5G.

Tout en conservant la possibilité de générer des moniteurs à mémoire bornée, le langage précédemment défini peut être enrichi d'opérateurs dits étendus. Ceux-ci nécessitent la définition préalable suivante : une fonction d'agrégation est une fonction qui possède deux entrées (l'une étant appelée un agrégat et l'autre une donnée), et une sortie qui est un agrégat. Un agrégat peut notamment être l'objet vide noté 0. Par convention l'agrégat sera le second argument de la fonction, la donnée le premier. Par exempte la fonction notée « sup » est une fonction d'agrégation : sup(8, 0) = 8, sup(10.8) = 10, sup(6.10) = 10. On aura donc sup(6,sup(10.sup(8, 0))) = 10.

Comme on voit une fonction d'agrégation peut être appliquée à son propre résultat un nombre arbitraire de fois. Autre exemple : la moyenne pondérée que l'on notera « average ». L'agrégat est ici un couple (valeur, poids) :

average(8, 0) = (8, 1 )

average(10, (8, 1 )) = (9,2) .. (10x1 +8x1 )/(1 +1 ), donc de poids 2

average(6, (9,2)) = (8,3) ... (6x1 +9x2)/(2+1 ) = 8, donc de poids 3

Donc average(6, average(10, average(8, 0))) = (8,3).

L'adjonction selon une fonction d'agrégation f d'un intervalle i ^A v dans une liste L d'intervalles valués par des agrégats est une généralisation de l ^' adjonction avec compteur. Si j ^A a de L est tel que j c i, on le remplace par j ^A f(v,a). Si j ^A a est partiellement couvert par i ^A v, il est remplacé par deux intervalles qui sont (jni) ^A f(v,a) et (jHC(i)) ^A a (où C(i) désigne le complémentaire de i dans les réels). Si L possède des interstices, ils sont considérés comme des intervalles dont la valuation est 0.

Le langage peut être étendu par les opérateurs suivants :

• A{f}i Φ où f est une fonction d'agrégation et i un intervalle. Si à la date t, si {ji ^A Vi , ... j _n ^A v _n } est la sous-liste de validité constituée par l ^' ensemble des intervalles de Φ touchés par i © t alors la valeur du terme Α{ί¾ Φ est f(v _n , ...f(V2,f(vi,0)}), c'est-à-dire l'agrégation selon f des valeurs 0,vi v„ et dans cet ordre. Αίί¾ Φ est appelée une agrégation de Φ selon f.

• Χ{%νη] Φ avec Φ non décalée, n et m des entiers tels que n < m, f une fonction d ^' agrégation Si i est le k ^ieme intervalle de Φ et que k+n et k+m sont des entiers positifs alors, alors en supposant que {jk+ _n ^A i , ... j _k .,. _ri ^« v _n+m+1 } sont les intervalles de Φ de rang k+n à k+m, la valeur de X{f}[n,m] en toute date t de i est f(v _n +m+i , . , .f(v ₂ ,f(vi ,0))). C'est une agrégation discrète. On peut remarque que X[n] est équivalent à X{ :=}[n,n] où « := » désigne la fonction d'agrégation « assignation »,

* Τορ{β} Φ où β est un du même type que Φ. Même sémantique que Top mais en faisant l'hypothèse que Φ est initialisée par β. Ainsi

Top{0} p est vraie sur [def(p),lb, def(p).lb] si la proposition p est vraie en def(p).lb.

* Bot {β} Φ où β est un du même type que Φ, Même sémantique que Bot mais en faisant l'hypothèse que Φ est initialisée par β. Ainsi par exemple Bot{8} x vaut 8 sur [def(x).lb,def(x).lb] si le signal x vaut 7 en def(p).lb, ou bien n'est pas défini si le signal x vaut aussi 8 en def(p).lb.

* Ι_(Φ). Cet opérateur est intiment lié au procédé lui-même. Si i est un intervalle de Φ alors Ι_(Φ) contiendra l'intervalle i ^A (i,ub - ï.lb) c ^' est-à- dire i muni de sa longueur comme valeur.

Mode de calculs possibles:

Cas de X{g} _[n ,m] σ

Si i _k est un intervalle de (r,o) (qui est une sous-formule de X{g}[ _n ,m]), donc de valeur (k,v _k ), et que i _k+r , ^A (k+n,v _n ) et i _k+m ^A (k+m,v _m ) sont aussi définis alors on adjoint j ^A v à la liste de X{g}[n, _m j Φ où j = i et v est l'agrégation des valeurs r„¥ i , v _m données par i _k+n ^A (k+n,v _n ) ... i _k+m ^A (k+m,v _m ).

Cas de A{g}, σ

On parcoure la liste de σ dans l'ordre chronologique. Si j ^A v est un intervalle de σ alors on pratique l'adjonction par agrégation de (j®i) ^A v à la liste de A{g} σ, supposée être initialisée à vide (ou de façon équivalente par un unique intervalle qui est son intervalle de définition assorti de la valeur vide).

Cas de L(#)

Evident d'après la sémantique de L, · ûeUA{g}i Φ) = de¾#) j i • def _E (X{g} _In , _m] Φ) :

o si m < 0 vaut [i _n+ i ,lb, π-last.t] si i _n+1 le (n+1 ) ^,ème intervalle de

(r, Φ) existe, vaut vide sinon,

o si n > 0 vaut (1 ,7t.first.t, i _m+1 .ub, i _m+ i.u) si i _m+ i le (n+1 )' ^eme intervalle de (r, Φ) existe, vide sinon

o sinon vaut (1 , i _n+ i .lb, i _s .ub, i _s .u) si, avec s tel que s+m = last (numéro du dernier instantané de π), i _n+1 et i _s existent, vide sinon

• def„(Bot {β} Φ) = def,(Bot Φ)

· def^Top {β} Φ) = def„(Top Φ)

. deUim) = de¾#)

Zone d'influence

La zone d'influence pour A{f}, est la même que celle pour N, , celle de Ι_(Φ) identique à !(Φ) celles de Top {β} et Bot {β} respectivement indentiques à Top et Bot. Pour X{f}[n, m] elle n'est pas définie car le mode de calcul peut d'en affranchir.

Limite d'inutilité

• ϋ(Φ,) = ((LI(A{f} _k i)).ub + k.lb, k.l => (LI(A{f} _k Φ,))Μ)

• 1\(Φ,) < = Ll(* Φ ) où * est parmi Τορ{β}, Bot{p}

· Ll(r,#i) = (z, 1 ) où z satisfait les conditions suivantes:

o avec j ^A (k,v) le plus grand (selon l'ordre sur les intervalles) intervalle de (r,#j).LV tel que (0, LI(X{g}[ _nim] i).ub, LI(X{g}[n,rr,j#î).u) Π j ≠ 0, autrement dit l'intervalle contenant LI{X{gjf _r , _i?î ,j«l»î) est de rang k (issu du k' ^eme instantané) alors i ■ Si n < 0 et qu'il existe h ^A (k-n,v')€ (r _f #î).LV (h est un intervalle de rang k-n), alors z = h.lb ■ S» n > 0, z = j.lb

o z = def(#i).lb dans les autres cas (X{g}fn,m i demande encore une conservation totale de (τ,Φύ et donc de 4>,} Exemple d'application du procédé pour la surveillance d'un système de fermeture automatique de portes

Un système de fermeture automatique de portes d'un véhicule doit satisfaire à l'exigence que, chacune de ses portes doit être fermée dans les deux secondes qui suivent le dépassement de la vitesse de 5 kilomètres/heure par le véhicule. Nous supposons que chaque porte d'indice k est équipée d'un capteur Door k Locked qui vaut 1 quand la porte k est fermée et verrouillée, et qui vaut 0 sinon. En supposons que speed_exceed_5 dénote la proposition (speed > 5) pour chaque porte l'exigence peut donc être écrite ainsi :

speed exceed 5→ Ep,2i Door k Locked

Ce qui est redouté est donc exprimé par :

(speed exceed 5→ Ερ,2] Door k_Locked)

Analysons la validité de cette formule compte tenu du processus décrit par le tableau ci-dessous :

Dans cet exemple nous utiliserons la date d'inutilité (abs di), version dégradée de la limite d'inutilité (absjî). Les tableaux ci-dessous décrivent, en fonction des instantanés, l'évolution de certains attributs utiles à la compréhension du procédé, et ce pour chaque sous-expression du comportement redoutés. O ne n'intéresse qu'à la porte d'indice k. Instantané 0: date 0, speed = 0, Φ-def Φ w Φ LV .abs di vitesse _excède_5 [0,0] [O,O]\0= [0,0] 0 ?

Porte_k Fermée [0,0] [O,O]\0= [0,0] [0,0] ?

E _[0 ,2] Porte k_Fermée [0,-21=0 0\0= 0 0 ?

(vitesse_ excède .5 ->E _{0 2:} [Û,-2]=0 0\0= 0 0 ? Porte_k Fermée)

!{ vitesse_excède__5_5 → E _[0 ,2] [O,-2]=0 0\0= 0 0 ? Porte_k_ Fermée)

Instantané 2, date 1.1 Φ-def Φ.νν Φ- LV 0.abs_di speed = 3

vitesse excède 5 [0.1.1] ]Û,1.1] 0 ?

Porte k_ Fermée [0,1.1] jo.1.1] [0,0.1 [ ?

Ep,2i Porte_k_Fermée [0,-1.9]=0 0\0= 0 0 ?

(vitesse_excède _5) ~- Ε _[0ι 2ΐ [0,-1.9]=0 0 ?

Porte_k_Fermée)

! (vitesse_excède_5→ Ep,¾ [0,-1 ,9]=0 0\0= ø ¹ 0 ?

Porte k Fermée) Instantané 3, date 2, .def Φ w O.LV O.abs di speed = 7

vitesse_excède_5 [0,2] ]1.1 , 2] [2,2] 0

Porte k Fermée [0,2] ]1.1 , 2] [0,0, 1[ 0

E[o,2] Porte k Fermée [0,0] [0,0] [0,0] ^* 0

\0=[O,O]

vitesse excède 5 > Ep.q [0,0] [0,0] [0,0] ^** 0

Porte k Fermée

! (vitesse excède 5- E[ ₀ ,2j [0,0] [0,0] 0 0

Porte k Fermée)

* On a adjoint [-2,0.1 [ n [0,0] soit [0,0]

** (vitesse excède_5 + E _[ o,2j Porte_k_Fermée) est de la forme (a→ b) qui est équivalente à (-.a v b). Quand a est faux alors—a et vrai et donc ( -.a v b) l'est aussi. Comme vitesse_excède_5 est fausse sur [0,0] il suit que -, vitesse excède 5 est vraie sur [0,0] et donc de même de (vitesse excède 5v Ep.q Porte k Fermée).

Instantané 3, date 2.8, O.def Φ.νν Φ-LV Φ-abs di speed = 4

vitesse excède s [0,2,8] ]2,2.8] [2,2.8[ 0,8

Porte k Fermée [0,2,8] ]2,2,8] [0,0, 1[ ^* 0.8

E[o,2] Porte k Fermée [0,0,8] [0,0,8]\[0,0] [0,0,1]* 0.8

=]0,0.8]

vitesse excède 5- Ep _,2 i [0,0.8] ]0,0.8] [0, 0.8] 0.8 Porte k Fermée

! (vitesse_excède_5→ E _f0 ,2i [0,0.8] JO.0.8] 0 0.8 Porte_k_Fermée) ^* On remarque que pour Porte_k_Fermée et E _(0, 2i Porte_k_Fermée les intervalles de validité [0,0.1 [ sont strictement inférieurs aux dates d'inutilité de ces formules ; nous pouvons donc les éliminer de leurs listes de. Ainsi ils disparaissent dans le tableau du prochain instantané.

A cette étape un intervalle est créé dans la liste de formule principale, signifiant ainsi que le comportement redouté qu'elle modélise s'est produit. Une alarme peut donc être déclenchée pour signifier ce dysfonctionnement.

Application du procédé aux systèmes synchrones

Les systèmes synchrones sont des systèmes dont le changement d'état est cadencé par une horloge. Leurs changements d'états se produisent lors de chaque « tic » de cette horloge. Dans ce cas de figure on peut fixer par convention que le temps entre deux tics vaut 1 et que le premier tic est de date 0. Ainsi les dates portées par les instantanés seront des entiers. Dès lors, dans (es intervalles de portée des opérateurs du langage, on ne mettra que des entiers relatifs ; ces entiers ne dénoteront plus des décalages dans les réels mais des décalages en nombre de tics. Par exemple, dans le contexte synchrone, E _[ i. _3! p sera vraie en t (où t est un entier) si p est vraie entre 1 tic et 3 tics après t.

Exemple d'application du procédé pour le diagnostique embarqué.

Dans cet exemple le procédé selon l ^' invention est embarqué dans un contrôleur afin de surveiller qu ^' un signal reçu SigSys en entrée est conforme au signal de référence SigMod obtenu avec un modèle embarqué par le contrôleur. La notion de conformité est formalisée par une formule du langage.

Etant la fonction valeur absolue abs(abs(x) = x si x > 0 et abs(x) = -x sinon) les propositions sont:

seuiH pour abs(SigMod - SigSys) < 0.1

seuil2 pour abs(SigMod - SigSys) < 0.3

check pour (SigSys < 0.48)

La conformité est modélisée par la formule suivante:

seuil2 Λ E[ _0, 2.5] seuill

qui signifie : «en toute date on veut que seuil2 soit satisfait et que le seuiH soit satisfait dans les 2 secondes qui suivent» autrement dit on ne veut pas que abs(SigMod - SigSys) > 0.3 ni avoir abs(Sig od - SigSys) > 0.1 satisfait pendant plus de 2 secondes.

Variante (plus faible). On ne souhaite cette conformité que lorsque check est vraie depuis au moins 0.5 seconde:

(G[-o.5,oj check)→ (seuil2 Λ E| ₀ ,2.5] seuil 1 )

Autres exemples de formules:

(p→ E[4,4] P) « p est de période 4 »

(p→ E[4,4] p) A p) « p est strictement de période 4 (exactement

1 passage à vrai sur toute période de longueur 4 ouverte) » (Top p) >((-(Bot p))U[3,3 _] Bot p) « quand p devient vraie elle reste vraie jusqu'au troisième tic où elle repasse à faux » Top{<4}[0,5] p « densité de p : p survient au plus 3 fois sur une période de longueur 5 » p Λ E[_o.5,o.5] q « q est dans le voisinage de p à +/- 0,5 près » Les figures 9A et 9B représentent deux signaux dont on veut étudier la corrélation avec le prototype au sens de l ^' exemple détaillé ci- dessus. La figure 9A représente en jaune le signal selon le modèle de référence et en violet le signal du système acquis au moyen d'une carte d ^' acquisition. L'écart en valeur absolue entre les deux signau est donné en figure 9B. Le système a été instrumenté selon la figure 9C pour pouvoir envoyer les données à l'analyse par le prototype appelé « MONITEUR » dans cette figure.

Annexe 1

Notations :

« Nil » intervient pour dénoter des objets vides ou non définis (listes vides, intervalles vides. , .)

O.LV : pour liste de validité de Φ (listes d'intervalles disjoints rangés de façon croissante)

Φ. LV.fi rst et O.LV.Iast dénotent respectivement le premier et le dernier élément de O.LV (sont tous deux Nil lorsque O.L est vide)

Pour un intervalle deux notations sont utilisées:

la notation usuelle telle: ]4.32, 6.21]

la notation sous forme de quadruplet (I, Ib, ub , u) où:

I et u sont éléments de {0,1} qui dénotent l'ouverture ou la fermeture de l'intervalle sur les bornes Ib et ub

Ib : borne inférieure

ub: borne supérieure

exemple : (0, 4,32, 8.21 , 1 ) représente ]4,32, 6.21] si i est un intervalle alors t.l, i.lb, i.ub et Lu dénotent les paramètres ci-dessus mentionnés

Soit i un intervalle d'une liste de validité LV :

i.pred dénote son prédécesseur dans LV (Nil si i est premier élément)

i.next dénote l'intervalle suivant dans LV (Nil si i est dernier élément) Pour une expression donnée, la plupart des algorithmes de continuation donnés ci-dessous ont une structure commune :

• Initialisation des itérateurs en fin des listes de validité des sous- expressions

• Parcours des listes de validité des sous-expressions avec ces itérateurs dans le sens anti-chronologique (de la fin vers le début)

• Test de la position de ces itérateurs par rapport à la zone d ^' influence o si hors influence saut à l'étape de raccordement du Buffer à la liste de validité

o si dans la zone d'influence production de nouveaux intervalles dans Buffer

* Raccordement du Buffer à la liste de validité de la formule calculée • FIN

Dans tous les algorithmes, Buffer est une liste d'intervalles initialisée à la liste vide.

Calcul de Φ = :

1. iter = M'.LV.Iast, virtual = (1 - O.w.u, O.w.ub, < .w.ub + 1 , 1 )

2. Si iter n'est pas Nil faire :

a. Si iter < virtual faire :

i. assigner iter au prédécesseur de virtual soit faire virtual. red = iter

ii. iter devient cet intervalle virtuel: iter = virtual

iii. passer à l'étape 4

b. Si iter chevauche Φ.νν à droite (iter couvre les dates supérieures de Φ.νν) alors passer à l'étape 4

c. iter = iter. pred

d. retour à l'étape 2

3. Si iter est Nil (Ψ.Ι_¥ est vide ou bien tous les intervalles de M'.LV sont strictement supérieurs à Φ.νν) alors adjoindre Φ.νν à Φ LV puis FIN (étape 8).

4. Si iter n'est pas Nil faire i

a. si iter < ΖΙ(Ψ,Φ) alors passer à l'étape 5

b créer l'intervalle nv comme suit

i. Si iter.pred n'est pas Nil alors nv est (1 - iter.pred.u, iter. pred. ub. iter.lb, 1 - iter.l )

ii. sinon nv est (O.w.l, Φ-W.lb, iter.lb, 1 - iter.l )

c. si nv n Φ.νν n ^' est pas Nil l'adjoindre à gauche dans Buffer d. iter = iter.pred

e, retour à l'étape 4

5, Raccorder Buffer à droite de O.LV

6. FIN

Calcul de = V _[a] 4' :

1. iter = 4'.LV.Iast

2. Si iter n'est pas Nil faire :

2.1. Si iter ΖΙ(Ψ. Φ) est Nil

a) Si iter < ΖΙ(Ψ, Φ) alors passer à l'étape 3

b) iter = iter.pred

c) retour à l'étape 2

2.2. Ajouter ((iter. I, iter.lb ·- a, iter.ub - a, iter.u) n Φ.νν) en tête de Buffer

2.3. iter = iter.pred

2.4. retour à l'étape 2

3. Raccorder Buffer à droite de Φ-LV avec prise en compte de la valeur

4. FIN

Calcul de Φ = Ψ, A Ψ ₂ :

1. iterl = ¥,.LV.Iast

2. iter2 = ¥ ₂ .LV,last

3. Si iterl n ^' est pas Nil faire

3.1. Si iterl η ΖΙ(Ψ), Φ) est Nil

a) Si iterl < ΖΙ(Ψ., Φ) alors passer à l'étape 4

b) iterl = iterl .pred

c) retour à l'étape 3

3.2, Si iter2 n'est pas Nil et que (iter2 iterl ) est faux

a) adjoindre (iterl n iter2 n O.w) à gauche dans Buffer b) iter2 = iter2.pred c) retour à l'étape 3.2

3.3. iterl = iterl . pred

3.4. retour à l'étape 3

4. Raccorder Buffer à droite de .Ι_ν

FIN

Calcul de Φ = Ψ, v Ψ ₂ :

On introduit une notation supplémentaire. Soient i et j deux intervalles. On note j z. i si une des conditions suivantes est satisfaite :

• j est Nil et i n'est pas Nil

• i = j

• i ub > j.ub

• i.ub = j.ub et i.u = 1 et j.u = 0

• i.ub = j.ub et i.u = j.u et une de ces conditions est satisfaite :

o i.lb < j.lb

o i.lb = j.lb et i.l = 1 et j.i = 0

Autrement dit j Z i lorsque i va plus loin dans le futur que j ou bien, s'il va exactement aussi loin que j dans le futur, il va plus loin dans le passé que j.

1 . iterl = MV LV.Iast, iter2 = MVLV.Iast, tmp = Nil

2. Si iterl ou ïter2 est différent de Nil faire i

2.1 . si iter2 Z iterl alors passer à l'étape 2.3

2.2. sinon {on échange iterl et iter2):

a) tmp = iterl

b) iterl = iter2

c) iter2 = tmp

2.3. Si iterl < ΖΙ(Ψ, , Φ) alors passer à l'étape 3

2.4. Adjoindre à gauche iterl Φ .νν dans Buffer

2.5. Si iter2 n ^' est pas Nil faire : a) si iter2 chevauche iteri à gauche ou si iter2 < iteri alors passer en 2,6

b) iter2 = iter2.pred

c) retour à l'étape 2,5.

2.6. iteri = iteri . red

2.7, retour à l'étape 2.

3. Raccorder Buffer à droite de #.LV

4. FIN Calcul de Φ = Ψ, > Ψ ₂ : se ramène au calcul de -ι4Ί v ψ _2.

Calcul de Φ = Ej Ψ ;

1. iter = ^l F.LV.Iast

2. Si iter n'est pas Nil faire :

2.1. Si iter n ΖΙ(Ψ, Φ) est Nil

a) Si iter < ΖΙ(Ψ, Φ) alors passer à l'étape 3

b) iter = iter. red

c) retour à l'étape 2

2.2. Adjoindre à gauche ((iter. I x i.u, iter.lb - i.ub, iter.ub - i.lb, iter.u x i.l) n Φ.νν) dans Buffer

2.3. iter = iter.pred

2.4. retour à l'étape 2

3. Raccorder Buffer à droite de O.LV

4. FIN

Calcul de Φ = GÎ Ψ i

! iter = H'. LV last

2 Si iter n'est pas Nil faire i

2.1. Si iter n ΖΙ(Ψ, Φ) est Nil

a) Si iter < ΖΙ(Ψ, Φ) alors passer à l'étape 3 b) iter = iter pred

c) retour à l'étape 2

2.2. Adjoindre à gauche ((iter. I, iter.lb, iter.ub, iter.u) J i) Φ.νν) dans Buffer

2.3. iter = iter.pred

2.4. retour à l ^' étape 2

3. Raccorder Buffer à droite de O. LV

FIN

Calcul de Φ = B _(e . _K) Ψ :

1. Si #.LV n'est pas vide, alors soit i son unique intervalle. On modifie cet intervalle de sorte qu ^' il devienne (i.l, Mb, #,w,ub, Φ /V. U ) puis FIN.

2. Sinon (Φ. Ι / est vide) :

a. Si H'. LV est vide alors FIN .

b. Si '.LV n ^' est pas vide et que j est son premier élément alors ajouter à (B _(e ,k) OJ.LV l ^' intervalle (j.lxk, j.lb - e, O.w.ub, O.w.u) puis FI N.

Calcul de Φ = Ψ, U ₍ i, ₀ .b.k) ^Ψ 2 :

1 . iterl = Ψ-..LV. Iast, iter2 = M LV last, ante = Nil

2. Si iter2 n ^' est pas Nil

2.1 . Si ¾ΘΓ2 ΖΙ(Ψ ₂ , Φ) est Nil

a) Si iter2 < ΖΙ(Ψ ₂ , Φ) alors passer à l ^' étape 3.

b) Îter2 = iter2.pred

c) retour à l'étape 2

2.2. Adjoindre iter2 à gauche dans Buffer (il y a déjà iter2 tout entier)

2.3. Si iterl n'est pas Nil

a) Si iterl ] n iter2 n'est pas Nil alors poser ante = iterl b) Si iterl] < iter2 alors passer à l'étape 2,4

c) iterl = iterl .pred

d) retour à l'étape 2.3 2.4. iteii = ante (iterl est alors l'intervalle le plus antérieur de ¥i.LV qui étende iter2 vers le passé ou bien est Nil)

2.5. ante = Nil

2.6. Si iterl n'est pas Nil et que iterl j chevauche iter2 à gauche alors adjoindre à gauche ((iterl .1, iterl ,tb, iter2.lb, 1 - iter2.l) ( iter2.lxk, iter2.lb - b, iter2.lb, 1 - iter2.l)) n Φ.νν dans Buffer

2.7. iter2 = iter2.pred

2.8. retour à l'étape 2

3. Raccorder Buffer à droite de <I>.LV

4. FIN

Calcul de Φ = Ψι U _i+ Ψ ₂ avec 0 i i+ :

1 . iterl = ¥i.LV.Iast, iter2 = ¥ ₂ .LV.Iast

2. Si iter2 n'est pas Nil faire :

2.1 . Si iter2 η ΖΙ(Ψ ₂ , Φ) est Nil

a) Si iter2 < ΖΙ(Ψ ₂ , Φ) alors passer à l'étape 3.

b) iter2 = iter2.pred

c) retour à l'étape 2

2.2. Si iterl n'est pas Nil faire :

a) Si r = (iterl ] n iter2) n'est pas Nil adjoindre à gauche i

((r.lx(i+).u, r.lb - (i+).ub, r.ub ~~ (î+).lb, r.ux(i+).l) n iterl ] ) n Φ w dans Buffer

b) Si iterl ] < iter2 passer à l'étape 2.3

c) iterl = iterl .pred

d) retour à l'étape 2.2

2 3. iter2 = iter2.pred

2.4. retour à l'étape 2

3. Raccorder Buffer à droite de «ï»,L¥

4. FIN Calcul de Φ = Top Ψ :

1 . iter = H'.LV.Iast

2. Si iter ^A s n'est pas Nil faire :

2.1. Si iter n ΖΙ(Ψ, Φ) est Nil

a) Si iter < ΖΙ(Ψ, Φ) alors passer à l'étape 3

b) iter = iter.pred

c) retour à l'étape 2

2.2. Adjoindre à gauche ((1 , iter.lb, iter.lb, 1 ) ^A s n Φ.νν) dans Buffer

2.3. iter = iter.pred

2.4. retour à l'étape 2

3. Raccorder Buffer à droite de #.LV

4. FIN

Calcul de Φ = Bot ψ :

1. iter = H'.LV.Iast

2. Si iter n'est pas Nil faire ;

2.1. Si iter ^A s ΖΙ(Ψ, Φ) est Nil

a) Si iter < Ζ!(Ψ. Φ) alors passer à l'étape 3

b) iter = iter.pred

c) retour à l'étape 2

2.2. Si iter ne chevauche pas Ψ.νν à droite alors adjoindre à gauche ((1 , iter.ub, iter.ub, 1 ) ^A s Φ.νν) dans Buffer

2.3. iter = iter.pred

2.4. retour à l'étape 2

3 Raccorder Buffer à droite de #.LV

4 FIN

Calcul de Φ = S _(1i0 , _b .k) :

1 iferl = LVJast, iter2 = ¥ ₂ .LV.fast 2. Si iter2 n'est pas Nil

2.1 . Si iter2 n ΖΙ(Ψ ₂ , Φ) est Nil

a) Si iter2 < ΖΙ(Ψ ₂ , Φ) alors passer à l'étape 3.

b) Sinon iter2 = iter2.pred

c) retour à l'étape 2

2.2. Si iterl n'est pas Nil

a) Si iter2 n [iterl n'est pas Nil alors passer à l'étape 2.3 b) Si iter2 chevauche iterl à droite ou si iterl < iter2 alors passer à l'étape 2.3

c) iterl = iterl .pred

d) retour à l'étape 2 2

2.3. Si iterl n ^' est pas Nil et que [iterl chevauche iter2 à droite : a) alors adjoindre à gauche (fiter2 I, iter2.lb, iterl .ub, iterl ,u) n ( iter2.l, iter2.lb, iter2.ub + b. iter2. lxk)) n Φ.νν dans Buffer b) sinon adjoindre à gauche iter2 dans Buffer

2.4. iter2 = iter2.pred

2.5. retour à l'étape 2

3. Raccorder Buffer à droite de <I .LV

4. FIN

Calcul de Φ = Ψι S Ψ ₂ avec 0 e i+:

1 . iterl = 4VLV.Iast et iter2 = ₂ .LV.Iast

2. Si iter2 n ^' est pas Nil faire :

2.1 . Si iter2 η ΖΙ(Ψ ₂ , Φ) est Nil

a) Si iter2 < ΖΙ(Ψ _2» Φ) alors passer à l'étape 3

b) iter2 = iter2 pred

c) retour à l'étape 2

2.2. Si iterl n'est pas Nil faire ;

a) Si r = îter2 [iterl n'est pas Nil alors adjoindre à gauche

((rJx(i+).l, r.ib + (i+)Jb. r.ub + (H-).ub, r.ux(i+).u)n j iterl )) n #.w dans Buffer

b) Si [iterl < iter2 alors passer à l'étape 2.3 c) iterl = iterl .pred

d) retour à l ^' étape 2.2

2.3. iter2 = iter2.pred

2.4. retour à l'étape 2

Raccorder Buffer à droite de #.LV

FIN

Calcul pour Φ = Ο(σ).

1 . iter = o.LV.Iast

2. Si iter ^A s n'est pas Nil faire :

2.1 . Si iter n ΖΙ(σ, Φ) est Nil

a) Si iter < ΖΙ(σ, Φ) alors passer à l'étape 3 b) iter = iter. pred

c) retour à l'étape 2

2.2. Si s e O.set ajouter (iter n Φ.νν) en tête de Buffer

2.3. iter = iter.pred

2.4. retour à l ^' étape 2

3. Raccorder Buffer à droite de Φ LV

4. FIN

Calcul de Φ = 4Ί S ₍ d, _k) ¾ avec d > 0 ou bien k = 0:

1 . iterl = *F, .LVJast et iter2 = ₂ .LV.Iast

2, Si iter2 n'est pas Nil faire :

2.1 Si iter2 n ΖΙ(Ψ ₂ , Φ) est Nil

a) Si iter2 < ΖΙ(Ψ ₂ , Φ) alors passer à l'étape 3. b) Sinon iter2 = Îter2.pred

c) retour à l'étape 2

2.2. Si iterl n ^' est pas Nil faire i a) Si iterl chevauche Φ.νν à gauche et que Φ LV last jouxte Φ.νν à gauche alors :

• adjoindre iterl n Φ.νν à gauche dans Buffer

• passer à l'étape 3

b) Si r = iter2 n [iterl n'est pas Nil alors adjoindre (kxr.l, r.lb + d, iterl .ub, iterl .u) n Φ-w à gauche dans Buffer

c) Si iterl < iter2 passer à l'étape 2.3

d) iterl = iterl . pred

e) retour à l'étape 2.2

2.3. iter2 = iter2.pred

2.4. retour à l'étape 2

3. Raccorder Buffer à droite de Φ.Ι_ν

4. FIN

Calcul pour Φ = f(o).

1 . iter = o.LV.Iast

2. Si iter ^A s n'est pas Nil faire :

2.1 . Si iter η ΖΙ(σ, Φ) est Nil

a) Si iter < ΖΙ(σ, Φ) alors passer à l'étape 3

b) iter = iter.pred

c) retour à l'étape 2

2.2. ajouter (iter n #.w) ^A f(s) en tête de Buffer

2.3. iter = iter.pred

2.4. retour à l'étape 2

3. Raccorder Buffer à droite de Φ.Ι_ν

4. FIN

Calcul de Φ = Ψι 8, _α Ψ ₂ :

1. iterl = uLVJast et iter2 = ₂ .LV.Iast

2 Si iter2 n'est pas Nil 2.1 . Si iter2 n ΖΙ(Ψ ₂ , Φ) est Nil

a) Si îter2 < ΖΙ(Ψ ₂₎ Φ) alors passer à l'étape 3.

b) iter2 = iter2.pred

c) retour à l'étape 2

2.2. Si iterl n ^' est pas Nil

a) Si iter2 n [iterl n'est pas Nil alors passer à l'étape 2.3 b) Si iter2 chevauche iterl à droite ou si iterl < iter2 alors passer à l'étape 2.3

c) iterl = iterl .pred

d) retour à l ^' étape 2.2

2.3. Si [iterl chevauche iter2 à droite :

a) alors adjoindre à gauche (iter2.l, iter2.lb. iterl .ub, iterl . u) η Φ.νν dans Buffer

b) sinon adjoindre iter2 n Φ.νν à gauche dans Buffer

2.4. iter2 = iter2.pred

2.5. retour à l'étape 2

3. Raccorder Buffer à droite de Φ.ΐν

4. FIN Calcul de Φ = Nj Ψ :

1 . iter = Ψ. Ι /.last

2. Buffer = (Φ.ννχΟ) (la liste Buffer est initialisée avec un unique

intervalle de compteur 0 et égal à Φ.νν)

3. Si iter n'est pas Ni! faire :

3.1 . Si iter n Zi( \ Φ) est Nil

a) Si iter < ΖΙ(Ψ, Φ) alors passer à l'étape 4

b) iter = iter.pred

c) retour à l ^' étape 3

3.2. Effectuer l'adjonction à gauche avec compteur de ((i.u, iter.lb - Lut», iter.lb - i.Ib, U) <t>.w)x1 dans Buffer 3.3. iter = iter.pred

3.4. retour à l'étape 3

4. Raccorder Buffer à droite de Φ. Ι_ν

5. FIN

Calcul de Φ = Top{@}, ψ : se réduit au calcul de @(N, (Top Ψ)) Calcul de Φ = Bot{@}i Ψ : se réduit au calcul de @(N. (Bot Ψ))

Calcul de Φ = (01 ,02) (procédure dédiée aux couples de termes)

1 . iterl = 01.LV.last ; iter2 = o ₂ .LV.Iast

2. Si iterl n'est pas Nil faire 1

2, 1. Si iterl n ΖΙ(οι , Φ) est Nil

a) Si iterl < ΖΙ(σι , Φ) alors FIN

b) iterl = iterl .pred

c) retour à l ^' étape 2

3. Si iter2 n'est pas Nil faire :

3.1 . Si iter2 n ΖΙ(σ ₂ , Φ) est Nil

a) Si iter2 < ΖΙ(σ ₂ , Φ) alors FIN

b) iter2 = iter2.pred

c) retour à l'étape 3

4. Si iterl et iter2 ne sont pas Nil faire 1

4.1 . si iterl < ZI(o< . Φ) et iter2 < ΖΙ(σ _? , Φ) alors passer en l'étape 5

4.2. si iter2 Z iterl alors passer à l'étape 4.4

4.3. sinon (on échange iterl et iter2):

a) tmp = iterl

b) iterl = ïter.2

c) iter2 = tmp

4.4. En supposant que si est la valeur de Iterl et. s2 celle de iter2 ajouter (iterl nrter2ri#. ) ^A (s1 ,s2) en tête de Buffer 4.5. si itei .lb = iter2.lb et iterl . I = iter2

a) iterl = iterl .pred

b) iter2 = iter2.pred

c) retour à l'étape 4

4.6. Si iter2 chevauche iterl à gauche

a) iterl = iterl .pred

b) retour à l'étape 4

4.7. iter2= iter2.pred

4.8. retour à l'étape 4

Raccorder Buffer à droite de O.LV

FIN

Calcul général pour Φ = (σι, .., σ _η )

Cette procédure est récursive :

1. Si n = 2 on applique le calcul dédié aux couples sur le couple (σι, 02) 2. Si n > 2 on voit Φ comme le couple (Φ'. σ _η ) où Φ ^' = (σι, .., σ _η -ι) et on fait:

o Appel récursif au calcul de Φ

On applique le calcul dédié aux couples sur le couple (Φ',σ.,).

Les algorithmes explicités ci-dessus sont tous basés sur une marche arrière (parcours anti-chronologique). Il est aussi possible d ^' utiliser des algorithmes plus optimisés pour réduire tant les parcours que l'élimination. Ces algorithmes sont chronologiques Ils consistent à mémoriser Sors du calcul, sur quels intervalles des sous-expressions il faudra reprendre lors de la continuation suivante. Ceci évite de faire te parcours depuis ie dernier élément jusqu'à la zone d'influence. Par ailleurs, un intervalle de reprise dans une sous-expression désigne implicitement quels intervalles sont devenus inutiles à l'expression. Ce sont ses prédécesseurs, Ce principe est explicité par exemple sur le calcul de Ε|Φ: Soit rep l'intervalle de reprise mémorisé par Ε Φ (initialisé à Nil).

1 , Si rep est Nil on pose iter = (E _! ). LV.first sinon iter = rep

2. Tant que iter≠ Nil faire :

a. Si iter > ΖΙ(Φ.Ε,Φ) passer à l'étape ??.

b. Adjoindre à droite j = ((iter I x Lu, iter.lb - i.ub, iter.ub - i.lb, iter.u x i.l) n (Ε _ί Φ.νν)) dans (E D).LV

c. Si j chevauche E<I>.w à droite faire rep = iter et passer à l'étape ??

d, retour du Tant que 2

3, Communiquer à Φ que rep est un intervalle de reprise (laquelle retient le plus antérieur parmi ceux qui lui sont communiqués pour l'étape l'élimination)

4, FIN