ตรรกะต้นไม้การคำนวณเชิงความน่าจะเป็น (PCTL) เป็นส่วนขยายของตรรกะต้นไม้การคำนวณ (CTL) ที่อนุญาตให้มีการกำหนดปริมาณเชิงความน่าจะเป็น ของคุณสมบัติที่อธิบายไว้ ได้รับการกำหนดไว้ในบทความโดย Hansson และ Jonsson ^{[ 1 ]}

PCTL เป็นตรรกะ ที่มีประโยชน์ สำหรับการระบุคุณสมบัติของกำหนดเวลาที่ไม่เข้มงวด เช่น "หลังจากได้รับการร้องขอบริการแล้ว มีโอกาสอย่างน้อย 98% ที่บริการนั้นจะดำเนินการเสร็จภายใน 2 วินาที" เช่นเดียวกับ CTL ที่เหมาะสมสำหรับการตรวจสอบแบบจำลองส่วนขยายของ PCTL ถูกนำมาใช้กันอย่างแพร่หลายในฐานะภาษาสำหรับการระบุคุณสมบัติสำหรับตัวตรวจสอบแบบจำลองเชิงความ น่าจะเป็น

รูปแบบไวยากรณ์ที่เป็นไปได้ของ PCTL สามารถกำหนดได้ดังนี้:

ในนั้นสำหรับเซตจำกัดของประพจน์อะตอมิกจะมีตัวดำเนินการเปรียบเทียบ และจะมีเกณฑ์ความน่าจะเป็น สูตรของ PCTL จะถูกตีความบนลูกโซ่ Markov แบบไม่ต่อเนื่อง โครงสร้างการตีความคือควอดรูเพิลโดยที่ ${\displaystyle a\in A}$${\displaystyle A}$${\displaystyle \sim \in \{<,\leq ,\geq ,>\}}$${\displaystyle \lambda }$${\displaystyle K=\langle S,s^{i},{\mathcal {T}},L\rangle }$

• ${\displaystyle S}$เป็นเซตของสถานะ ที่มีจำนวนจำกัด
• ${\displaystyle s^{i}\in S}$เป็นสถานะเริ่มต้น
• ${\displaystyle {\mathcal {T}}}$เป็นฟังก์ชันความน่าจะเป็นของการเปลี่ยนสถานะโดยที่สำหรับทุกค่าเรามีและ${\displaystyle {\mathcal {T}}:S\times S\to [0,1]}$${\displaystyle s\in S}$${\displaystyle \sum _{s'\in S}{\mathcal {T}}(s,s')=1}$
• ${\displaystyle L}$เป็นฟังก์ชันการติดป้ายกำกับซึ่งกำหนดข้อเสนอเชิงอะตอมให้กับสถานะต่างๆ${\displaystyle L:S\to 2^{A}}$

เส้นทางจากสถานะหนึ่งไปยังอีกสถานะหนึ่งคือลำดับอนันต์ของสถานะต่างๆ สถานะที่ n ของเส้นทางจะถูกแทนด้วย และส่วนนำหน้าของเส้นทางที่มีความยาว จะ ถูก แทนด้วย${\displaystyle \sigma }$${\displaystyle s_{0}}$${\displaystyle s_{0}\to s_{1}\to \dots \to s_{n}\to \dots }$${\displaystyle \sigma [n]}$${\displaystyle \sigma }$${\displaystyle n}$${\displaystyle \sigma \uparrow n}$

การวัดความน่าจะเป็นบนเซตของเส้นทางที่มีคำนำหน้าความยาวร่วมกันนั้น กำหนดโดยผลคูณของความน่าจะเป็นของการเปลี่ยนผ่านตามคำนำหน้าของเส้นทาง: ${\displaystyle \mu _{m}}$${\displaystyle n}$

${\displaystyle \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})}$

เนื่องจากค่าการวัดความน่าจะเป็นเท่ากับ. ${\displaystyle n=0}$${\displaystyle \mu _{m}(\{\sigma \in X:\sigma \uparrow 0=s_{0}\})=1}$

ความสัมพันธ์ของความพึงพอใจถูกกำหนดโดยวิธีอุปนัยดังนี้: ${\displaystyle s\models _{K}f}$

• ${\displaystyle s\models _{K}a}$ก็ต่อเมื่อ,${\displaystyle a\in L(s)}$
• ${\displaystyle s\models _{K}\neg f}$ถ้าและเฉพาะในกรณีที่ไม่เป็นเช่นนั้น${\displaystyle s\models _{K}f}$
• ${\displaystyle s\models _{K}f_{1}\lor f_{2}}$ก็ต่อเมื่อหรือเท่านั้น${\displaystyle s\models _{K}f_{1}}$${\displaystyle s\models _{K}f_{2}}$
• ${\displaystyle s\models _{K}f_{1}\land f_{2}}$ก็ต่อเมื่อและ,${\displaystyle s\models _{K}f_{1}}$${\displaystyle s\models _{K}f_{2}}$
• ${\displaystyle s\models _{K}{\mathcal {P}}_{\sim \lambda }(f_{1}{\mathcal {U}}f_{2})}$ก็ต่อเมื่อและ${\displaystyle \mu _{m}(\{\sigma :\sigma [0]=s\land (\exists i)\sigma [i]\models _{K}f_{2}\land (\forall 0\leq j<i)\sigma [j]\models _{K}f_{1}\})\sim \lambda }$
• ${\displaystyle s\models _{K}{\mathcal {P}}_{\sim \lambda }(\square f)}$ก็ต่อเมื่อ...${\displaystyle \mu _{m}(\{\sigma :\sigma [0]=s\land (\forall i\geq 0)\sigma [i]\models _{K}f\})\sim \lambda }$

• ตรรกะต้นไม้การคำนวณ
• ตรรกะเชิงเวลา