Jaka jest różnica między LTL a CTL?

Przeczytałem już przykłady formuł w CTL, ale nie w LTL i vice versa, ale mam problem z uzyskaniem mentalnego zrozumienia formuł LTL i naprawdę, co jest w istocie różnicą.

Aby naprawdę zrozumieć różnicę między LTL i CTL, musisz przestudiować semantykę obu języków. Formuły LTL oznaczają właściwości, które będą interpretowane przy każdym uruchomieniu programu. Dla każdego możliwego wykonania (przebiegu), które może być postrzegane jako sekwencja zdarzeń lub stanów w linii - i dlatego nazywa się to „czasem liniowym” - sprawdzanie satysfakcji w przebiegu bez możliwości przełączenia na inny przebieg podczas sprawdzania. Z drugiej strony, semantyka CTL sprawdza formułę dla wszystkich możliwych przebiegów i spróbuje albo wszystkich możliwych przebiegów ( operator A ), albo tylko jednego przebiegu ( operator E ), gdy spojrzy się na gałąź.

W praktyce oznacza to, że niektórych wzorów każdego języka nie można podać w innym języku. Na przykład właściwość resetowania (ważna właściwość osiągalności przy projektowaniu obwodu) stwierdza, że ​​zawsze istnieje możliwość, że stan może zostać osiągnięty podczas przebiegu, nawet jeśli nigdy nie zostanie osiągnięty ( reset EF EF ). LTL może jedynie stwierdzić, że stan resetowania został rzeczywiście osiągnięty, a nie, że można go osiągnąć.

Z drugiej strony formuły LTL nie można przetłumaczyć na CTL. Ta formuła oznacza właściwość stabilności: przy każdym uruchomieniu programu s będzie w końcu prawdą do końca programu (lub na zawsze, jeśli program nigdy się nie zatrzyma). CTL może dostarczyć tylko formułę, która jest zbyt ścisła ( AF AG ) lub zbyt liberalna ( AF EG ). Drugi jest wyraźnie błędny. Po raz pierwszy nie jest to takie proste. Ale AF AG jest błędne. Rozważ system, który zapętla się na A1 , może przejść z A1 do B, a następnie przejdzie do A2 przy następnym ruchu. Następnie system pozostanie włączony$\Diamond\Box s$Stan A2 na zawsze. Wtedy „system w końcu pozostanie w stanie A ” jest właściwością typu . Oczywiste jest, że ta właściwość utrzymuje się w systemie. Jednak AF AG s puszka nie uchwycić tę właściwość, ponieważ jest odwrotnie: jest prowadzony w których system zawsze będzie w stanie, z którego ostatecznie przechodzi w bieg non A państwo.$\Diamond\Box s$

Nie wiem, czy to odpowiada na twoje pytanie, ale chciałbym dodać kilka komentarzy.

Dyskutuje się o najlepszej logice wyrażania właściwości do weryfikacji oprogramowania ... ale prawdziwa debata jest gdzie indziej. LTL może wyrażać ważne właściwości do modelowania systemu oprogramowania (uczciwość), gdy CTL musi mieć nową semantykę (nową relację satysfakcji), aby je wyrazić. Ale algorytmy CTL są zwykle bardziej wydajne i mogą wykorzystywać algorytmy oparte na BDD. Więc ... nie ma najlepszego rozwiązania. Jak dotąd tylko dwa różne podejścia.

Jeden z komentatorów sugeruje artykuł Vardiego „Rozgałęzienie a czas liniowy: ostateczne starcie” .

Jeśli podano jeden obiekt (np. Ślad w przypadku LTL), rozważasz tylko jedną przyszłość na każdy punkt w czasie, w CTL masz ich mnóstwo.

W szczególności nextdaje unikalne działanie w LTL, ale (potencjalnie) cały zestaw w CTL.