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

13

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.

Gabriel Ščerbák
źródło
1
musisz być bardziej precyzyjny. Co chcesz udowodnić? Czy potrzebujesz automatycznego narzędzia do sprawdzania właściwości? Jaka jest twoja aplikacja?
Dave Clarke
@Dave Clarke pod redakcją
Gabriel Ščerbák
2
Drugi wynik w Googling „Labeled Transition Systems”: doc.ic.ac.uk/ltsa
Kaveh
Dziękuję wszystkim bardzo za pomoc, nie czekałem na tak wiele pomocy. Teraz mam wiele do przeczytania i dopóki nie skończę, nie mogę uczciwie przyjąć żadnej odpowiedzi, chyba że niektóre wyróżnią się głosami. Więc proszę o cierpliwość.
Gabriel Ščerbák

Odpowiedzi:

11

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.

Neel Krishnaswami
źródło
11

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.

Dave Clarke
źródło
Nie wiedziałem, że modalne mu-rachunek jest rozstrzygalny! Teraz idę sprawdzić dowód w twoim łączu ...
Neel Krishnaswami
5
Zdanie modalne calculus jest rozstrzygalne; Wierzę, że Street i Emerson pokazali to w latach 80-tych. Pierwsze zamówienie z pewnością nie jest: jeśli o ile pamiętam, jest kompletne dla pierwszego poziomu hierarchii analitycznej. BTW, uwielbiam tę ankietę autorstwa Bradfielda i Stirlinga. Myślę, że jest to jedno z najlepiej napisanych relacji z teorii calculus. μμμ
Mark Reitblatt
5

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).NPco-NP

Aubrey da Cunha
źródło
3
Problem sprawdzania modelu występuje w . Problemem jest decyzja -time kompletne, wierzę. E X PNPcoNPEXP
Mark Reitblatt,
3

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.

Radu GRIGore
źródło
Wątpię, by FRELIMO zostało sprawdzone za pomocą CTL - możesz poprawić ten link.
reinierpost
Naprawiony. Może Google Scholar zmienił swoje identyfikatory? Nie pamiętam, żeby kiedykolwiek widziałem „FRELIMO”.
Radu GRIGore,
2

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.

Raphael
źródło
1
Przeczytałem (jedną część) pytania jako „Jakie są narzędzia, które pomagają mi udowodnić właściwości LTS?” I dowodzą, że przyszli mi na myśl asystenci. Z pewnością masz rację, inni mogą również wykonywać tę pracę, ale nie mogę zbyt dobrze twierdzić, że robią to, jeśli nie wiem tego na pewno, prawda?
Raphael
1
Radu, interpolowałem. Należy pamiętać, że narzędzia takie jak Isabelle mają zdolność do automatyzacji proofów, chociaż mogą być słabsze w określonych aplikacjach (ponieważ są to narzędzia ogólne). Mogą być bardziej pomocne niż specjalistyczne narzędzia, jeśli chcesz udowodnić właściwości, których narzędzia te nie mogą automatycznie udowodnić.
Raphael
Interesujące jest, jak można dziś interpretować termin „ogólny asystent dowodowy”, który L. Paulson wprowadził w 1989 roku. To jest całkowicie OK. Początkowo pomysł polegał na stworzeniu ogólnej logicznej struktury do gromadzenia teorii tygodnia Martina-Löfa tygodnia (która w tym czasie bardzo się zmieniała). Później framework został ponownie użyty dla Isabelle / ZF, ponownie później dla Isabelle / HOL, która jest teraz główną aplikacją.
Makarius
2

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.

meolic
źródło