Technical Report: Distribution Temporal Logic: Combining Correctness with Quality of Estimation

TL;DR

This paper introduces Distribution Temporal Logic (DTL), a new logic for expressing properties involving uncertainty in partially observable systems, with algorithms for monitoring such properties in Markov decision processes.

Contribution

The paper proposes DTL, a novel temporal logic that captures uncertainty and likelihood, along with monitoring algorithms for partially observable systems.

Findings

DTL can express properties involving uncertainty and likelihood.

Algorithms for monitoring DTL in POMDPs are developed.

A rescue robotics case study demonstrates the approach.

Abstract

We present a new temporal logic called Distribution Temporal Logic (DTL) defined over predicates of belief states and hidden states of partially observable systems. DTL can express properties involving uncertainty and likelihood that cannot be described by existing logics. A co-safe formulation of DTL is defined and algorithmic procedures are given for monitoring executions of a partially observable Markov decision process with respect to such formulae. A simulation case study of a rescue robotics application outlines our approach.