Barrier Certificates for Uncertain Temporal Specifications

TL;DR

This paper introduces a barrier certificate framework for probabilistically verifying temporal logic specifications on stochastic systems with uncertain, evolving predicates, reducing computational complexity.

Contribution

It transforms stochastic predicate satisfaction problems into deterministic ones on an augmented space, enabling tractable probabilistic safety guarantees.

Findings

Derived analytical conditions for barrier certificates ensuring safety probabilities.

Developed a method to convert stochastic predicate satisfaction into deterministic verification.

Demonstrated effectiveness through numerical case studies.

Abstract

This paper studies satisfying temporal logic specifications on stochastic dynamical systems, where the predicates evolve randomly over time. Such randomness may arise from uncertain environment models or external stochastic processes causing the sets associated with predicate satisfaction to vary in a non-deterministic manner. As a result, verifying whether a stochastic dynamical system satisfies a temporal specification depends also on the uncertainty in the predicates. We develop a certificate-based framework to bound the probability of satisfying temporal logic specifications with randomly evolving predicates. We first show that temporal logic specifications with stochastic predicates can be transformed to specifications with deterministic predicates on an augmented space which is extended to include the stochastic space of predicate's uncertainty. We then utilize barrier certificates on an augmented space to provide tractable optimization-based conditions and to avoid the computational burden of dynamic programming. Focusing on linear dynamics and safety-type specifications, we derive analytical conditions under which barrier certificates guarantee bounds on the probability of violating the stochastic safety predicates. The approach is demonstrated on numerical case studies.