Abstract
We introduce a propositional logic whose formulas are built using the language of CTL *, enriched by two types of probability operators: one speaking about probabilities on branches, and one speaking about probabilities of sets of branches with the same initial state. An infinitary axiomatization for the logic, which is shown to be sound and strongly complete with respect to the corresponding class of models, is proposed.
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
Abadi, M.: The power of temporal proofs. Theoretical Computer Science 65, 35–83 (1989)
Aziz, A., Singhal, V., Balarin, F., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, Springer, Heidelberg (1995)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–512. Springer, Heidelberg (1995)
Burgess, J.: Axioms for tense logic. I. “Since” and “until”. Notre Dame Journal of Formal Logic 23(4), 367–374 (1982)
Burgess, J.: Logic and time. The Journal of Symbolic Logic 44(4), 566–582 (1979)
Burgess, J.: Basic tense logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. II, pp. 89–133. D. Reidel Publishing Compaany, Dordrecht (1984); Kopetz, H., Kakuda, Y. (eds.) Dependable Computing and Fault-Tolerant Systems. Responsive Computer Systems, Vol. 7 pp. 30–52. Springer, Heidelberg (1993)
Doder, D., Ognjanović, Z., Marković, Z.: An Axiomatization of a First-order Branching Time Temporal Logic. Journal of Universal Computer Science 16(11), 1439–1451 (2010)
Doder, D., Marković, Z., Ognjanović, Z., Perović, A., Rašković, M.: A Probabilistic Temporal Logic That Can Model Reasoning about Evidence. In: Link, S., Prade, H. (eds.) FoIKS 2010. LNCS, vol. 5956, pp. 9–24. Springer, Heidelberg (2010)
Doder, D., Marinković, B., Maksimović, P., Perović, A.: A Logic with Conditional Probability Operators. Publications de l’Institut Mathématique, Nouvelle Série, Beograd 87(101), 85–96 (2010)
Emerson, E., Clarke, E.: Using branching time logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 241–266 (1982)
Emerson, E.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pp. 995–1072. North-Holland Pub. Co./MIT Press (1990)
Fagin, R., Halpern, J., Megiddo, N.: A logic for reasoning about probabilities. Information and Computation 87(1–2), 78–128 (1990)
Feldman, Y.: A decidable propositional dynamic logic with explicit probabilities. Information and Control 63, 11–38 (1984)
Guelev, D.P.: A propositional dynamic logic with qualitative probabilities. Journal of Philosophical Logic 28(6), 575–605 (1999)
Guelev, D.P.: Probabilistic neighbourhood logic. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 264–275. Springer, Heidelberg (2000)
Guelev, D.P.: Probabilistic Interval Temporal Logic and Duration Calculus with Infinite Intervals: Complete Proof Systems. Logical Methods in Computer Science 3(3), 1–43 (2007)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspect of Computing 6(5), 512–535 (1994)
Hart, S., Sharir, M.: Probabilistic temporal logics for finite and bounded models. In: 16th ACM Symposium on Theory of Computing, pp. 1–13. ACM, New York (1984): Extended version In: Information and Control 70 (2/3), 97-155 (1986)
Hung, D.V., Chaochen, Z.: Probabilistic Duration Calculus for Continuous Time. Formal Aspects of Computing 11(1), 21–44 (1999)
Kozen, D.: A probabilistic PDL. Journal of Computer and System Sciences 30, 162–178 (1985)
Lehmann, D., Shelah, S.: Reasoning with time and chance. Information and Control 53, 165–198 (1982)
Liu, Z., Ravn, A.P., Sorensen, E.V., Chaochen, Z.: A Probabilistic Duration Calculus. In: Kopetz, H., Kakuda, Y. (eds.) Dependable Computing and Fault-Tolerant Systems. Responsive Computer Systems, vol. 7, pp. 30–52. Springer, Heidelberg (1993)
Marković, Z., Ognjanović, Z., Rašković, M.: A Probabilistic Extension of Intuitionistic Logic. Mathematical Logic Quarterly 49, 415–424 (2003)
Ognjanović, Z., Rašković, M.: Some probability logics with new types of probability operators. Journal of Logic and Computation 9(2), 181–195 (1999)
Ognjanović, Z., Rašković, M.: Some first-order probability logics. Theoretical Computer Science 247(1-2), 191–212 (2000)
Ognjanović, Z.: Discrete Linear-time Probabilistic Logics: Completeness, Decidability and Complexity. Journal of Logic Computation 16(2), 257–285 (2006)
Ognjanović, Z., Perović, A., Rašković, M.: Logics with the Qualitative Probability Operator. Logic Journal of IGPL 16(2), 105–120 (2008)
Perović, A., Ognjanović, Z., Rašković, M., Marković, Z.: A Probabilistic Logic with Polynomial Weight Formulas. In: Hartmann, S., Kern-Isberner, G. (eds.) FoIKS 2008. LNCS, vol. 4932, pp. 239–252. Springer, Heidelberg (2008)
Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of the 18th IEEE Symposium Foundations of Computer Science (FOCS 1977), pp. 46–57 (1977)
Prior, A.: Time and Modality. Oxford University Press, Oxford (1957)
Rašković, M., Marković, Z., Ognjanović, Z.: A Logic with Approximate Conditional Probabilities that can Model Default Reasoning. International Journal of Approximate Reasoning 49(1), 52–66 (2008)
Reynolds, M.: An axiomatization of full computation tree logic. The Journal of Symbolic Logic 66(3), 1011–1057 (2001)
Segerberg, K.: Qualitative probability in a modal setting. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium. North-Holland, Amsterdam (1971)
Stirling, C.: Modal and temporal logic. Handbook of Logic in Computer Science 2, 477–563 (1992)
Tzanis, E., Hirsch, R.: Probabilistic Logic over Paths. Electronic Notes in Theoretical Computer Science 220(3), 79–96 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ognjanović, Z., Doder, D., Marković, Z. (2011). A Branching Time Logic with Two Types of Probability Operators. In: Benferhat, S., Grant, J. (eds) Scalable Uncertainty Management. SUM 2011. Lecture Notes in Computer Science(), vol 6929. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23963-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-23963-2_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23962-5
Online ISBN: 978-3-642-23963-2
eBook Packages: Computer ScienceComputer Science (R0)