Probabilistisk CTL

Probabilistic Computation Tree Logic (PCTL) är en förlängning av Computation Tree Logic (CTL) som möjliggör probabilistisk kvantifiering av beskrivna egenskaper. Det har definierats i tidningen av Hansson och Jonsson.

PCTL är en användbar logik för att ange egenskaper för mjuka deadline, t.ex. "efter en begäran om en tjänst finns det minst 98 % sannolikhet att tjänsten kommer att utföras inom 2 sekunder". Liknande CTL-lämplighet för modellkontroll PCTL-tillägg används i stor utsträckning som ett egenskapsspecifikationsspråk för probabilistiska modellcheckare.

PCTL-syntax

En möjlig syntax för PCTL kan definieras enligt följande:

$\n:eg=p\midten phi \lor \phi \mid \phi \land \phi \mid {\mathcal {P}}_{\sim \lambda }(\phi {\mathcal {U}}\phi )\mid {\mathcal {P} }_{\sim \lambda }(\square \phi )$

Däri $\sim \in \{<,\leq ,\geq ,>\}$ en jämförelseoperator och $\lambda$ är en sannolikhetströskel . Formler för PCTL tolkas över diskreta Markov-kedjor . En tolkningsstruktur är en fyrdubbel ${\displaystyle K=\langle S,s^{i},{\mathcal {T}},L\rangle } ,$ där

• $S$ är en ändlig uppsättning tillstånd,
• $s^{i}\in S$ är ett initialtillstånd,
• ${\mathcal {T}}$ är en övergångssannolikhetsfunktion, ${\mathcal {T}}:S\times S\to [0,1]$ , så att vi för alla ${\displaystyle s\in S} har$$\sum _{s'\in S}{\mathcal { T}}(s,s')=1$ , och
• $L$ är en märkningsfunktion, $L:S\to 2^{A}$ , som tilldelar atomära propositioner till tillstånd.

En sökväg $\sigma$ från ett tillstånd $s_{0}$ är en oändlig sekvens av tillstånd $s_{0}\to s_{1 }\to \dots \to s_{n}\to \dots$ . Banans n:te tillstånd betecknas som $\sigma [n]$ och prefixet för $\sigma$ av längden $n$ betecknas som ${ \displaystyle \sigma \uparrow n}$ .

Sannolikhetsmått

Ett sannolikhetsmått $\mu _{m}$ på uppsättningen banor med ett gemensamt prefix av längden $n$ ges av produkten av övergångssannolikheter längs prefixet för sökvägen:

$\mu _{m} (\{\sigma \in X:\sigma \uparrow n=s_{0}\to \dots \to s_{n}\})={\mathcal {T}}(s_{0},s_{1} )\times \dots \times {\mathcal {T}}(s_{n-1},s_{n})$

För $n=0$ är sannolikhetsmåttet lika med $\mu _{m}(\{\sigma \in X: \sigma \uparrow 0=s_{0}\})=1$ .

Tillfredsställelse relation

Tillfredsställelserelationen $s\models _{K}f$ definieras induktivt enligt följande:

• $s\models _{K}a$ om och endast om $a\in L(s)$ ,
• $s\models _{K}\neg f$ om och endast om inte $s\models _{K}f$ ,
• $s\models _{K}f_{1}\lor f_{2}$ om och endast om $s\models _{K}f_{ 1}$ eller $s\models _{K}f_{2}$ ,
• $s\models _{K}f_{1}\land f_{2}$ om och endast om $s\models _{K}f_{ 1}$ och $s\models _{K}f_{2}$ ,
• $s\models _{K}{\mathcal {P}}_{\sim \lambda }(f_{1}{\mathcal {U}}f_ {2})$ om och endast om ${\displaystyle \mu _{m}(\{\sigma :\sigma [0]=s\land (\exists i)\sigma [i]\modeller _{K}f_{2}\land ( \forall 0\leq j<i)\sigma [j]\models _{K}f_{1}\})\sim \lambda } ,$ och
• $s\models _{K}{\mathcal {P}}_{\sim \lambda }(\square f)$ om och endast om $\mu _{m}(\{\sigma :\sigma [0]=s\land (\forall i \geq 0)\sigma [i]\models _{K}f\})\sim \lambda$ .

Se även

• Beräkningsträdlogik
• Temporal logik