منطق درخت محاسباتی

منطق درخت محاسباتی (به انگلیسی: Computation Tree Logic) یک منطق زمانی است؛ که در آن حالت‌های مختلف سامانه، به صورت راس‌های یک ماشین حالت وجود دارند. این ماشین حالت، به صورت یک درخت زمانی است؛ که هر مجموعه حالت‌های سامانه در طول زمان (تاریخچه آن سامانه) متناظر یک مسیر با شروع از ریشهٔ درخت است. مزیت این منطق بر منطق‌های مشابه؛ مثل منطق خطی زمانی، این است که می‌توان یک مسیر خاص را مشخص کرد. برای مثال این جملات در این منطق(منطق درخت محاسباتی) قابل بیان هستند:

حتماً به حالتی خواهیم رسید که در آن شرط $q$ برقرار است.
اگر در حالتی باشیم که $q$ درست باشد، ممکن نیست در آینده $p$ برقرار شود.
اگر حالتی باشد که $q$ درست نباشد، از آن به بعد همواره $p$ درست است.

منطق کلی این منطق، این است که در هر لحظه، ممکن است آینده‌های متفاوتی داشته باشیم؛ لذا این درخت نامتناهی، تمامی حالت‌های ممکن برای سامانه را در طول زمان نشان می‌دهد. ابداع اولیهٔ آن توسط Clarke و Emerson در سال ۱۹۸۱ بوده و پس از آن، Queille و Sifakis با کمی تفاوت، از آن در وارسی مدل‌ها استفاده کردند. به علت سادگی، کارایی و گستردگی کاربرد این منطق، امروزه در بسیاری از روش‌های درستی‌یابی سیستم‌ها از آن استفاده می‌شود.^[۱]

قواعد لغوی

اگر $AP$ مجموعهٔ متغیرهای منطقی باشد، فرمول‌های حالت منطق درخت محاسباتی به این صورت تعریف می‌شوند:

{\begin{aligned}\phi &::=\top \mid a\mid (\neg \phi _{1})\mid (\phi _{1}\land \phi _{2})\mid \exists {\gamma }\mid \forall \gamma \end{aligned}}

که در آن، $a\in AP$ ، $\phi _{1},\phi _{2}$ یک فرمول حالت و $\gamma$ یک فرمول مسیر است.

فرمول‌های مسیر هم این‌گونه تعریف می‌شوند:

{\begin{aligned}\gamma &::=X\phi \mid \phi _{1}U\phi _{2}\end{aligned}}

که در آن، $\phi _{1},\phi _{2}$ فرمول‌های حالت هستند. البته در این‌جا، ما یک تعریف مینیمال ارائه دادیم و تعاریف معادلی با استفاده از دیگر عملگرهای زمانی وجود دارد. برای مثال، جملات زیر در منطق درخت محاسباتی هستند:

{\begin{aligned}\exists X(x=1),\forall X(x=1),and\;x<2\lor x=1\end{aligned}}

قواعد معنایی

فرض کنید $M=(S,\rightarrow ,L)$ یک مدل برای منطق درخت محاسباتی باشد. یعنی $M$ یک سیستم جابجایی است که مجموعهٔ حالت‌های آن $S$ ، جابجایی‌ها $\rightarrow$ (که همان قواعد جابجایی از یک حالت به حالت دیگر است) و $L$ نیز مجموعه‌ای است که نشان می‌دهد در هر حالت کدام‌یک از متغیرهای منطقی عضو $AP$ درست هستند.^[۲] حال معنای یک عبارت در منطق روی این مدل و با حالت شروع $s$ ، برای فرمول‌های حالت به صورت استقرایی با قواعد زیر مشخص می‌شود:

${\Big (}({\mathcal {M}},s)\models \top {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}$
${\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}$
${\Big (}({\mathcal {M}},s)\models \neg \phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \phi {\Big )}$
${\Big (}({\mathcal {M}},s)\models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}$

و اما برای فرمول‌های مسیر، برای مسیر $\pi$ در این سیستم جابجایی، به صورت زیر:

${\Big (}({\mathcal {M}},\pi )\models X\phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},\pi [1])\models \phi {\Big )}$
${\Big (}({\mathcal {M}},\pi )\models \phi _{1}U\phi _{2}{\Big )}\Leftrightarrow {\Big (}\exists {j\geq 0}.(({\mathcal {M}},\pi [j])\models \phi _{2}\land (0\leq k<j.({\mathcal {M}},\pi [k])\models \phi _{1})){\Big )}$

مثال‌ها

فرض کنید سامانه‌ای داشته باشیم که بتواند حالت‌های ready یا started را داشته باشد. حال می‌توانیم بیان کنیم «ممکن است زمانی برسد که started درست باشد اما ready غلط». این عبارت به صورت $E\;\top U(started\land \neg ready)$ است. یا برای مثال، اگر بخواهیم بیان کنیم ready هیچ‌گاه درست نمی‌شود، به صورت $\neg E\;ready$ است.

ارتباط با دیگران منطق‌ها

همان‌طور که منطق درخت محاسباتی یک منطق زمانی است، منطق خطی زمانی نیز شباهت‌های بسیاری با آن دارد. تفاوت در این‌جاست که در منطق خطی زمانی، امکان مشخص کردن یک مسیر به‌طور خاص وجود ندارد و احکام بیان‌شده در مورد همه یا هیچ‌یک از مسیرهای ممکن است. هرچند عباراتی وجود دارند که فقط در منطق درخت محاسباتی یا فقط در منطق خطی زمانی قابل بیان هستند، هر دوی این منطق‌ها زیرمجموعهٔ منطق CTL* هستند که در آن زبان جملات بیشتری قابل بیان هستند هرچند وارسی مدل‌ها سخت‌تر و پیچیده‌تر از لحاظ محاسباتی است.

منابع

↑ E.M. Clarke; E.A. Emerson (1981). "Design and synthesis of synchronisation skeletons using branching time temporal logic". Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science, vol. 131. Springer, Berlin: 52–71.
↑ Michael Huth; Mark Ryan (2004). "Logic in Computer Science (Second Edition)". Cambridge University Press: 207. ISBN 0-521-54310-X. {{cite journal}}: Cite journal requires |journal= (help)

Micheal Huth, Mark Ryan, Logic in Computer Science, Modeling and reasoning about systems, Cambridge University Press, 2004. ISBN 978-0-511-26401-6
Christel Baier, Joost-Pieter Katoen, Principles of Model Checking, The MIT Press 2007. ISBN 978-0-262-02649-9
Emerson, E. A. "Temporal and modal logic". In Jan van Leeuwen (ed.). Handbook of Theoretical Computer Science, vol. B. MIT Press. pp. 955–1072. ISBN 0-262-22039-3.

این یک مقالهٔ خرد منطق است. می‌توانید با گسترش آن به ویکی‌پدیا کمک کنید.

[1] E.M. Clarke; E.A. Emerson (1981). "Design and synthesis of synchronisation skeletons using branching time temporal logic". Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science, vol. 131. Springer, Berlin: 52–71.

[2] Michael Huth; Mark Ryan (2004). "Logic in Computer Science (Second Edition)". Cambridge University Press: 207. ISBN 0-521-54310-X. {{cite journal}}: Cite journal requires |journal= (help)

[۱]

[۲]