Learning Probabilistic Temporal Safety Properties from Examples in Relational Domains

TL;DR

This paper introduces a method for learning probabilistic temporal safety properties expressed in relational pCTL from labeled states, enabling systems to autonomously identify safe behaviors in relational domains.

Contribution

It presents a novel relational learning framework for inferring probabilistic temporal safety properties from labeled data, combining relational MDPs with pCTL model-checking.

Findings

Successfully learned safety properties in synthetic relational domains.

Able to distinguish safe and unsafe states with high accuracy.

Framework applicable to domains with unknown policies.

Abstract

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.