Rättvis logik för beräkningsträd

Rättvis beräkningsträdlogik är konventionell beräkningsträdlogik som studeras med explicita rättvisa begränsningar.

Svag rättvisa/rättvisa

Detta förklarar tillstånd som att alla processer exekveras oändligt ofta. Om du anser att processerna är P _i blir villkoret:

$\bigwedge GFP_{i}$

Stark rättvisa/medkänsla

Här, om en process begär en resurs oändligt ofta (R), bör den vara tillåten att få resursen (C) oändligt ofta:

$\bigwedge (GFR\longrightarrow GFC)$

Modellkontroll för rättvis CTL

Betrakta en Kripke-modell med uppsättning tillstånd F . En sökväg $\pi =s_{o},s_{1}\dots$ anses vara en rättvis väg , om och bara om sökvägen inkluderar alla medlemmar av F oändligt ofta. Rättvis CTL- modellkontroll begränsar kontrollerna till endast rättvisa vägar. Det finns två typer av rättvisa kvantifierare:

1. M _f , s _i |= A $\phi$ om och endast om $\phi$ gäller i alla rättvisa banor.

2. M _f , s _i |= E $\phi$ om och endast om $\phi$ håller i en eller flera rättvisa banor.

En rättvis stat är en från vilken åtminstone en rättvis väg kommer. Detta översätts till Mf _, s |= EGtrue.

SCC-baserat tillvägagångssätt

En starkt ansluten komponent (SCC) i en riktad graf är en maximal starkt ansluten subgraf – alla noder kan nås från varandra. En rättvis SCC är en som har en kant i minst en nod för vart och ett av de rättvisa förhållandena.

För att kontrollera rättvis EG för någon formel,

1. Beräkna vad som kallas beteckningen av formeln φ : mängden tillstånd så att M, s |= φ .
2. Begränsa modellen till beteckningen.
3. Hitta mässan SCC.
4. Få föreningen av alla 3 (ovan).
5. Beräkna de stater som kan nå facket.

Emerson Lei algoritm

Fixpunktskarakteriseringen av Exist Globally ges av: [EGφ] = νZ .([φ] ∩ [EXZ ]), vilket i princip är den gräns som tillämpas enligt Kleenes sats . För rättvisa banor blir det [Ef Gφ] = νZ .([φ] ∩ _{Fi ∈FT} [EX[E(ZU(Z ∧ Fi ))]), vilket betyder att formeln håller i det nuvarande tillståndet och nästa tillstånd och nästa till nästa stater tills den uppfyller alla medlemmar av mässvillkoren. Detta betyder att villkoret är likvärdigt med en sorts acceptanspunkt där det accepterande villkoret är hela uppsättningen av rättvisa villkor.

• Emerson, EA; Halpern, JY (1985). "Beslutsprocedurer och uttrycksfullhet i den tidsmässiga logiken för förgrening av tid" . Tidskrift för data- och systemvetenskap . 30 (1): 1–24. doi : 10.1016/0022-0000(85)90001-7 .
• Clarke, EM ; Emerson, EA & Sistla, AP (1986). "Automatisk verifiering av samtidiga system i finita tillstånd med hjälp av tidslogikspecifikationer". ACM-transaktioner på programmeringsspråk och system . 8 (2): 244–263. doi : 10.1145/5397.5399 .