Information-Guided Temporal Logic Inference with Prior Knowledge

TL;DR

This paper develops methods to infer interpretable parametric linear temporal logic formulas from data, incorporating prior knowledge to enhance informativeness and applicability to system analysis.

Contribution

It introduces algorithms for computing information gain with respect to prior distributions and provides a polynomial-time inference method for certain pLTL formulas.

Findings

Effective explanation of anomalous patterns

Detection of pattern changes in data

Analysis of Markov decision process policies

Abstract

This paper investigates the problem of inferring knowledge from data so that the inferred knowledge is interpretable and informative to humans who have prior knowledge. Given a dataset as a collection of system trajectories, we infer parametric linear temporal logic (pLTL) formulas that are informative and satisfied by the trajectories in the dataset with high probability. The informativeness of the inferred formula is measured by the information gain with respect to given prior knowledge represented by a prior probability distribution. We first present two algorithms to compute the information gain with a focus on two types of prior probability distributions: stationary probability distributions and probability distributions expressed by discrete time Markov chains. Then we provide a method to solve the inference problem for a subset of pLTL formulas with polynomial time complexity with respect to the number of Boolean connectives in the formula. We provide implementations of the proposed approach on explaining anomalous patterns, patterns changes and explaining the policies of Markov decision processes.