Learning Probabilistic Temporal Safety Properties from Examples in Relational Domains
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 relational Markov Decision Processes with pCTL model-checking. More specifically, we assume that there is an unknown relational pCTL target formula that is satisfied by only safe states, and has a horizon of maximum $k$ steps and a threshold probability $\alpha$. The task then consists of learning this unknown formula from states that are labeled as safe or unsafe by a domain expert. We apply principles of relational learning to induce a pCTL formula that is satisfied by all safe states and none of the unsafe ones. This formula can then be used as a safety specification for this domain, so that the system can avoid getting into dangerous situations in future. Following relational learning principles, we introduce a candidate formula generation process, as well as a method for deciding which candidate formula is a satisfactory specification for the given labeled states. The cases where the expert knows and does not know the system policy are treated, however, much of the learning process is the same for both cases. We evaluate our approach on a synthetic relational domain.
Code (0)
등록된 구현이 없습니다.
Tasks
Relational ReasoningMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Synthesis of Safety Specifications for Probabilistic Systems
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…
Discrete-Time Nonlinear Systems Identification with Probabilistic Safety and Stability Constraints
This paper presents a discrete-time nonlinear system identification method while satisfying the stability and safety properties of the system with high probability. An Extreme Learning Machine (ELM) is used with a Gaussi…
Probabilistic Safety Verification for an Autonomous Ground Vehicle: A Situation Coverage Grid Approach
As industrial autonomous ground vehicles are increasingly deployed in safety-critical environments, ensuring their safe operation under diverse conditions is paramount. This paper presents a novel approach for their safe…
Lifted Model Checking for Relational MDPs
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…
modelModel-based Reinforcement Learningreinforcement-learningReinforcement Learning (RL)Safe Control under Uncertainty
Controller synthesis for hybrid systems that satisfy temporal specifications expressing various system properties is a challenging problem that has drawn the attention of many researchers. However, making the assumption …
Autonomous Vehicles