4 papers
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…