Probabilistic Omega-regular Verification via Lexicographic Parity Supermartingales

This dissertation investigates algorithmic procedures for probabilistic model checking of stochastic models with general, possibly infinite, state space. Building on a novel proof certificate for Markov Decision Processes that ensures almost sure satisfaction of parity objectives, we develop two algorithms for demonic omega-regular verification of stochastic reactive systems via the synthesis of Lexicographic Parity Supermartingales. Prior work on proof certificates, particularly supermartingale certificates in stochastic settings, has been limited to simpler property classes such as safety and reachability. In contrast the methodologies presented here apply to the broader class of omega-regular properties, encompassing the entire LTL property class. The proposed algorithmic procedures leverage reduction techniques and synthesis methods previously explored in related works, employing SMT solvers to efficiently solve the underlying constraint satisfaction problems. Specifically, when the systems dynamics and the certificates templates are restricted to affine functions, we show that the synthesis can be reduced to a sequence of linear programming problems, which can be solved in polynomial time. For more general cases, the problem reduces to quantifier elimination over the reals, and a counter-example guided synthesis (CEGIS) procedure is proposed. Experimental evaluations and comparisons with state-of-the-art probabilistic model checkers demonstrate the effectiveness and practical relevance of our algorithms for the verification of large state space systems and countably infinite state space systems.