Abstract
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 decidability of satisfiability and compare our logic of probability with the probabilistic temporal logic pCTL *.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi and J. Halpern. Decidability and expressiveness for first-order logic of probability. Information and Computation, 112(1):1–36, 1994.
A. Aziz, V. Singhal, F. Balarin, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. It usually works: the temporal logic of stochastic systems. In Computer Aided Verification. Proceeding of CAV’95, pages 155–165. Springer Verlag, 1995. Lect. Notes in Comput. Sci., vol. 939.
J. R. Büchi. Weak second-order arithmetic and finite automata. Z. Math. Logik u. Grundlag. Math., (6):66–92, 1960.
C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42:857–907, 1995.
R. Fagin and J. Halpern. Reasoning about knowledge and probability. J. of the Assoc. Comput. Mach., 41(2):340–367, 1994.
R. Fagin, J.Y. Halpern, and N. Megiddo. A logic for reasoning about probabilities. Information and Computation, 87:1,2:78–128, 1990.
F. R. (Feliks Ruvimovich) Gantmakher. The Theory of Matrices. Chelsea Pub. Co., New York, 1977.
D. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic. Clarendon Press, Oxford, 1994.
J. Halpern. An analysis of first-order logics of probability. Artificial Intelligence, 46:311–350, 1990.
H. A. Hansson. Time and Probability in Formal Design of Distributed Systems. Elsevier, 1994. Series: “Real Time Safety Critical System”, vol. 1.
H. A. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6(5):512–535, 1994.
W. A. Hodges. Model Theory. Cambridge University Press, Cambridge, 1993.
J. G. Kemeny and J. L. Snell. Finite Markov Chains. D Van Nostad Co., Inc., Princeton, N.J., 1960.
J. G. Kemeny, J. L. Snell, and A.W. Knapp. Denumerable Markov Chains. D Van Nostad Co., Inc., Princeton, N. J., 1966.
H. J. Keisler. Probability quantifiers. In J. Barwise and S. S.Feferman, editors, Model Theoretic Logics, pages 509–556. Springer, 1985.
D. Lehmann and S. Shelah. Reasoning about time and chance. Information and Control, 53(3):165–198, 1982.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 131–191. North-Holland, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beauquier, D., Rabinovich, A., Slissenko, A. (2002). A Logic of Probability with Decidable Model-Checking. In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_21
Download citation
DOI: https://doi.org/10.1007/3-540-45793-3_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44240-0
Online ISBN: 978-3-540-45793-0
eBook Packages: Springer Book Archive