Jakie są praktycznie obliczalne właściwości znakowanych układów przejściowych?

Znalazłem systemy przejściowe oznaczone jako dobry model dla mojej aplikacji, a mianowicie jest artykuł na temat modelowania przypadków użycia przy użyciu LTS. Pytanie brzmi: co można łatwo udowodnić w LTS? Chciałbym ponownie wykorzystać istniejące rozwiązania, aby sprawdzić, czy są one przydatne w mojej aplikacji. Chciałbym wiedzieć, jakie właściwości LTS (i przypadków użycia) można łatwo automatycznie udowodnić, więc mogę zdecydować, czy istnieje praktyczny odpowiednik problemu dla przypadków użycia.

Formuły logiki Hennessy-Milnera są bardzo łatwe do udowodnienia na temat oznakowanych układów przejściowych. Jednak ta logika jest na tyle mało ekspresyjna (nie ma możliwości określenia właściwości nieskończonych ścieżek), że prawdopodobnie zechcesz rozważyć jej rozszerzenie, takie jak liniowa logika czasowa. LTL ma rozstrzygalny, ale kompletny problem z PSPACE.

Moduł sprawdzania modelu SPIN jest szeroko stosowanym narzędziem do sprawdzania właściwości LTL.

Kolejne dwa narzędzia, uzupełniające to zasugerowane przez Neela, to muCRL i mCRL2 . Oba zestawy narzędzi mają dość szeroki zakres narzędzi do definiowania LTS na różnych poziomach abstrakcji. Dostępne są również narzędzia do wizualizacji przestrzeni stanu i sprawdzania modelu. Podstawową logiką jest proposycyjny modalny rachunek mu , który jest znacznie bardziej wyrazisty niż LTL, ale wciąż jest rozstrzygalny. Inne przydatne narzędzia pozwalają na wykonanie modulo bisimulacji redukcji przestrzeni stanu w celu uzyskania najmniejszej reprezentacji twojego systemu.

Aby rozwinąć odpowiedź Dave'a, rachunek modalny mu jest również powiązany z pojęciem gier o nieskończonej parzystości. Istnieje bardzo dobry zestaw notatek z wykładów dostępnych tutaj: http://pub.ist.ac.at/gametheory/, które przedstawiają połączenie. Na marginesie, nie tylko decydujący jest modalny rachunek Mu-Dec, ale jest on w (patrz uwagi do wykładu).$\mathit{NP}\cap \mathit{co\text{-}NP}$

Właściwości CTL można sprawdzić w czasie liniowym (patrz Clarke i in .).

Dawno temu pracowałem w firmie, w której wielu kolegów używało Rulebase do weryfikacji projektów układów scalonych. Językiem właściwości jest PSL , jest standaryzowany przez IEEE i jest rodzajem CTL na sterydach.

Podczas kursu poznałem Isabelle , „ogólną asystentkę dowodową”. Obsługuje (całkowite) programowanie funkcjonalne (zbliżone do ML) i logikę wyższego rzędu. Możesz zdefiniować (lub znaleźć) języki dla LTS i LTL i udowodnić na nich twierdzenia. Nie wiem, czy można to uznać za łatwe, ale na pewno działa.

Jeśli twoje tło to CTL interpretowane przez struktury Kripke i szukasz czegoś podobnego interpretowanego przez LTS, to ACTL (CTL oparty na akcji) może być interesujące.

W 1990 r. R. De Nicola i F. Vaandrager wprowadzili ACTL jako CTL oparty na działaniu ( Logika oparta na działaniu dla systemów przejściowych , Semantyka systemów współbieżnych procesów (1990), s. 407-419). Został on dalej zbadany w 1993 r. (R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori: Ramy oparte na działaniu do weryfikacji właściwości logicznych i behawioralnych współbieżnych systemów , sieci komputerowych i systemów ISDN, t. 25, Nr 7, s. 761-778.), A ostatnio w 2008 r. (R. Meolic, T. Kapus, Z. Brezočnik: ACTLW - logika drzewa obliczeń opartych na działaniu z operatorem , chyba , że nauki ścisłe , 178 (6) , ss. 1542–1557).

Główną ideą ACTL (nie mylić z podzbiorem CTL z tym samym akronimem) jest posiadanie podobnych operatorów i podobnych algorytmów do sprawdzania modelu, jak dla CTL. Ponadto operatory są zdefiniowane przez wyrażenia stałoprzecinkowe analogiczne do tych używanych w CTL. Złożoność (nie jestem pewien co do ekspresyjności) ACTL leży gdzieś pomiędzy HML a modulacją μ-rachunku modalnego.