Advertisement

It usually works: The temporal logic of stochastic systems

  • Adnan Aziz
  • Vigyan Singhal
  • Felice Balarin
  • Robert K. Brayton
  • Alberto L. Sangiovanni-Vincentelli
Session 6: Invited Titorial
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

In this paper the branching time logic pCTL* is defined. pCTL* expresses quantitative bounds on the probabilities of correct behavior; it can be interpreted over discrete Markov processes. A bisimulation relation is defined on finite Markov processes, and shown to be sound and complete with respect to pCTL*. We extend the universe of models to generalized Markov processes in order to support notions of refinement, abstraction, and parametrization. Model checking pCTL* over generalized Markov processes is shown to be elementary by a reduction to RCF. We conclude by describing practical and theoretical avenues for further work.

Keywords

Markov Process Model Check Temporal Logic Stochastic System Atomic Proposition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    R. Alur, C. Courcoubetis, and D. Dill. Model Checking for Probabilistic Real Time Systems. In Proc. of the Colloquium on Automata, Languages, and Programming, pages 115–126, 1991.Google Scholar
  2. 2.
    A. Aziz, V. Singhal, F. Balarin, R. K. Brayton, and A. Sangiovanni-Vincentelli. It Usually Works: The Temporal Logic of Stochastic Systems. http://www-cad.eecs.berkeley.edu:80/ãdnan/cav95.1.Google Scholar
  3. 3.
    A. Aziz, V. Singhal, F. Balarin, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Equivalences for Fair Kripke Structures. In International Colloquium on Automata, Languages and Programming. Springer Verlag, July 1994.Google Scholar
  4. 4.
    R. I. Bahar, E. A. Frohm, C. M. Gaona, G. D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic Decision Diagrams and their Applications. In Proc. Intl. Conf. on Computer-Aided Design, pages 188–192, 1993.Google Scholar
  5. 5.
    M. Ben-Or, D. Kozen, and J. Reif. The Complexity of Elementary Algebra and Geometry. In Proc. ACM Symposium on the Theory of Computing, pages 457–464, 1984.Google Scholar
  6. 6.
    M. C. Browne, E. M. Clarke, and O. Grümberg. Characterizing Kripke Structures in Temporal Logic. Technical Report CMU-CS-87-104, Department of Computer Science, Carnegie Mellon University, 1987.Google Scholar
  7. 7.
    R. Cleavland, S. A. Smolka, and A. Zwarico. Testing Preorders for Probabilistic Processes. In Proc. of the Colloquium on Automata, Languages, and Programming, pages 708–719, 1992.Google Scholar
  8. 8.
    C. Courcoubetis and M. Yannakakis. Verifying Temporal Properties of Finite State Probabilistic Programs. In Proc. IEEE Symposium on the Foundations of Computer Science, pages 338–345, 1988.Google Scholar
  9. 9.
    C. Courcoubetis and M. Yannakakis. Automatic Verification of Finite State Programs. In Proc. of the Colloquium on Automata, Languages, and Programming, pages 326–347, 1990.Google Scholar
  10. 10.
    E. A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, pages 996–1072. Elsevier Science, 1990.Google Scholar
  11. 11.
    Ioannis Emiris. Sparse Elimination and Applications in Kinematics. PhD thesis, University of California at Berkeley, Berkeley, CA, December 1994.Google Scholar
  12. 12.
    H. Hansson and B. Jonsson. A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing, 6:512–535, 1994.CrossRefGoogle Scholar
  13. 13.
    S. Hart and M. Shamir. Probabilistic Temporal Logics for Finite and Bounded Models. In Proc. ACM Symposium on the Theory of Computing, pages 1–13, 1984.Google Scholar
  14. 14.
    S. Hart, M. Sharir, and A. Pneuli. Verification of Probabilistic Programs. SIAM Journal of Computation, 13:292–314, 1984.Google Scholar
  15. 15.
    A. Paz. Introduction to Probabilistic Automata. Academic-Press, 1971.Google Scholar
  16. 16.
    A. Pnueli and L. Zuck. Probabilistic verification. Information and Computation, 103(1):1–29, 1993.CrossRefGoogle Scholar
  17. 17.
    Ashutosh Rege. Efficient Decision Procedures for Fragments of R.C.F. (in preparation). PhD thesis, University of California at Berkeley, Berkeley, CA, June 1995.Google Scholar
  18. 18.
    D. Revuz. Markov Chains. North-Holland, 1975.Google Scholar
  19. 19.
    H. L. Royden. Real Analysis. Macmillan Publishing, 1889.Google Scholar
  20. 20.
    M. Y. Vardi and P. L. Wolper. An Automata-Theoretic Approach to Program Verification. In Proc. IEEE Symposium on Logic in Computer Science, pages 332–334, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Adnan Aziz
    • 1
  • Vigyan Singhal
    • 1
  • Felice Balarin
    • 1
  • Robert K. Brayton
    • 1
  • Alberto L. Sangiovanni-Vincentelli
    • 1
  1. 1.Department of Electrical Engineering and Computer SciencesUniversity of CaliforniaBerkeleyUSA

Personalised recommendations