Reasoning About States of Probabilistic Sequential Programs

A complete and decidable propositional logic for reasoning about states of probabilistic sequential programs is presented. The state logic is then used to obtain a sound Hoare-style calculus for basic probabilistic sequential programs. The Hoare calculus presented herein is the first probabilistic Hoare calculus with a complete and decidable state logic that has truth-functional propositional (not arithmetical) connectives. The models of the state logic are obtained exogenously by attaching sub-probability measures to valuations over memory cells. In order to achieve complete and recursive axiomatization of the state logic, the probabilities are taken in arbitrary real closed fields.

• Type: Conference
• Year: 2006
• Where: CSL
• Authors: Rohit Chadha, Paulo Mateus, Amílcar Sernadas
• Keywords: Automated Reasoning, CSL 2006, Decidable Propositional Logic, Probabilistic Sequential Programs, State Logic