در حالی که در MTL خیلی راحت تر بیان می شود . در این روش دو سطح از بیان وجود دارد ، یکی سطح کاربر است که برنامه منطقی را تولید می کند ، وی در سطح MTL برنامه خود را طراحی می کند "اگر جایی کپی می کنید منبع را هم ذکر کنید !" اما برای تجزیه تحلیل منطقی ، سطح MTL می بایست به سطح پایین تری تبدیل شود . این تبدیل که کار دشواری است باعث می شود از نظر کارایی این روش دچار مشکل شود و برای تفسیرهای پیچیده بسیار زمان بر باشد و منابع زیادی مصرف شود .
در شکل زیر تمامی اپراتورهایی که برای MTL طراحی شده است را مشاهده می کنید .
توسعه هایی برای راحتی بیان : به غیر از روش آرگومان و MTL می توان با استفاده از برخی predicate ها زمان را به روشی آسان تر برای کاربر تعریف کرد . در این حالت از predicateی به نام >قید زمانی , جمله مستقل از زمان TRUE<می توان استفاده کرد که آرگومان اول طی مدت آرگومان دوم درست است برای مثال TRUE<Happy(hamed),1April> .
مشکلی که این روش دارد تعریف دقیق آرگومان زمان است . در مثال قبل این سوالها قابل بیان است
- حامد در طول روز خوشحال است ؟
- حامد فقط مدتی از آن روز خوشحال است ؟
- حامد کل April خوشحال بوده ، که 1هم جزو آن است ؟
آرگومانهای زمانی دارای مشکلی به نام Temporal Occurrence Pattern هستند . این مشکل از نحوه تعریف نوع رخداد آرگومان زمان ناشی می شود که سه سوالی که نمونه اش ذکر شد نشان دهنده ابهام در تعریف زمان است .
یک نمونه دیگر از توسعه هایی که برای راحتی بیان ذکر شده HOLDS است . بدین معنی که در مدت زمان T ، عبارت p صحیح می باشد .
نمونه دیگر INCOMPATIBLE است که برای بیان دو رخدادی که همزمان نمی توانند رخ دهند کاربرد دارد .
Predicate دیگری که برای راحتی بیان ایجاد شده است CAUSES است . از این predicate برای بیان رخدادهایی که با هم رابطه علت و معلول دارند می توان استفاده کرد .
دیدگاه دوم
در این دیدگاه روشهایی بیان می شود که ساده سازی هایی در آن انجام شده تا بتوان از آنها در نرم افزارهای منطقی استفاده کرد .
Linear Temporal Logic : در این روش ، زمان ، گسسته مانند دنباله ای از اعداد صحیح فرض می شود . همانطور که پیش تر دیدیم ، آینده را می توان به شکل انشعابی یا خطی دید ، در روش LTL آینده خطی است . یعنی برای زمان حال فقط یک آینده قابل تصور است .
اپراتورهایی که برای LTL تعریف شده عبارتست از :
به ترتیب عبارتند از :
- Next یا بعدی : بدین معنی که عبارت مورد نظر دقیقا ً در اولین زمان بعد از حال درست باشد . تعریف رسمی برای Next عبارتست از :
- All یا همه : به این معنی که عبارت مورد نظر در کلیه زمانهای آینده درست باشد .
- Some یا تعدادی : به این معنی که عبارت مورد نظر در بعضی از زمانهای آینده درست باشد . تعریف رسمی :
- Until : به این معنی است که عبارت اول درست است تا زمانی که عبارت دوم درست شود .
برای مثال :
اگر در زمان حال بلیط و پاسپورت وجود دارد ، در زمان بعدی سوار هواپیما نمی توان بود و کل این عبارت برای همه زمانهای آینده درست است .
اگر درخواستی ارسال شده باشد ، در زمانی در آینده توسط گیرنده دریافت خواهد شد و این عبارت برای همه زمانهای آینده درست خواهد بود .
اگر شخصی به دنیا آمده باشد ، زنده است تا وقتی که بمیرد .
کسی که در قرعه کشی برنده شود ، در زمانهای بعد از برنده شدن ثروتمند خواهد بود .
M اگر در شرایط زیر صدق کند مدل خواهد بود .
که
مجموعه قابل شمارش از اتمهاست و
که نگاشتی از مجموعه اعداد طبیعی (زمان) به مجموعه یی از گزاره ها می باشد .
روابط کلاسیک در اپراتورهای LTL درست هستند .
Computation Tree Logic : این روش بسیار شبیه روش LTL است بیشترین تفاوتی وجود دارد در نگاه آن به آینده است . هنگامی که آینده ی زمان حال دارای چند انشعاب باشد و "اگر جایی کپی می کنید منبع را هم ذکر کنید !" بتوان چندین آینده را برای اکنون تصور کرد از این روش استفاده می شود . CTL دو اپراتور بیشتر از LTL دارد که از ترکیب هر دوی این اپراتورها با LTL استفاده می شود.
فرض کنید در نقطه شروع قرار داریم ، می خواهیم درستی عبارتی را در تمامی انشعاب های آینده مشخص کنیم . در این حالت از اپراتور A استفاده می شود . اگر بخواهیم مشخص کنیم که درستی عبارت در بعضی از مسیرهای آینده برقرار است از E استفاده می شود . به طور خلاصه :
به عنوان مثال مفهوم عبارت زیر
این چنین است : این همیشه درست است که ، اگر P درست باشد ، آنگاه وجود دارد مسیری در آینده که در زمانی از آن q درست باشد .
سیستم های انتقالی
یکی از مهمترین کاربردهای منطق Temporal در سیستم هایی است که به نحوی بر اساس رویدادهایی از یک حالت به حالت دیگر منتقل می شوند . مثلا ً کامپیوتر آسانسور باید در یک تصمیم گیری منطقی با توجه به حالت فعلی و درخواست های رسیده حالت بعدی خود را انتخاب کرده و به سمت آن حرکت کند .
سیستم های انتقالی با یک سه تایی نمایش داده می شوند M = (S,R,L)
- R : رابطه دودویی بین حالت ها
- L : تابع برچسب زنی که در هر کدام از حالت ها گزاره های درست را مشخص می کند .
برای مثال در شکل زیر سیستم داری سه حالت است و در هر حالت تعدادی از متغیر ها True ارزیابی می شوند که عناوین آنها در L آمده است . برای حرکت از هر حالت به حالت دیگر هم قوانین مشخصی دارد که در R مشخص شده .
با استفاده از منطق Temporal می توان درستی حالت های مختلفی که سیستم می تواند در آنها قرار بگیرد را سنجید . برای مثال در شکل زیر یک سیستم انتقالی مشخص شده است . می خواهیم بدانیم آیا اگر در حال حاضر در حالت S0 باشیم ، عبارت زیر درست ارزیابی خواهد شد یا مقدار آن false خواهد بود .
مفهوم عبارت فوق این است که : اگر هم اکنون در S0 باشیم ، آیا مسیری وجود دارد که حالت بعدی آن شامل p نباشد ؟ دو حالت بعدی S0 ، گره های S1 و S2 هستند که هیچ کدام p ندارند ، پس عبارت فوق به True ارزیابی می شود .
منابع- A survey on Temporal Reasoning in AI , Llus Vila
- Formal Methods , Lecture III: Linear Temporal Logic , Alessandro Artale
- Wikipedia
- The temporal logic CTL , A gentle introduction , F. Raimondi
- Temporal Logic Tutorial , Edsko de Vries 2006
اگر جایی کپی می کنید منبع را هم ذکر کنید !