ارائه الگوریتمی جهت تسریع روش تکرار سیاست در وارسی مدل فرآیندهای تصمیم مارکوف با استفاده از یادگیری ماشین

نوع مقاله : مقاله پژوهشی

نویسنده

گروه علوم کامپیوتر، دانشکده علوم ریاضی، دانشگاه ولیعصر رفسنجان، رفسنجان، ایران

چکیده

فرآیندهای تصمیم مارکوف (MDPs) در هوش مصنوعی و راستی‌آزمایی رسمی برای مدلسازی سیستم‌های کامپیوتری که دارای رفتارهای تصادفی و غیرقطعی هستند استفاده می‌شوند. دو دسته مهم از ویژگی‌هایی که در وارسی مدل احتمالاتی استفاده می‌شوند شامل احتمال بهینه (بیشنه یا کمینه) رسیدن به حالت هدف و پاداش‌ انباشته شده بهینه تا رسیدن به هدف هستند. تکرار مقدار و تکرار سیاست دو روش عددی تکراری شناخته شده برای تقریب مقادیر بهینه مورد نیاز هستند. یکی از ایرادات اساسی این روش‌ها زمان اجرایی بالای آنهاست. در این مقاله روشی جدید برای تسریع همگرایی به سیاست بهینه ارائه می‌شود که زمان اجرایی روش تکرار سیاست را کاهش می‌دهد. این روش بر پایه استفاده از یادگیری ماشین برای تخمین یک سیاست‌ نزدیک به بهینه است. برای هر کلاس از مدل‌های MDP, تعدادی مدل کوچک را برای مرحله آموزش و ساخت دسته‌بند در نظر می‌گیریم. دسته‌بند ساخته شده در فرآیند یادگیری، برای پیش‌بینی کنش بهینه هر حالت MDP داده شده به کار می‌رود تا یک سیاست نزدیک به بهینه را ارائه دهد. این دسته‌بند برای MDP های بزرگ از همان دسته مدل‌ها قابل استفاده است تا با پیشنهاد یک سیاست مناسب، زمان مصرفی کل را کاهش دهد. پیاده سازی روش ارائه شده در وارسی‌گر مدل PRISM نشان می‌دهد زمان اجرا می‌تواند تا 90 درصد کاهش ‌یابد.

کلیدواژه‌ها

موضوعات


عنوان مقاله [English]

A new approach to accelerate policy iteration for probabilistic model checking of Markov decision processes using machine learning

نویسنده [English]

  • Mohammadsadegh Mohagheghi
Department of Computer science, Faculty of Mathematical science, Vali-e-Asr university of Rafsanjan, Rafsanjan, Iran
چکیده [English]

Markov decision processes (MDPs) are used in artificial intelligence and formal verification to model computer systems with nondeterministic and stochastic behaviors. Optimal reachability probabilities and expected accumulated rewards are two main classes of properties that are used in probabilistic model checking. Value iteration and policy iteration are two well-known iterative numerical methods to approximate the optimal values. A main challenge of these approaches is their high running time. In this paper, a new method is proposed for accelerating the convergence to the optimal policy. This method is based on using machine learning to estimate optimal policies. For each class of MDP models, we consider several small models for the training and construction step of the classifier model. The classifier model is used to predict the optimal actions of each MDP model and for suggesting a near optimal policy for large models of the same MDP class. Implementing the proposed method in the PRISM model checker shows a 50% improvement in the average runtime.

کلیدواژه‌ها [English]

  • Formal verification
  • probabilistic model checking
  • Markov decision processes
  • maximal reachability probabilities
  • policy iteration
  • machine learning