Advertisement

Real-time and the Mu-Calculus (preliminary report)

  • E. Allen Emerson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 600)

Abstract

We argue that the Mu-Calculus provides a conceptually advantageous framework for specifying and reasoning about Real-Time Systems. We show that mechanical reasoning can be done efficiently in a quantitative formulation of the Mu-Calculus. Our work also suggests a new complexity theory for reactive systems.

Keywords

Model Check Temporal Logic Atomic Proposition Concurrent Program Computation Tree Logic 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Ab80]
    Abrahamson, K. Decidability and Expressiveness of Logics of Processes, Ph.D. Thesis, Univ. of Washington, 1980.Google Scholar
  2. [A191]
    Alur, R., Techniques for Automatic Verification of Real-Time Systems, PhD Thesis, Computer Science Department, Stanford University, August 1991, Technical Report STAN-CS-91-1378.Google Scholar
  3. [ACD90]
    Alur, R., Courcoubetis, C, and Dill, D., Model-checking for Real-Time Systems, Proc. of the Fifth IEEE Symp. on Logic in Computer Science (LICS), pp. 414–425, 1990.Google Scholar
  4. [AC88]
    Arnold, A., and Crubille, P., A Linear Time Algorithm to Solve Fixed Point Equations of Transitions Systems, Information Processing Letters, vol. 29, pp. 57–66, Sept., 1988.CrossRefGoogle Scholar
  5. [Br86]
    Browne, M.C., An Improved Algorithm for the Automatic Verification of Finite State Systems Using Temporal Logic, Proc. Symp. on Logic in Computer Science, Cambridge, pp. 260–266, 1986.Google Scholar
  6. [Bu84]
    Burgess, J., Basic Tense Logic, in Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, eds., D. Reidel Pub. Co, 1984.Google Scholar
  7. [CKS81]
    Chandra, A., Kozen, D., and Stockmeyer, L., Alternation, JACM, vol. 28, no. 1, pp. 114–133, 1981.CrossRefGoogle Scholar
  8. [CE81]
    Clarke, E.M., E.A. Emerson, Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic, Proc. of the Workshop on Logics of Programs, Yorktown Heights, D. Kozen, editor, LNCS#131, Springer-Verlag, pp. 52–71, 1981.Google Scholar
  9. [CES83]
    Clarke, E.M., E.A. Emerson, A.P. Sistla, Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach, Proc. 10th Annual ACM Symp. on Principles of Programming Languages, Austin, pp. 117–126, 1983; also appeared in ACM Transactions on Programming Languages and Systems, vol. 8, no. 2, pp. 244–263, 1986.Google Scholar
  10. [CG87]
    Clarke, E., and Grumber, O., Research on Automatic Verification of Finite State Concurrent Systems, Ann. Rev. Comp. Sci., vol. 2, pp. 269–290, 1987.CrossRefGoogle Scholar
  11. [CBBG87]
    E. Clarke, S. Bose, M. Browne, O. Grumberg, The Design and Verification of Finite State Hardware Controllers, Technical Report CMU-CS-87-145, Carnegie-Mellon Univ., July 1987.Google Scholar
  12. [CS91]
    Cleaveland, R., and Steffen, B., A Linear Time Model Checking Algorithm for the Alternation Free Modal Mu-Calculus, Proc. of the Third Workshop on Computer Aided Verification (Participant's Version), ed. K. Larsen and A. Skou, Math. and CS Dept, Univ. of Aalbourg, Denmark, July 1–4, 1991.Google Scholar
  13. [deB80]
    de Bakker, J. W., Mathematical Theory of Program Correctness, Prentice-Hall, Englewood Cliffs, NJ, 1980.Google Scholar
  14. [deR76]
    de Roever, W.P., Recursive Program Schemes: Semantics and Proof Theory, Mathematical Centre Tracts 70, Mathematisch Centrum, Amsterdam, 1976.Google Scholar
  15. [deR91]
    de Roever, W.-P., editor, Real-Time: Theory in Practice, Springer LNCS, to appear.Google Scholar
  16. [Di76]
    Dijkstra, E.W., A Discipline of Programming, Prentice-Hall, 1976.Google Scholar
  17. [Em90]
    Emerson, E.A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, vol. B., J. van Leeuwen, editor, North-Holland, pp. 995–1072Google Scholar
  18. [EC80]
    Emerson, E.A., E.M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Proc. 7th Annual International Colloquium on Automata, Languages and Programming, LNCS#85, Springer-Verlag, pp. 169–181, 1980.Google Scholar
  19. [EC82]
    Emerson, E.A., E.M. Clarke, Using Branching Time Logic to Synthesize Synchronization Skeletons, Science of Computer Programming, vol. 2, pp. 241–266, 1982.CrossRefGoogle Scholar
  20. [EH82]
    Emerson, E.A., J.Y. Halpern, Decision Procedures and Expressiveness in the Temporal Logic of Branching Time, Proc. of the 14th Annual ACM Symp. on Theory of Computing, San Francisco, pp. 169–180, 1982; also appeared in Journal of Computer and System Sciences, vol 30, no. 1, pp. 1–24, 1985.Google Scholar
  21. [EL85]
    Emerson, E.A., C.L. Lei, Modalities for Model Checking: Branching Time Logic Strikes Back, Proc. 12th Annual ACM Symp. on Principles of Programming Languages, New Orleans, pp. 84–96, 1985; also appeared in Science of Computer Programming, vol. 8, pp. 275–306, 1987.Google Scholar
  22. [EL86]
    Emerson, E. A., and Lei, C.-L., Efficient Model Checking in Fragments of the Mu-Calculus, IEEE Symp. on Logic in Computer Science, 1986.Google Scholar
  23. [EL87]
    Emerson, E.A., C.L. Lei, New Results on Model-Checking in the Prepositional Mu-Calculus, presented at the Colloquium on Temporal Logic and Specification, Altrincham, England, 1987.Google Scholar
  24. [EMSS89]
    Emerson, E. A., Mok, A. K., Sistla, A. P., and Srinivasan, J., Quantitative Temporal Reasoning, Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems (Participants Version), C-cube, the French National Concurrency Project, June 12–14, 1989.Google Scholar
  25. [FL79]
    Fischer, M., and Ladner, R., Propositional Dynamic Logic of Regular Programs, JCSS, vol. 18, no. 2, pp. 194–211, 1979.Google Scholar
  26. [GB87]
    Gerth, R., and Boucher, A., A Timed Failures Model for Extending Communicating Processes, In Proc. of the 14th Ann. ICALP, pp. 95–114, Springer LNCS no. 267, 1987.Google Scholar
  27. [He91]
    Henzinger, T., The Temporal Specification and Verification of Real Time Systems, PhD Thesis, Computer Science Department, Stanford University, August 1991, Technical Report STAN-CS-91-1380.Google Scholar
  28. [Ho91]
    Hooman, J. Specification and Compositional Verification of Real Time Systems, PhD Thesis, Eindhoven University of Technology, 1991.Google Scholar
  29. [JM86]
    Jahanian, F., and A. K. Mok, Safety Analysis of Timing Properties in Real Time Systems, IEEE Trans. Software Eng., SE-12(9), pp. 890–904, 1986.Google Scholar
  30. [JM87]
    Jahanian, F., A.K. Mok, A Graph-Theoretic Approach for Timing Analysis and its Implementation, IEEE Transactions on Computers, vol. C-36, no. 8, pp. 961–975, 1987.Google Scholar
  31. [JS88]
    Jahanian, F., and Mok, A., A Method for Verifying Properties of Modechart Specifications, Proc. of the Ninth IEEE Real-Time Systems Symposium, pp. 12–21, 1988.Google Scholar
  32. [Koy89]
    Koymans, R., Specifying Message Passing and Time Critical Systems with Temporal Logic, PhD Thesis, Eindhoven University of Technology, 1989.Google Scholar
  33. [Koy90]
    Koymans, R. Specifying Real Time Properties with Metric Temporal Logic, Real Time Systems, vol. 2, no. 4., pp. 255–299, 1990.CrossRefGoogle Scholar
  34. [KVD83]
    Koymans, R., Vytopil, J., and de Roever, W.-P., Real Time Programming and Asynchronous Message Passing, Proceedings of the Second Annual ACM Symp. on Principles of Distributed Computing (PODC), pp. 187–197, 1983.Google Scholar
  35. [Ko83]
    Kozen, D., Results on the Propositional μ-Calculus, Proc. 9th Annual International Colloquium on Automata, Languages and Programming, LNCS#140, Springer-Verlag, pp. 348–359, 1982; also appeared in Theoretical Computer Science, vol. 27, no. 3, pp. 333–354, 1983.Google Scholar
  36. [Le90]
    Lewis, H. R., A Logic of Concrete Time Intervals, Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS), IEEE Press, pp. 380–399, 1990.Google Scholar
  37. [LP85]
    Lichtenstein, O., A. Pnueli, Checking That Finite State Concurrent Programs Satisfy Their Linear Specification, Proc. 12th Annual ACM Symp. on Principles of Programming Languages, New Orleans, pp. 97–107, 1985.Google Scholar
  38. [LPZ85]
    Lichtenstein, O., A. Pnueli, L. Zuck, The Glory of The Past, Proc. Conf. on Logics of Programs, Brooklyn, R. Parikh, editor, LNCS#193, Springer-Verlag, pp. 196–218,1985.Google Scholar
  39. [MW84]
    Manna., Z., P. Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems, vol. 6, no. 1, pp. 68–93, 1984.CrossRefGoogle Scholar
  40. [Os90]
    Ostroff, J., Temporal Logic of Real-Time Systems, Research Studies Press, 1990.Google Scholar
  41. [Pn77]
    Pnueli, A., The Temporal Logic of Programs, 18th Annual Symp. on Foundations of Computer Science, Providence, pp. 46–57,1977.Google Scholar
  42. [PH88]
    Pnueli, A., and Harel, E., Application of Temporal Logic to the Specification of Real-Time Systems, in Formal Techniques in Real-Time and Fault Tolerant Systems, M. Joseph (ed.), Springer LNCS #331, 1988.Google Scholar
  43. [PR89]
    Pnueli, A., R. Rosner, On the Synthesis of a Reactive Module, Proc. 16th Annual ACM Symp. on Principles of Programming Languages, Austin, pp. 179–190, 1989.Google Scholar
  44. [QS81]
    Queille, J.P., J. Sifakis, Specification and Verification of Concurrent Systems in CESAR, Proc. of the 5th International Symposium on Programming, LNCS#137, Springer-Verlag, pp. 337–350, 1981.Google Scholar
  45. [Pr81]
    Pratt, V., A Decidable Mu-Calculus, 22nd FOCS, pp. 421–427, 1981.Google Scholar
  46. [SdeB69]
    Scott, D., and de Bakker, J., A Theory of Programs, unpublished notes, IBM seminar, Vienna, 1969.Google Scholar
  47. [SC82]
    Sistla, A.P., E.M. Clarke, The Complexity of Prepositional Linear Temporal Logics, Proc. of the 14th Annual ACM Symp. on Theory of Computing, San Francisco, pp. 159–168, 1982; also appeared in Journal ACM, vol. 32, no. 3, pp. 733–749, 1985.Google Scholar
  48. [SE84]
    Streett, R., Emerson, E. A., An Automata-Theoretic Decision Procedure for the Propositional Mu-calculus, ICALP84, also appears in Information and Computation, vol. 81, no. 3, June 1989., pp. 249–264.CrossRefGoogle Scholar
  49. [vB83]
    van Benthem, J., The Logic of Time, D. Reidel Pub. Co., 1983.Google Scholar
  50. [Wo83]
    Wolper, P., Temporal Logic can be More Expressive, Information and Control, 1983.Google Scholar
  51. [YR90]
    Yodaiken, V., and Ramamritham, K., Specifying and Verifiying a Real-Time Priority Queue with Modal Algebra, Proc. 11th IEEE Symp on Real-Time Systems, pp. 300–311, Dec. 5–7, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • E. Allen Emerson
    • 1
  1. 1.Computer Sciences DepartmentUniversity of Texas at AustinAustinUSA

Personalised recommendations