Barrier Certificates for Uncertain Temporal Specifications
For researchers in formal verification and control, this provides a tractable optimization-based approach to verify temporal properties under predicate uncertainty, though it is incremental as it extends existing barrier certificate methods to a new problem setting.
This paper develops a certificate-based framework using barrier certificates to bound the probability that stochastic dynamical systems satisfy temporal logic specifications with randomly evolving predicates, avoiding dynamic programming. The method is demonstrated on numerical case studies with linear dynamics and safety specifications.
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.