4 citations · 17 across the 19 of their papers we have counts for
20 papers
Runtime Monitoring of Supermartingale Certificates
Mirco Giacobbe, Thomas A. Henzinger, Konstantin Kueffner +2
Supermartingale certificates formally guarantee temporal properties of discrete and continuous-time stochastic dynamical systems. However, these guarantees rely on a mathematical m…
Comparative Analysis of Barrier-like Function Methods for Reach-Avoid Verification in Stochastic Discrete-Time Systems
Zhipeng Cao, Peixin Wang, Luke Ong +3
In this paper, we compare several representative barrier-like conditions from the literature for infinite-horizon reach-avoid verification of stochastic discrete-time systems. Our…
Automating the Refinement of Reinforcement Learning Specifications
Tanmay Ambadkar, Đorđe Žikelić, Abhinav Verma
Logical specifications have been shown to help reinforcement learning algorithms in achieving complex tasks. However, when a task is under-specified, agents might fail to learn use…
Supermartingale Certificates for Quantitative Omega-regular Verification and Control
Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi +1
We present the first supermartingale certificate for quantitative -regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the produ…
Refuting Equivalence in Probabilistic Programs with Conditioning
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný +1
We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We st…
Predictive Monitoring of Black-Box Dynamical Systems
Thomas A. Henzinger, Fabian Kresse, Kaushik Mallik +2
We study the problem of predictive runtime monitoring of black-box dynamical systems with quantitative safety properties. The black-box setting stipulates that the exact semantics…
Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi +3
The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of…
Neural Control and Certificate Repair via Runtime Monitoring
Emily Yu, Đorđe Žikelić, Thomas A. Henzinger
Learning-based methods provide a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. To ensure the satisfaction…
Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties
S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer +1
Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defi…
Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady +2
We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witne…
Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees
Đorđe Žikelić, Mathias Lechner, Abhinav Verma +2
Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of s…
Solving Long-run Average Reward Robust MDPs via Stochastic Games
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi +2
Markov decision processes (MDPs) provide a standard framework for sequential decision making under uncertainty. However, MDPs do not take uncertainty in transition probabilities in…
Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks
Mathias Lechner, Đorđe Žikelić, Krishnendu Chatterjee +2
We study the problem of training and certifying adversarially robust quantized neural networks (QNNs). Quantization is a technique for making neural networks more efficient by runn…
Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees
Đorđe Žikelić, Mathias Lechner, Thomas A. Henzinger +1
We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for p…
Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems
Matin Ansaripour, Krishnendu Chatterjee, Thomas A. Henzinger +2
We consider the problem of learning control policies in discrete-time stochastic systems which guarantee that the system stabilizes within some specified stabilization region with…
Learning Stabilizing Policies in Stochastic Control Systems
Đorđe Žikelić, Mathias Lechner, Krishnendu Chatterjee +1
In this work, we address the problem of learning provably stable neural network policies for stochastic control systems. While recent work has demonstrated the feasibility of certi…
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
Đorđe Žikelić, Bor-Yuh Evan Chang, Pauline Bolignano +1
We present a novel approach to differential cost analysis that, given a program revision, attempts to statically bound the difference in resource usage, or cost, between the two pr…
Stability Verification in Stochastic Control Systems via Neural Network Supermartingales
Mathias Lechner, Đorđe Žikelić, Krishnendu Chatterjee +1
We consider the problem of formally verifying almost-sure (a.s.) asymptotic stability in discrete-time nonlinear stochastic control systems. While verifying stability in determinis…
Infinite Time Horizon Safety of Bayesian Neural Networks
Mathias Lechner, Đorđe Žikelić, Krishnendu Chatterjee +1
Bayesian neural networks (BNNs) place distributions over the weights of a neural network to model uncertainty in the data and the network's prediction. We consider the problem of v…
Scalable Verification of Quantized Neural Networks (Technical Report)
Thomas A. Henzinger, Mathias Lechner, Đorđe Žikelić
Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle.…