Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates

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