Barrier Certificates for Weighted Automata-based Specifications
Vishnu Murali, Ashutosh Trivedi, Majid Zamani.
CDC 2024 : 5191-5196
Abstract
Barrier certificates, functional analogs of inductive invariants, play a fundamental role in the verification of safety for dynamical systems. The success of these certificates in safety verification has led to the investigation of their use to verify more general qualitative objectives such as those characterized by omega-regular automata. Here the certificates are used to establish a proof to ensure a set of accepting states are visited only finitely often. While omega-automata provide a reliable framework for specifying qualitative objectives such as safety, reachability, and patrolling, they are unable to capture notions of how “well” a system satisfies a desired property. Weighted-automata, weighted extensions to omega-automata, provide an expressive framework to describe quantitative objectives. We thus consider the problem of using barrier certificate-based approaches to verify dynamical systems against properties specified by weighted automata. Here one seeks to prove that all traces of a system have corresponding runs on the weighted automata with an aggregated cost that is greater than a fixed (a priori) threshold. We provide certificates to verify systems against weighted automata based on the choice of aggregation function. Our certificates rely on proving properties of safety, or (repeated) reachability in appropriate augmented systems. Finally, we demonstrate our approach on a case study.