Ich fand, dass markierte Übergangssysteme ein gutes Modell für meine Anwendung sind. Es gibt nämlich einen Artikel über die Modellierung von Anwendungsfällen mithilfe von LTS. Die Frage ist, was kann über LTSs leicht bewiesen werden? Ich möchte vorhandene Lösungen wiederverwenden, um festzustellen, ob sie für meine Anwendung nützlich sind. Ich möchte wissen, welche Eigenschaften von LTSs (und Anwendungsfällen) einfach automatisch nachgewiesen werden können, damit ich entscheiden kann, ob es ein praktisches Gegenstück zum Problem für Anwendungsfälle gibt.
lo.logic
formal-modeling
model-checking
program-verification
automated-theorem-proving
Gabriel Ščerbák
quelle
quelle
Antworten:
Die Formeln der Hennessy-Milner-Logik lassen sich sehr leicht über markierte Übergangssysteme beweisen. Diese Logik ist jedoch nicht aussagekräftig genug (es gibt keine Möglichkeit, Eigenschaften unendlicher Pfade anzugeben), sodass Sie wahrscheinlich eine Erweiterung in Betracht ziehen möchten, z. B. die lineare zeitliche Logik. LTL hat ein entscheidendes, aber PSPACE-vollständiges Problem.
Die SPIN-Modellprüfung ist ein weit verbreitetes Tool zur Modellprüfung von LTL-Eigenschaften.
quelle
Weitere zwei Tools, die das von Neel vorgeschlagene ergänzen, sind muCRL und mCRL2 . Beide Toolsets verfügen über eine Reihe von Tools zum Definieren von LTS auf verschiedenen Abstraktionsebenen. Tools zur Statusraumvisualisierung und Modellprüfung sind ebenfalls verfügbar. Die zugrunde liegende Logik ist die propositionale Modal-Mu-Rechnung , die viel aussagekräftiger als LTL ist, aber dennoch entscheidbar ist. Mit anderen nützlichen Tools können Sie eine Modulo-Bisimulation zur Reduzierung des Zustandsraums durchführen, um die kleinste Darstellung Ihres Systems zu erhalten.
quelle
quelle
CTL-Eigenschaften können in linearer Zeit überprüft werden (siehe Clarke et al. ).
Vor langer Zeit arbeitete ich in einem Unternehmen, in dem viele Kollegen Rulebase zur Überprüfung des Designs von integrierten Schaltkreisen verwendeten. Die Eigenschaftssprache ist PSL , sie ist nach IEEE standardisiert und eine Art CTL für Steroide.
quelle
In einem Kurs lernte ich Isabelle kennen , eine "allgemeine Beweisassistentin". Es unterstützt (vollständige) Funktionsprogrammierung (in der Nähe von ML) und Logik höherer Ordnung. Sie können Sprachen für LTS und LTL selbst definieren (oder finden) und Theoreme auf diesen beweisen. Ich weiß nicht, ob das so einfach ist, aber es funktioniert auf jeden Fall.
quelle
Wenn Ihr Hintergrund eine CTL-Interpretation über Kripke-Strukturen ist und Sie nach einer ähnlichen Interpretation über LTS suchen, könnte ACTL (action-based CTL) interessant sein.
Bereits 1990 führten R. De Nicola und F. Vaandrager ACTL als aktionsbasierte CTL ein ( Action versus state based logics für Übergangssysteme , Semantics of Systems of Concurrent Processes (1990), S. 407-419). Es wurde 1993 weiter untersucht (R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori: Ein aktionsbasiertes Framework zur Verifikation der logischen und Verhaltenseigenschaften von gleichzeitigen Systemen , Computernetzwerken und ISDN-Systemen, Band 25). Nr. 7., S. 761-778.) Und vor kurzem in 2008 (R. Meolic, T. Kapus, Z. Brezočnik: ACTLW - Eine aktionsbasierte Berechnungsbaumlogik mit außer Operator , Information Sciences, 178 (6) , S. 1542-1557.)
Die Hauptidee von ACTL (nicht zu verwechseln mit einer Teilmenge von CTL mit demselben Akronym) besteht darin, ähnliche Operatoren und ähnliche Algorithmen für die Modellprüfung wie für CTL zu haben. Darüber hinaus werden Operatoren durch Festkommaausdrücke definiert, die den für CTL verwendeten entsprechen. Die Komplexität von ACTL (ich bin mir nicht sicher über die Expresivität) liegt irgendwo zwischen HML und propositional modal μ-calculus.
quelle