Reasoning about probabilistic sequential programs
A complete and decidable Hoare-style calculus for iteration-free probabilistic sequential programs is presented using a state logic with truth-functional propositional (not arithmetical) connectives. (c) 2007 Elsevier B.V.. All rights reserved.
completeness decidability probabilistic reasoning hoare calculus