A Decidable Probability Logic for Timed Probabilistic Systems

• Autorzy: Lanotte R. , Beauquier D.
• Języki publikacji: EN

Abstrakty

EN

In this paper we extend the predicate logic introduced by Beauquier et al. in order to deal with Markov decision processes. We prove that with respect to qualitative probabilistic properties, model checking is decidable for this logic applied to Markov decision processes. Furthermore we apply our logic to probabilistic timed transition systems using predicates on clocks. We prove that results on Markov decision processes hold also for probabilistic timed transition systems. The interest of this logic lies in particular on the fact that some important properties are expressible in this logic but not expressible in pCTL.

Słowa kluczowe

EN

Markov decision processes; Probabilistic Timed Transition Systems; model checking; predicate logic of probabilities

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 96, nr 1/2
• Strony: 127--151
• Opis fizyczny: Bibliogr. 22 poz., tab., wykr.

Twórcy

autor

Lanotte R.

autor

Beauquier D.

• Dipartimento di Scienze della Cultura, Politiche e dell'Informazione, Universita dell'Insubria, Italy,

Bibliografia

• [1] Alur, R., Courcoubetis, C., D.Dill: Model-Checking for probabilistic real-time, International Colloquium on Automata, Languages, and Programming, number 510 in Lecture Notes in Computer Science, Springer, Berlin, 1991.
• [2] Alur, R., Courcoubetis, C., Dill, D. L.: Verifying Automata Specifications of Probabilistic Real-time Systems, Proceedings of the Real-Time: Theory in Practice, REX Workshop, Springer-Verlag, 1992.
• [3] Alur, R., Dill, D. L.: A Theory of Timed Automata, Theoretical Computer Science, 126, 1994, 183-235.
• [4] Alur, R., Henzinger, T. A.: Real-Time Logics: Complexity and Expressiveness, Information and Computation, 1993, 35-77.
• [5] Aziz, A., Singhal, V., Balarin, F., Brayton, R. K., Sangiovanni-Vincentelli,A. L.: It is usually works: the temporal logics of stochastic systems, Computer Aided Verification, number 939 in Lecture Notes in Computer Science, Springer, Berlin, 1995.
• [6] Baier, C., Kwiatkowska,M. Z.: On the Verification of Qualitative Properties of Probabilistic Processes under Fairness Constraints., Inf. Process. Lett., 66, 1998, 71-79.
• [7] Beauquier, D.: Markov decision processes and deterministic Buchi automata, Fundamenta Informaticae, 50, 2002, 1-13.
• [8] Beauquier, D.: On probabilistic timed automata, Theoretical Computer Science, 292, 2003, 65-84.
• [9] Beauquier, D., Rabinovich, A., Slissenko, A.: A logic of probability with decidable model-checking, Proceedings of the International Congress on Computer Science Logic, number 2471 in Lecture Notes in Computer Science, Springer, Berlin, 2002.
• [10] Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable Timed Automata, Theoretical Computer Science, 321, 2004, 291-345.
• [11] Buchi, J. R.: On a decision method in restricted second order arithmetic, Proceedings of the International Congress on Logic, Method, and Philosophy of Science, Stanford Univ. Press, 1962.
• [12] Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification, Journal of the ACM, 42, 1995, 340-367.
• [13] Daws, C., Kwiatkowska,M., Norman, G.: AutomaticVerification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM, International Journal on Software Tools for Technology Transfer (STTT), 5, 2004, 221-236.
• [14] Hansson, H. A., Jonsson, B.: A logic of reasoning about time and probability, Formal Aspects of Computing, 6, 1994, 512-535.
• [15] Kemeny, J. G., Snell, J. L.: Finite Markov Chains, Van Nostrand, 1960.
• [16] Kwiatkowska, M., Norman, G., Segala, R., Sproton, J.: Automatic verification of real-time systems with discrete probability distribuitions, Theoretical Computer Science, 282, 2002, 101-150.
• [17] Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic Model Checking of Deadline Properties in the IEEE 1394 Fire Wire Root Contention Protocol, Formal Aspects of Computing, 14, 2003, 295-318.
• [18] Kwiatkowska, M., Norman, G., Sproston, J.: Symbolic Model Checking for Probabilistic Timed Automata, Proc. of FORMATS-FTRTFT2004, number 3253 in Lecture Notes in Computer Science, Springer, Berlin, 2004.
• [19] Lehmann, D., Shelah, S.: Reasoning about time and change, Information and Control, 53, 1982, 165-198.
• [20] Schneider, F. B.: Implementing fault-tolerant services using the state machine approach: a tutorial, ACM Computing Surveys, 22, 1990, 299-319.
• [21] Thomas, W.: Automata on Infinite Objects, Handbook of Theoretical Computer Science, Volume B, 1990, 133-192.
• [22] Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs, In Proceedings of 26th Annual Symposium on Foundations of Computer Science, IEEE Computer Society Press, 1985.