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

2020-04-01 · Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, Geir E. Dullerud

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 on case studies.

📄 PDF Abstract BibTeX arXiv:2004.00273

Code (0)

등록된 구현이 없습니다.

Tasks

NegationQ-Learningreinforcement-learning Reinforcement Learning Reinforcement Learning (RL)

Methods 이 논문이 사용한 방법론

Q-Learning Q-Learning is an off-policy temporal difference control algorithm: $$Q\left(S\_{t}, A\_{t}\right) \leftarrow Q\left(S\_{t}, A\_{t}\right) + \alpha\left[R_{t+1} +…

Lifted Model Checking for Relational MDPs

2021-06-22 · Wen-Chi Yang, Jean-François Raskin, Luc De Raedt

Probabilistic model checking has been developed for verifying systems that have stochastic and nondeterministic behavior. Given a probabilistic system, a probabilistic model checker takes a property and checks whether or…

model Model-based Reinforcement Learning reinforcement-learning Reinforcement Learning (RL)

Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*

2022-09-06 · Spandan Das, Pavithra Prabhakar

In this paper, we present a Bayesian method for statistical model checking (SMC) of probabilistic hyperproperties specified in the logic HyperPCTL* on discrete-time Markov chains (DTMCs). While SMC of HyperPCTL* using se…

Probabilistic Model Checking of Stochastic Reinforcement Learning Policies

2024-03-27 · Dennis Gross, Helge Spieker

We introduce a method to verify stochastic reinforcement learning (RL) policies. This approach is compatible with any RL algorithm as long as the algorithm and its corresponding environment collectively adhere to the Mar…

model reinforcement-learning Reinforcement Learning Reinforcement Learning (RL)

Learning Probabilistic Temporal Safety Properties from Examples in Relational Domains

2022-11-07 · Gavin Rens, Wen-Chi Yang, Jean-François Raskin, Luc De Raedt

We propose a framework for learning a fragment of probabilistic computation tree logic (pCTL) formulae from a set of states that are labeled as safe or unsafe. We work in a relational setting and combine ideas from relat…

Relational Reasoning

Synthesis of Safety Specifications for Probabilistic Systems

2025-11-20 · Gaspard Ohlmann, Edwin Hamel-De le Court, Francesco Belardinelli arxiv

Ensuring that agents satisfy safety specifications can be crucial in safety-critical environments. While methods exist for controller synthesis with safe temporal specifications, most existing methods restrict safe tempo…