7 papers
HyperCertificates: Verification of Discrete-time Dynamical Systems against HyperLTL Specifications
Vishnu Murali, Amin Falah, Ashutosh Trivedi +1
We introduce a functional inductive framework to verify discrete-time dynamical systems against hyperproperties specified as Hyperlinear temporal logic formulae via a notion of Hyp…
Vector Certificates for -regular Specifications
Mohammed Adib Oumer, Vishnu Murali, Majid Zamani
The recently introduced notions of ranking functions and closure certificates utilize well-foundedness arguments to facilitate the verification of dynamical systems against -re…
Interpolation-Inspired Closure Certificates
Mohammed Adib Oumer, Vishnu Murali, Majid Zamani
Barrier certificates, a form of state invariants, provide an automated approach to the verification of the safety of dynamical systems. Similarly to barrier certificates, recent wo…
-Inductive and Interpolation-Inspired Barrier Certificates for Stochastic Dynamical Systems
Mohammed Adib Oumer, Vishnu Murali, Majid Zamani
In this paper, we introduce two new types of barrier certificates that are based on multiple functions rather than a single one. A conventional barrier certificate for a stochastic…
Control Closure Certificates
Vishnu Murali, Mohammed Adib Oumer, Majid Zamani
This paper introduces the notion of control closure certificates to synthesize controllers for discrete-time control systems against -regular specifications. Typical functional…
Data-Driven Safety Verification using Barrier Certificates and Matrix Zonotopes
Mohammed Adib Oumer, Amr Alanwar, Majid Zamani
Ensuring safety in cyber-physical systems (CPSs) is a critical challenge, especially when system models are difficult to obtain or cannot be fully trusted due to uncertainty, model…