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

منطق درخت محاسباتی ( به انگلیسی: Computation Tree Logic ) یک منطق زمانی است؛ که در آن حالت های مختلف سامانه، به صورت راس های یک ماشین حالت وجود دارند. این ماشین حالت، به صورت یک درخت زمانی است؛ که هر مجموعه حالت های سامانه در طول زمان ( تاریخچه آن سامانه ) متناظر یک مسیر با شروع از ریشهٔ درخت است. مزیت این منطق بر منطق های مشابه؛ مثل منطق خطی زمانی، این است که می توان یک مسیر خاص را مشخص کرد. برای مثال این جملات در این منطق ( منطق درخت محاسباتی ) قابل بیان هستند:
• حتماً به حالتی خواهیم رسید که در آن شرط q {\displaystyle q} برقرار است.
• اگر در حالتی باشیم که q {\displaystyle q} درست باشد، ممکن نیست در آینده p {\displaystyle p} برقرار شود.
• اگر حالتی باشد که q {\displaystyle q} درست نباشد، از آن به بعد همواره p {\displaystyle p} درست است.
منطق کلی این منطق، این است که در هر لحظه، ممکن است آینده های متفاوتی داشته باشیم؛ لذا این درخت نامتناهی، تمامی حالت های ممکن برای سامانه را در طول زمان نشان می دهد. ابداع اولیهٔ آن توسط Clarke و Emerson در سال ۱۹۸۱ بوده و پس از آن، Queille و Sifakis با کمی تفاوت، از آن در وارسی مدل ها استفاده کردند. به علت سادگی، کارایی و گستردگی کاربرد این منطق، امروزه در بسیاری از روش های درستی یابی سیستم ها از آن استفاده می شود. [ ۱]
اگر A P مجموعهٔ متغیرهای منطقی باشد، فرمول های حالت منطق درخت محاسباتی به این صورت تعریف می شوند:
که در آن، a ∈ A P ، ϕ 1 , ϕ 2 یک فرمول حالت و γ یک فرمول مسیر است.
فرمول های مسیر هم این گونه تعریف می شوند:
که در آن، ϕ 1 , ϕ 2 فرمول های حالت هستند. البته در این جا، ما یک تعریف مینیمال ارائه دادیم و تعاریف معادلی با استفاده از دیگر عملگرهای زمانی وجود دارد. برای مثال، جملات زیر در منطق درخت محاسباتی هستند:
فرض کنید M = ( S , → , L ) یک مدل برای منطق درخت محاسباتی باشد. یعنی M یک سیستم جابجایی است که مجموعهٔ حالت های آن S ، جابجایی ها → ( که همان قواعد جابجایی از یک حالت به حالت دیگر است ) و L نیز مجموعه ای است که نشان می دهد در هر حالت کدام یک از متغیرهای منطقی عضو A P درست هستند. [ ۲] حال معنای یک عبارت در منطق روی این مدل و با حالت شروع s ، برای فرمول های حالت به صورت استقرایی با قواعد زیر مشخص می شود: