Recherche d'un système de ré-écriture

Bonjour à tous,

Je me permets de venir vers la communauté car je suis franchement assez perdu.

Je travaille avec une logique formelle F qui est une extension temporelle de la logique du premier ordre (c’est grosso-merdo FOL avec en plus quelques prédicats un peu spéciaux). J’ai donc des variables quantifiées dans mes formules.

Exemple ($P,Q$ sont des prédicats, éventuellement spéciaux): $\forall x (P(x) \implies \exists y Q(y))$

Pour cette logique, j’ai sa sémantique, qui est définie sur une certaine gamme de structure d’interprétation avec un ensemble de règles de satisfactions. J’ai en particulier un ensemble $D$ de valeur que peuvent prendre les variables quantifiée et la valeur des prédicats. Par exemple dans $M$, j’ai $D=\{a,b\}$ et $P(a)$ et $Q(b)$ sont vrais, $P(b)$ et $Q(a)$ sont faux. alors me permet de dire que cette formule $f$ est vraie sur $M$

Jusque là rien que du très classique si vous avez fait un peu de logique.

Je cherche à définir un algo de model-checking pour cette logique. Autrement dit, étant donnée une formule $f$, une instance $M$ d’une structure d’interprétation, est ce que $ M \models f$. Ca revient (là encore grosso merdo), à énumérer toutes les valeurs possibles de $D$ pour chacune des variables quantifiées.

Contrainte supplémentaires, je souhaite le faire via un système de ré-écriture. L’idée, c’est d’exprimer mon problème de model checking via les ré-écriture de sorte que la terminaison de l’algo soit prouvée par la terminaison du système de ré-écriture et que sa correction le soit par la confluence du système (et la correction des règles vis à vis de la sémantique donnée).

Et c’est à partir de là que je suis perdu (la ré-écriture n’est pas du tout, mais pas du tout dans mon domaine de compétence).

Illustration de ce à quoi je souhaite arriver exprimer formellement avec des ré-écriture: $ \forall x (P(x) \implies \exists y Q(y)) $ se récrit en $ \forall x \in \{a,b\} (P(x) \implies \exists y Q(y)) $ qui se ré-écrit en $ (P(a) \implies \exists y Q(y)) \land (\forall x \in \{b\} (P(x) \implies \exists y Q(y))) $ qui se ré-écrit en $ ( \top \implies \exists y Q(y)) \land (\forall x \in \{b\} (P(x) \implies \exists y Q(y))) $ qui se ré-écrit en $ ( \exists y Q(y)) \land (\forall x \in \{b\} (P(x) \implies \exists y Q(y))) $ etc…

Expliqué comme ca, ca ne semble pas trop sorcier.

J’ai, à mes yeux, plusieurs contraintes qui rendent la tâche assez difficile:

• J’ai besoin d’intégrer les valeurs du domaine à mon système de ré-écriture. C’est le plus simple à régler, celles sont considérées comme des constantes et voilà.
• Le système de ré-écriture doit être/devrait être/est conditionnel avec une dépendance sémantique à la structure d’interpretation. Traduction sur l’exemple. Si le modèle $M$ me dit que $P(a)$ est vrai, alors je vais ré-écrire $P(a)$ en $\top$, sinon en $\bot$
• J’ai des variables liées. Cette dépendance m’a orienté vers les systèmes d’ordre supérieur mais qui sont bien un cran au dessus des système de ré-écriture de terme et j’ai beaucoup de mal à comprendre.

Et c’est là que je me tourne vers vous, car j’ai plusieurs questions

• Connaissez vous un système clé en main qui réponde à mes besoins ?
• Pensez vous que l’ordre supérieur soit nécessaire ? Des gens m’ont dit que non sans vraiment m’expliquer pourquoi ?
• S’il n’existe rien, connaissez vous des articles qui présentent des choses proches de ce que je cherche à faire ? En particulier, je n’ai rie trouvé pour la dépendance sémantique. Tous les systèmes conditionnels que j’ai pu trouver ont des contraintes non sémantiques (pas de meilleur mot) de la forme u = v => s -> t (s se récrit en t si u et v sont unifiables ou si on peut ré-écrire u en v par exemple).

Toute réponse est la bienvenue.

Merci beaucoup, David.

Même si j’ai une vague idée de ce que tu veux faire et que ça me semble pas trop sorcier à faire, est-il possible d’avoir une référence vers ta logique ?

En outil qui prouve la confluence et la terminaison pour toi c’est Maude. Dans ton cas, vu que tu es en FOL, je ne vois pas pourquoi il y aurait besoin de faire de l’ordre supérieur. Ca dépend ce que tu veux faire, mais avec ce que tu nous présentes je vois pas pourquoi tu en aurais besoin.

Pourquoi as-tu besoin de réécriture conditionnelle, car là non plus, avec ce que tu nous présentes je vois pas pourquoi tu en aurais besoin.

Je fais une thèse dans une équipe spécialisée en réécriture, donc je peux probablement t’aider un peu, mais comme je le dis au début de mon message, une référence serait intéressante pour aller plus loin.

Déjà, merci de ta réponse.

Oui, tu peux trouver une référence à la logique dans un article plus orienté application robotique :Improving Code Quality in ROS Packages Using a Temporal Extension of First-Order Logic. La logique est présentée partie IV, c’est dense, article oblige, mais tu as l’essentiel.

Je cherche justement à développer les aspects plus théoriques de la chose (je suis en thèse aussi).

J’étais parti sur de la ré-écriture d’ordre supérieur en lisant le chapitre 11 (Extensions) section 4 de Term Rewriting and All That. Il dit e gros que systèmes de ré-écriture de termes ne peuvent pas manipuler des éléments avec des variables liées (ce qui est mon cas), d’où mon orientation sur l’ordre supérieur et ma question sur la pertinence de cet axe.

En ce qui concerne la besoin de conditions, il me semble nécessaire si je veux mettre une seule règle du style $P(t_1,...,t_n) \rightarrow \top \text{ si } P(t_1,...,t_n) \text{ est vrai}$ et $P(t_1,...,t_n) \rightarrow \top \text{ si } P(t_1,...,t_n) \text{ est faux}$.

Si je peux encoder la valuation de chaque prédicat sur chaque combinaison de termes possible (genre $P(a)\rightarrow \top $, $Q(b)\rightarrow \top $, $P(b)\rightarrow \bot $, $Q(a)\rightarrow \bot $), alors oui, ca peut marcher mais ca semble assez contraire à l’idée des systèmes de ré-écriture qui ont en général un petit nombre de règle. Mais c’est le genre de chose que je ne suis même pas sûr d’avoir le droit (tellement je maitrise mal le sujet =/).

Je suis tombé sur Maude dans mes recherches, mais je ne vois pas comment formaliser mon cas avec.

Oui, tu peux trouver une référence à la logique dans un article plus orienté application robotique :Improving Code Quality in ROS Packages Using a Temporal Extension of First-Order Logic. La logique est présentée partie IV, c’est dense, article oblige, mais tu as l’essentiel.

Je ne peux pas accéder à ce papier. Est-ce que tu n’aurais pas quelque chose de libre d’accès ? (Ou pourrais-tu reproduire ici cette partie IV si c’est pas trop gros ?)

Je ne connais rien au sujet mais j’ai des questions :

• Est-ce que ce que tu veux faire correspond au mot-clef "symbolic model checking" ?
• C’est certain qu’une approche de type "tester bêtement toutes les possibilités" fonctionne avec une logique temporelle (mais je ne sais pas exactement ce que ça englobe) ? Il n’y a pas une infinité de possibilités à tester ?
• Est-ce que l’idée de système réécriture que tu proposes ne revient pas à tester toutes les possibilités ?
• Quand tu dis variables liées, tu parles des variables liées par les quantificateurs ?

J’ai mis le pre-print ici. L’organisation de l’article est légèrement différente, c’est section III.B Specification formalism: FO++

Est-ce que ce que tu veux faire correspond au mot-clef "symbolic model checking" ?

Pas vraiment. L’idée du model checking, c’est qu’on a un système représenté sous forme de structure de Kripke (~une machine à état) et une propriété décrite en logique temporelle, et on vérifier si cette propriété est vraie ou non sur le le système, sachant que la propriété porte sur les états actuels ou futurs (exemple, si dans un état température > 100 alors au prochain alarme = on). Le soucis, c’est qu’il faut générer/explorer tous les états possibles. n variables binaires définissent $2^n$ états possibles, ca explose vite. L’idée du symbolic model checking, c’est au lieu d’énumérer explicitement tous les états, on va en représenter certains de façon symboliques de façon à gagner en complexité.

