## Paper: Probabilistic Verification by Tableaux (at LICS 1986)

**Amir Pnueli Lenore D. Zuck**

### Abstract

We present an algorithm for verifying that a temporal formula holds with probability 1 over all computations of a given probabilistic finite state program. It is based on simple tableaux methods. The algorithm has a single exponential time complexity and considers a restricted temporal logic which is expressively equivalent to the full temporal logic.

### BibTeX

@InProceedings{PnueliZuck-ProbabilisticVerifi, author = {Amir Pnueli and Lenore D. Zuck}, title = {Probabilistic Verification by Tableaux}, booktitle = {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)}, year = {1986}, month = {June}, pages = {322--331}, location = {Cambridge, MA, USA}, publisher = {IEEE Computer Society Press} }