Quelles sont les propriétés pratiquement calculables des systèmes de transition étiquetés?

13

J'ai trouvé que les systèmes de transition étiquetés sont un bon modèle pour mon application, à savoir qu'il existe un article sur la modélisation des cas d'utilisation à l'aide de LTS. La question est, que peut-on facilement prouver sur les LTS? Je voudrais réutiliser les solutions existantes pour voir si elles sont utiles pour mon application. Je voudrais savoir quelles propriétés des LTS (et cas d'utilisation) peuvent être facilement prouvées automatiquement, donc je peux décider s'il y a une contrepartie pratique au problème pour les cas d'utilisation.

Gabriel Ščerbák
la source
1
vous devez être plus précis. Que voulez-vous prouver? Voulez-vous un outil automatique pour prouver les propriétés? Quelle est votre candidature?
Dave Clarke
@Dave Clarke édité
Gabriel Ščerbák
2
Le deuxième résultat sur Google "Systèmes de transition étiquetés": doc.ic.ac.uk/ltsa
Kaveh
Merci à tous pour votre aide, je n'ai pas attendu ces nombreuses aides. J'ai maintenant beaucoup à lire et jusqu'à ce que j'aie terminé, je ne peux pas accepter équitablement une réponse, à moins que certaines ne se démarquent par des votes. Soyez donc patient.
Gabriel Ščerbák

Réponses:

11

Les formules de la logique de Hennessy-Milner sont très faciles à prouver sur les systèmes de transition étiquetés. Cependant, cette logique est suffisamment inexpressive (il n'y a aucun moyen d'énoncer les propriétés de chemins infinis) que vous souhaiterez probablement envisager une extension, comme la logique temporelle linéaire. LTL a un problème décidable mais complet sur PSPACE.

Le vérificateur de modèle SPIN est un outil largement utilisé pour vérifier les propriétés LTL du modèle.

Neel Krishnaswami
la source
11

Deux autres outils, pour compléter celui suggéré par Neel, sont muCRL et mCRL2 . Les deux ensembles d'outils ont toute une gamme d'outils pour définir le LTS à différents niveaux d'abstraction. Des outils de visualisation de l'espace d'états et de vérification des modèles sont également disponibles. La logique sous-jacente est le calcul modal mu propositionnel , qui est beaucoup plus expressif que LTL, mais encore décidable. D'autres outils utiles vous permettent d'effectuer une bisimulation modulo de réduction de l'espace d'état pour obtenir la plus petite représentation de votre système.

Dave Clarke
la source
Je ne savais pas que le mu-calcul modal était décidable! Maintenant, je vais regarder la preuve dans votre lien ...
Neel Krishnaswami
5
μμ
5

NPco-NP

Aubrey da Cunha
la source
3
NPcoNPEXP
3

Les propriétés CTL peuvent être vérifiées en temps linéaire (voir Clarke et al ).

Il y a longtemps, je travaillais dans une entreprise où de nombreux collègues utilisaient Rulebase pour vérifier les conceptions de circuits intégrés. Le langage de propriété est PSL , il est normalisé par IEEE et est une sorte de CTL sur les stéroïdes.

Radu GRIGore
la source
Je doute que FRELIMO ait été contrôlé par modèle avec CTL - vous souhaiterez peut-être corriger ce lien.
reinierpost
Fixé. Peut-être que Google Scholar a changé ses identifiants? Je ne me souviens pas avoir jamais vu "FRELIMO".
Radu GRIGore
2

Dans un cours, j'ai fait la connaissance d' Isabelle , une "assistante de preuve générique". Il prend en charge la programmation fonctionnelle (totale) (proche de ML) et la logique d'ordre supérieur. Vous pouvez définir vous-même (ou trouver) des langages pour LTS et LTL et prouver des théorèmes sur ceux-ci. Je ne sais pas si cela peut être considéré comme facile, mais cela fonctionne certainement.

Raphael
la source
1
J'ai lu (une partie de) la question comme "Quels sont les outils qui m'aident à prouver les propriétés des LTS?", Et je prouve que les assistants me viennent à l'esprit. Vous avez certainement raison, d'autres pourraient aussi faire le travail, mais je ne peux pas très bien prétendre qu'ils le font si je n'en suis pas sûr, n'est-ce pas?
Raphael
1
Radu, j'ai interpolé. Notez que des outils comme Isabelle ont la capacité d'automatiser les épreuves, bien qu'ils puissent être plus faibles dans une application spécifique (car ce sont des outils généraux). Ils peuvent être plus utiles que les outils spécialisés si vous souhaitez prouver des propriétés que ces outils ne peuvent pas prouver automatiquement.
Raphael
Il est intéressant de voir comment le terme "assistant de preuve générique" que L. Paulson a introduit en 1989 peut être interprété de nos jours. C'est parfaitement OK. À l'origine, l'idée était d'avoir un cadre logique générique pour fumuler la théorie de type de Martin-Löf de la semaine (qui changeait beaucoup à l'époque). Plus tard, le framework a été réutilisé pour Isabelle / ZF, encore une fois plus tard pour Isabelle / HOL, qui est maintenant l'application principale.
Makarius
2

Si votre arrière-plan est interprété CTL sur des structures Kripke et que vous recherchez quelque chose de similaire interprété sur des LTS, ACTL (CTL basé sur l'action) pourrait être intéressant.

En 1990, R. De Nicola et F. Vaandrager ont introduit ACTL en tant que CTL basé sur l' action ( Action versus state based logics for transition systems , Semantics of Systems of Concurrent Processes (1990), pp. 407-419). Il a été étudié plus avant en 1993 (R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori: An Action-Based Framework for Verifying Logical and Behavioral Properties of Concurrent Systems , Computer Networks and ISDN Systems, Vol. 25, No 7., pp. 761-778.) Et plus récemment en 2008 (R. Meolic, T. Kapus, Z. Brezočnik: ACTLW - An Action-based Computation Tree Logic With Unless Operator , Information Sciences, 178 (6) , p. 1542-1557.)

L'idée principale d'ACTL (à ne pas confondre avec un sous-ensemble de CTL avec le même acronyme) est d'avoir des opérateurs et des algorithmes similaires pour la vérification des modèles comme ceux de CTL. De plus, les opérateurs sont définis par des expressions à virgule fixe analogues à celles utilisées pour CTL. La complexité (je ne suis pas sûr de l'expressivité) d'ACTL se situe quelque part entre HML et μ-calcul modal propositionnel.

méolique
la source