A probabilistic PDL

1 January 1983

proceedings article
Published by Association for Computing Machinery (ACM)

p. 291-297
https://doi.org/10.1145/800061.808758

Abstract

In this paper we give a probabilistic analog PPDL of Propositional Dynamic Logic. We prove a small model property and give a polynomial space decision procedure for formulas involving well-structured programs. We also give a deductive calculus and illustrate its use by calculating the expected running time of a simple random walk program.

Keywords

SMALL MODEL PROPERTY
WELL-STRUCTURED PROGRAM
SIMPLE RANDOM WALK PROGRAM
PROBABILISTIC ANALOG PPDL
PROBABILISTIC PDL
DEDUCTIVE CALCULUS
POLYNOMIAL SPACE DECISION PROCEDURE
PROPOSITIONAL DYNAMIC LOGIC

This publication has 0 references indexed in Scilit: