6 papers
Almost Sure Reachability in Continuous-time Stochastic Systems
Arash Bahari Kordabad, Rupak Majumdar, Sadegh Soudjani
We provide certificates for almost sure reachability of continuous-time stochastic systems governed by stochastic differential equations (SDEs). We first show that a standard Euler…
Sum-of-Squares Certificates for Almost-Sure Reachability of Stochastic Polynomial Systems
Arash Bahari Kordabad, Rupak Majumdar, Sadegh Soudjani
In this paper, we present a computational approach to certify almost sure reachability for discrete-time polynomial stochastic systems by turning drift--variant criteria into sum-o…
Formal Analysis of Metastable Failures in Software Systems
Peter Alvaro, Rebecca Isaacs, Rupak Majumdar +3
Many large-scale software systems demonstrate metastable failures. In this class of failures, a stressor such as a temporary spike in workload causes the system performance to drop…
MightyPPL: Verification of MITL with Past and Pnueli Modalities
Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani +2
Metric Interval Temporal Logic (MITL) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using MITL in verificatio…
On Certificates for Almost Sure Reachability in Stochastic Systems
Arash Bahari Kordabad, Rupak Majumdar, Harshit Jitendra Motwani +1
Almost sure reachability refers to the property of a stochastic system whereby, from any initial condition, the system state reaches a given target set with probability one. In thi…
Sound and Complete Proof Rules for Probabilistic Termination
Rupak Majumdar, V. R. Sathiyanarayana
Deciding termination is a fundamental problem in the analysis of probabilistic imperative programs. We consider the qualitative and quantitative probabilistic termination problems…