کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
7109770 1460660 2015 14 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Symbolic models for stochastic switched systems: A discretization and a discretization-free approach
ترجمه فارسی عنوان
مدل های نمادین برای سیستم های سوئیچ تصادفی: یک تقسیم بندی و یک رویکرد رایگان است
کلمات کلیدی
سیستم های ترکیبی استاکاستیک، سیستم های تصحیح تصادفی، سنتز رسمی، انتزاع انتزاعی، مدل های نمادین
ترجمه چکیده
سیستم های سوئیچ تصادفی یک کلاس مربوطه از سیستم های هیبرید تصادفی با تکامل احتمالی در یک دامنه پیوسته و پویایی گسسته وابسته به کنترل است که در یک حالت محدود از مجموعه محدود است. در چند سال گذشته، تکنیک های مختلفی برای کمک به تجزیه و تحلیل ثبات سیستم های سوئیچ تصادفی توسعه داده شده است. با این حال، اهداف پیچیده تر و چالش برانگیز مربوط به تأیید و سنتز کنترل کننده برای مشخصات منطقی تاکنون هنوز برای این کلاس سیستم ها مورد بررسی قرار نگرفته است. با مشخصات منطقی، به معنی خواص بیان شده به صورت فرمول در منطق زمانی خطی یا به عنوان خودکار در رشته های بی نهایت است. این مقاله با استفاده از ساختار تقریبا معادل (بی نظم) مدل های نمادین از سیستم های سوئیچ تصادفی، به این اهداف پیچیده می پردازد. دقیق تر، این مقاله دو تکنیک انتزاعی نمادین را ارائه می دهد: یکی نیاز به فریب سازی فضای حالت دارد، اما دیگری نیازی به فریب سازی فضا نیست که می تواند به طور بالقوه کارآمدتر از اولین کار با سیستم های سوئیچ شده است. هر دو تکنیک مدل های سمبلیک محدودی را ارائه می دهند که تقریبا مشابه با سیستم های سوئیچ تصادفی تحت برخی پیش فرض های ثبات در مدل بتن هستند. این اجازه می دهد تا به طور رسمی سینتیزه کردن کنترل کننده ها (سیگنال های سوئیچینگ) که برای سیستم بتن بر پایه مدل نمادین محدود، با استفاده از تکنیک های بالقوه تئوری اتوماتیک در ادبیات، معتبر باشد. اثربخشی نتایج با استفاده از سنتز سیگنالهای سوئیچینگ که به ارائه مشخصات منطقی برای دو مطالعه موردی از جمله کنترل دما در یک ساختمان شش اتاق کمک می کند، نشان داده شده است.
موضوعات مرتبط
مهندسی و علوم پایه سایر رشته های مهندسی کنترل و سیستم های مهندسی
پیش نمایش مقاله
مدل های نمادین برای سیستم های سوئیچ تصادفی: یک تقسیم بندی و یک رویکرد رایگان است
چکیده انگلیسی
Stochastic switched systems are a relevant class of stochastic hybrid systems with probabilistic evolution over a continuous domain and control-dependent discrete dynamics over a finite set of modes. In the past few years several different techniques have been developed to assist in the stability analysis of stochastic switched systems. However, more complex and challenging objectives related to the verification of and the controller synthesis for logic specifications have not been formally investigated for this class of systems as of yet. With logic specifications we mean properties expressed as formulae in linear temporal logic or as automata on infinite strings. This paper addresses these complex objectives by constructively deriving approximately equivalent (bisimilar) symbolic models of stochastic switched systems. More precisely, this paper provides two different symbolic abstraction techniques: one requires state space discretization, but the other one does not require any space discretization which can be potentially more efficient than the first one when dealing with higher dimensional stochastic switched systems. Both techniques provide finite symbolic models that are approximately bisimilar to stochastic switched systems under some stability assumptions on the concrete model. This allows formally synthesizing controllers (switching signals) that are valid for the concrete system over the finite symbolic model, by means of mature automata-theoretic techniques in the literature. The effectiveness of the results are illustrated by synthesizing switching signals enforcing logic specifications for two case studies including temperature control of a six-room building.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Automatica - Volume 55, May 2015, Pages 183-196
نویسندگان
, , ,