Uczciwa obliczeniowa logika drzewa

Uczciwa obliczeniowa logika drzewa to konwencjonalna obliczeniowa logika drzewa badana z wyraźnymi ograniczeniami rzetelności.

Słaba uczciwość / sprawiedliwość

Deklaruje warunki, takie jak wszystkie procesy wykonywane nieskończenie często. Jeśli uznasz, że procesy są P _i , to warunek przyjmuje postać:

${\ Displaystyle \ bigwedge GFP_ {i}}$

Silna sprawiedliwość / współczucie

Tutaj, jeśli proces żąda zasobu nieskończenie często (R), powinien mieć możliwość otrzymywania zasobu (C) nieskończenie często:

${\ Displaystyle \ bigwedge (GFR \ longrightarrow GFC)}$

Sprawdzanie modelu pod kątem uczciwego CTL

Rozważmy model Kripkego ze zbiorem stanów F . Ścieżka $uczciwą$ uważana za ścieżkę wtedy gdy ścieżka obejmuje wszystkich F często Sprawiedliwe sprawdzanie modelu CTL ogranicza sprawdzanie tylko do uczciwych ścieżek. Istnieją dwa rodzaje sprawiedliwych kwantyfikatorów:

1. M _fa , s $Displaystyle \$ _| = ZA $phi}$ wtedy i tylko wtedy, gdy zachodzi na wszystkich uczciwych ścieżkach.

2. M _fa , s $\$ _| = mi $phi}$ wtedy i tylko wtedy, gdy zachodzi jedna lub więcej uczciwych ścieżek.

Sprawiedliwy stan to taki, z którego pochodzi co najmniej jedna uczciwa ścieżka. To przekłada się na M _f , s |= EGtrue.

Podejście oparte na SCC

Składowa silnie spójna (SCC) grafu skierowanego to podgraf maksymalnie silnie spójny — wszystkie węzły są osiągalne względem siebie. Uczciwy SCC to taki, który ma przewagę w co najmniej jednym węźle dla każdego z uczciwych warunków.

Aby sprawdzić uczciwe EG dla dowolnej formuły,

1. Oblicz tak zwane oznaczenie wzoru φ : zbiór stanów takich, że M, s |= φ .
2. Ogranicz model do denotacji.
3. Znajdź uczciwy SCC.
4. Uzyskaj połączenie wszystkich 3 (powyżej).
5. Oblicz stany, które mogą osiągnąć unię.

Algorytm Emersona Lei

Charakterystyka punktu stałego Exist Globally jest dana wzorem: [EGφ] = νZ .([φ] ∩ [EXZ ]), co jest zasadniczo granicą stosowaną zgodnie z twierdzeniem Kleene'a . Dla uczciwych ścieżek staje się [Ef Gφ] = νZ .([φ] ∩ _{Fi ∈FT} [EX[E(ZU(Z ∧ Fi ))]), co oznacza, że ​​formuła obowiązuje w stanie bieżącym i stanach następnych oraz następny do następnych stanów, dopóki nie spełni wszystkich członków uczciwych warunków. Oznacza to, że warunek jest równoważny z rodzajem punktu akceptacji, w którym warunek akceptacji jest całym zestawem warunków Uczciwych.

• Emerson, EA; Halpern, JY (1985). „Procedury decyzyjne i ekspresywność w czasowej logice czasu rozgałęzionego” . Journal of Computer and System Sciences . 30 (1): 1–24. doi : 10.1016/0022-0000(85)90001-7 .
• Clarke, EM ; Emerson, EA i Sistla, AP (1986). „Automatyczna weryfikacja współbieżnych systemów o skończonych stanach przy użyciu specyfikacji logiki czasowej”. Transakcje ACM dotyczące języków i systemów programowania . 8 (2): 244–263. doi : 10.1145/5397.5399 .