Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games

ما مساله محاسبه مجموعه ای از حالت های اولیه یک سیستم دینامیکی را در نظر می گیریم به طوری که یک استراتژی کنترل وجود دارد تا اطمینان حاصل شود که مسیرها یک الگوریتم منطقی با احتمال 1 (تقریبا مطمئن) را برآورده می کنند. ما بر روی زمان گسسته، دینامیک خطی تصادفی و مشخصات داده شده به عنوان فرمول از بخش واکنش پذیری عمومی (1) منطق زمان منطقی بر پیش فرض های خطی در حالت سیستم تمرکز می کنند. ما یک راه حل مبتنی بر تکمیل انتزاعی تکراری و بازی های احتمال احتمالی 2 بازیکن را به شما پیشنهاد می کنیم. در حالی که تضمین نظری الگوریتم ما پس از هر تعداد محدود تکرار فقط یک راه حل جزئی است، ما نشان می دهیم که اگر الگوریتم ما متوقف شود، نتیجه مجموعه ای از تمام حالت های رضایت بخش اولیه است. علاوه بر این، برای راه حل (جزئی)، الگوریتم ما شاهد استراتژی های کنترل شاهدانه برای اطمینان از رضایت تقریبا مطمئن از مشخصات منطق زمانی است. در حالی که الگوریتم پیشنهادی پیشرفت و صدا را در هر تکرار تضمین می کند، از نظر محاسباتی خواسته شده است. ما یک راه حل جایگزین، کارآمدتری را برای خواص دستیابی ارائه می دهیم که این مسئله را به یک سری مشکلات کوچکتر از همان نوع تجزیه می کند. تمام الگوریتم ها بر روی یک مطالعه موردی نشان داده شده است.