Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Probabilistic Computation Tree Logic (PCTL) is frequently used to formally specify control objectives such as probabilistic reachability and safety. In this work, we focus on model checking PCTL specifications statistically on Markov Decision Processes (MDPs) by sampling, e.g., checking whether there exists a feasible policy such that the probability of reaching certain goal states is greater than a threshold. We use reinforcement learning to search for such a feasible policy for PCTL specifications, and then develop a statistical model checking (SMC) method with provable guarantees on its error. Specifically, we first use upper-confidence-bound (UCB) based Q-learning to design an SMC algorithm for bounded-time PCTL specifications, and then extend this algorithm to unbounded-time specifications by identifying a proper truncation time by checking the PCTL specification and its negation at the same time. Finally, we evaluate the proposed method by case studies.

Original languageEnglish (US)
Title of host publication2020 59th IEEE Conference on Decision and Control, CDC 2020
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1392-1397
Number of pages6
ISBN (Electronic)9781728174471
DOIs
StatePublished - Dec 14 2020
Event59th IEEE Conference on Decision and Control, CDC 2020 - Virtual, Jeju Island, Korea, Republic of
Duration: Dec 14 2020Dec 18 2020

Publication series

NameProceedings of the IEEE Conference on Decision and Control
Volume2020-December
ISSN (Print)0743-1546

Conference

Conference59th IEEE Conference on Decision and Control, CDC 2020
Country/TerritoryKorea, Republic of
CityVirtual, Jeju Island
Period12/14/2012/18/20

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Modeling and Simulation
  • Control and Optimization

Fingerprint

Dive into the research topics of 'Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning'. Together they form a unique fingerprint.

Cite this