A Logic of Probability with Decidable Model Checking

A predicate logic of probability, close to the logics of probability of Halpern et al., is introduced. Our main result concerns the following model-checking problem: deciding whether a given formula holds on the structure defined by a given finite probabilistic process. We show that this model-check...

Full description

Saved in:
Bibliographic Details
Published in:Journal of logic and computation 2006-08, Vol.16 (4), p.461-487
Main Authors: Beauquier, Daniéle, Rabinovich, Alexander, Slissenko, Anatol
Format: Article
Language:English
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:A predicate logic of probability, close to the logics of probability of Halpern et al., is introduced. Our main result concerns the following model-checking problem: deciding whether a given formula holds on the structure defined by a given finite probabilistic process. We show that this model-checking problem is decidable for a rather large subclass of formulas of a second-order monadic logic of probability. We discuss also the decidability of satisfiability and compare our logic of probability with the probabilistic temporal logic pCTL *. * Partially supported by French-Israeli Arc-en-ciel/Keshet project No. 30 and No. 15.
ISSN:0955-792X
1465-363X
DOI:10.1093/logcom/exl004