Technical Report: Distribution Temporal Logic: Combining Correctness with Quality of Estimation
This work addresses the problem of combining correctness with quality of estimation for researchers in formal methods and robotics, but it appears incremental as it builds on existing temporal logics.
The authors introduced Distribution Temporal Logic (DTL) to express properties involving uncertainty and likelihood in partially observable systems, which existing logics cannot describe, and provided algorithmic procedures for monitoring executions in a simulation case study of a rescue robotics application.
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.