|
Organizers |
A Logic of Probability with Decidable Model-checking
by
Anatol Slissenko
University Paris-12, France
Coauthors: Daniele Beauquier (University Paris-12, France), Alexander Rabinovich (Tel-Aviv University, Israel)
A predicate logic of probability, close to logics of probability of Halpern and 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 expressive power of nesting of probabilities and the decidability of satisfability. Some open problems will be discussed.
Date received: June 2, 2002
Copyright © 2002 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cail-25.