Advertisement

Local model checking for real-time systems

Extended abstract
  • Oleg V. Sokolsky
  • Scott A. Smolka
Session 7: Invited Titorial
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

We present a local algorithm for model checking in a real-time extension of the modal mu-calculus. As such, the whole state space of the real-time system under investigation need not be explored, but rather only that portion necessary to determine the truthhood of the logical formula. To the best of our knowledge, this is the first local algorithm for the verification of real-time systems to appear in the literature.

Like most algorithms dealing with real-time systems, we work with a finite quotient of the inherently infinite state space. For maximal efficiency, we obtain, on-the-fly, a quotient that is as coarse at possible in the following sense: refinements of the quotient are carried out only when necessary to satisfy clock constraints appearing in the logical formula or timed automaton used to represent the system under investigation. In this sense, our data structures are optimal with respect to the given formula and automaton.

Keywords

Model Check Product Graph Logical Formula Atomic Proposition Model Check Problem 
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. [ACD+92]
    R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. “An Implementation of Three Algorithms for Timing Verification Based on Automata Emptiness”. In Proceedings of IEEE Real-Time Symposium. IEEE Computer Society Press, 1992.Google Scholar
  2. [ACD93]
    R. Alur, C. Courcoubetis, and D. Dill. “Model-Checking for Real-Time Systems”. Information and Computation, 104(1):2–34, 1993.CrossRefGoogle Scholar
  3. [ACH+92]
    R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. “Minimization of Timed Transition Systems”. In Proceedings of CONCUR'92. LNCS 630, 1992.Google Scholar
  4. [AD94]
    R. Alur and D. L. Dill. “The Theory of Timed Automata”. Theoretical Comput. Sci., 126(2), 1994.Google Scholar
  5. [Alu91]
    R. Alur. Techniques for Authomatic Verification of Real-Time Systems. PhD thesis, Stanford University, 1991.Google Scholar
  6. [And94]
    H. R. Andersen. “Model Checking and Boolean Graphs”. Theoretical Comput. Sci., 126(1), 1994.Google Scholar
  7. [BFH+92]
    A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. “Minimal State Graph Generation”. Sci. Comput. Programming, 18(3):247–269, 1992.Google Scholar
  8. [BVW94]
    O. Bernholz, M. Y. Vardi, and P. Wolper. “An Automata-Thoeretic Approach to Branching-Time Model Checking”. In Proceedings of CAV'94. LNCS 818, 1994.Google Scholar
  9. [CC79]
    P. Cousot and R. Cousot. “Constructive Versions of Tarski's Fixed Point Theorems”. Pacific J. Math., 82(1):43–57, 1979.Google Scholar
  10. [CE81]
    E. M. Clarke and E. A. Emerson. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. LNCS 131, 1981.Google Scholar
  11. [CES86]
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. “Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications”. ACM Trans. Prog. Lang. Syst., 8(2), 1986.Google Scholar
  12. [CGL+94]
    R. Cleaveland, J. N. Gada, P. M. Lewis, S. A. Smolka, O. V. Sokolsky, and S. Zhang. “The Concurrency Factory — Practical Tools for Specification, Simulation, Verification and Implementation of Concurrent Systems”. In Proceedings of the DIMACS Workshop on Specification Techniques for Concurrent Systems, Princeton, NJ, 1994.Google Scholar
  13. [Cle90]
    R. Cleaveland. “Tableau-Based Model Checking in the Propositional Mu-Calculus”. Acta Inf., 27, 1990.Google Scholar
  14. [CPS93]
    R. Cleaveland, J. Parrow, and B. Steffen. “The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems”. ACM TOPLAS, 15(1), 1993.Google Scholar
  15. [CS93]
    R. Cleaveland and B. Steffen. “A Linear-Time Model Checking Algorithm for the Alternation-Free Modal Mu-Calculus”. Formal Methods in System Design, 2, 1993.Google Scholar
  16. [Dil89]
    D. Dill. “Timing Assumptions and Verification of Finite-State Concurrent Systems”. In Proceedings of CAV'89. LNCS 407, 1989.Google Scholar
  17. [EJS93]
    E. A. Emerson, C. S. Jutla, and A. P. Sistla. “On Model Checking for Fragments of μ-calculus”. In Proceedings of CAV'93. LNCS 697, 1993.Google Scholar
  18. [EL86]
    E. A. Emerson and C.-L. Lei. “Efficient Model Checking in Fragments of the Propositional Mu-Calculus”. In Proceedings LICS '86. IEEE Computer Society Press, 1986.Google Scholar
  19. [Eme91]
    E. A. Emerson. “Real-Time and the Mu-Calculus”. In Real-Time: Theory in Practice. LNCS 600, 1991.Google Scholar
  20. [HLW91]
    U. Holmer, K. G. Larsen, and Y. Wang. “Deciding Properties of Regular Real Timed Processes”. In Proceedings of CAV'91. LNCS 575, 1991.Google Scholar
  21. [HNSY94]
    T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. “Symbolic Model Checking for Real-time Systems”. Information and Computation, 111(2), 1994.Google Scholar
  22. [Koz83]
    D. Kozen. “Results on the Propositional Mu-Calculus”. Theoretical Comput. Sci., 27:333–354, 1983.Google Scholar
  23. [Lar92]
    K. G. Larsen. “Efficient Local Correctness Checking”. In Proceedings of CAV'92. LNCS 663, 1992.Google Scholar
  24. [SS94]
    O. Sokolsky and S. A. Smolka. “Incremental Model Checking in the Modal Mu-Calculus”. In Proceedings of CAV'94. LNCS 818, 1994.Google Scholar
  25. [SW91]
    C. Stirling and D. Walker. “Local Model Checking in the Modal Mu-Calculus”. Theoretical Comput. Sci., 89(1), 1991.Google Scholar
  26. [VLAP94]
    B. Vergauwen, J. Lewi, I. Avau, and A. Pote. “Efficient Computation of Nested Fix-Points, with applications to Model Checking”. In Proceedings of ICTL'94, 1st Intl. Conference on Temporal Logic. LNCS 827, 1994.Google Scholar
  27. [VW86]
    M. Y. Vardi and P. Wolper. “An Automata-Theoretic Approach to Automatic Program Verification”. In Proceedings of LICS'86, pages 322–331. IEEE Computer Society Press, 1986.Google Scholar
  28. [Wan91]
    Y. Wang. A Calculus of Real Time Systems. PhD thesis, Chalmers University of Technology, 1991.Google Scholar
  29. [YL93]
    M. Yannakakis and D. Lee. “An Efficient Algorithm for Minimizing Real-Time Transition Systems”. In Proceedings of CAV'93. LNCS 697, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Oleg V. Sokolsky
    • 1
  • Scott A. Smolka
    • 1
  1. 1.Department of Computer ScienceSUNY at Stony BrookStony Brook

Personalised recommendations