Je fais un truc assez différent: je vérifie la conformité de source avec une spécification utilisateur. La spécificité de l’approche, c’est qu’on analyse les fonctions sous l’angle de leur CFG (vue comme des structures de Kripke) et qui qu’on est capable d’utiliser des informations en provenance de l’AST, en particulier celui en dehors des fonctions. Ca permet de formaliser et vérifier des trucs comme:Dans toutes les classes $c$, pour toutes les fonctions membres $f$ non const de $c$, un attribut $a$ de la classe est modifié (syntaxiquement parlant) dans $f$. Si y’en a pas, c’est que la fonction devrait etre déclarée const.

En formel dans ma logique, ca donne:

La logique du premier ordre sert à exploiter l’information en provenance de l’AST (notion de class, lister les fonctions de la classe, est ce qu’une fonction est const ou non..) et les logiques temporelles à dire des choses sur les CFG des fonctions. Les logiques temporelles sont intégrées par le biais de prédicat spéciaux dont je parlais (ici, $modelsCTL(\circ,\circ))$. Intuitivement, $modelsCTL(x,g)$ sera vrai si la formule de CTL $g$ est vraie sur le CFG de $x$ selon les règles de CTL classiques.

La vérification du code est alors définie comme l’extraction d’une structure d’interprétation pour la logique depuis le code et la vérif de la spec sur cette structure par un algo de model checking pour ma logique. Et c’est cet algo de model checking aec

J’espère que c’est clair.

C’est certain qu’une approche de type "tester bêtement toutes les possibilités" fonctionne avec une logique temporelle (mais je ne sais pas exactement ce que ça englobe) ? Il n’y a pas une infinité de possibilités à tester ?

C’est le rôle du model-checking que de vérifier si une formule de logique temporelle est valide ou non sur une structure de Kripke. C’est un peu plus fin que de tester toutes les valeurs possibles car les logiques temporelles sont évaluées sur des traces / arbres d’évaluation infinies.

Est-ce que l’idée de système réécriture que tu proposes ne revient pas à tester toutes les possibilités ?

Le model checking de ma logique consiste à tester toutes les valeurs acceptables pour chacune des variables quantifiées. Dans mon exemple, si dans mon code, j’ai 3 classes C1,C2,C3, alors je vais tester pour $c$, $C1$, puis toutes les fonctions membres de $C1$,… Je souhaite utiliser des re-écriture pour représenter ce "calcul"

Quand tu dis variables liées, tu parles des variables liées par les quantificateurs ?

Oui, cf exemple =)

J’espère que c’est clair.

Merci. Ça reste assez flou mais je ne vais pas entrer dans les détails.

Tu as une idée de comment faire un model-checker pour CTL avec un système de réécriture ? Parce que dans ce que tu présentes tu ne parles que de la partie "premier ordre".

Et c’est cet algo de model checking aec

Phrase non terminée ?

Alors, les re-ecritures se cantonnent à la partie premier ordre. Dans mon approche, la valuation des predicats pour les logiques temporelles est calculée en se ramenant à un problème de model checking de logique temporelle, problèmes pour lequel il existe des algorithmes classiques. Donc du point de vu évaluation, ces predicats rentrent au meme titre que d’autres prédicats (ex, isConst) au détail pret que la valuation dema de un plus de calcul.

Donc je recherche essentiellement un système de recriture pour evaluer des formules du premier ordre.

Edit: la phrase non finie disait simplement que c’est mon algo de MC que je veux représenter avec des réécriture

Ah d’accord. Donc ce que tu fais, c’est réécrire :

• les $∀$ en conjonction,
• les $∃$ en disjonction,
• les $P(a_1,…,a_n)$ en leurs valeurs (avec $P$ qui peut être également un connecteur comme $⇒$ ou $∧$) ?

Ça fait un système de réécriture différent par modèle, avec plein de règles, mais ça me semble obligatoire. Qu’est-ce qui bloque ? J’ai relu la question initiale mais je ne vois pas en quoi les points que tu listes posent problème. Je ne sais pas ce que tu entends par "les systèmes d’ordre supérieur" mais tu traites les variables liées avec les deux premiers types de règles, non ?