Sciweavers

CSL
2006
Springer

Reasoning About States of Probabilistic Sequential Programs

13 years 7 months ago
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.
Rohit Chadha, Paulo Mateus, Amílcar Sernada
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where CSL
Authors Rohit Chadha, Paulo Mateus, Amílcar Sernadas
Comments (0)