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

Conference paper

First Online:

## 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.

## References

- [Ab80]Abrahamson, K. Decidability and Expressiveness of Logics of Processes, Ph.D. Thesis, Univ. of Washington, 1980.Google Scholar
- [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
- [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
- [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
- [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 - [Bu84]Burgess, J., Basic Tense Logic, in
*Handbook of Philosophical Logic*, D. Gabbay and F. Guenthner, eds., D. Reidel Pub. Co, 1984.Google Scholar - [CKS81]Chandra, A., Kozen, D., and Stockmeyer, L., Alternation, JACM, vol. 28, no. 1, pp. 114–133, 1981.CrossRefGoogle Scholar
- [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 - [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 - [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
- [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
- [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
- [deB80]de Bakker, J. W., Mathematical Theory of Program Correctness, Prentice-Hall, Englewood Cliffs, NJ, 1980.Google Scholar
- [deR76]de Roever, W.P., Recursive Program Schemes: Semantics and
*Proof Theory*, Mathematical Centre Tracts 70, Mathematisch Centrum, Amsterdam, 1976.Google Scholar - [deR91]de Roever, W.-P., editor, Real-Time: Theory in Practice, Springer LNCS, to appear.Google Scholar
- [Di76]Dijkstra, E.W.,
*A Discipline of Programming*, Prentice-Hall, 1976.Google Scholar - [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 - [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 - [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 - [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 - [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 - [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
- [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 - [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
- [FL79]Fischer, M., and Ladner, R., Propositional Dynamic Logic of Regular Programs, JCSS, vol. 18, no. 2, pp. 194–211, 1979.Google Scholar
- [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
- [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
- [Ho91]Hooman, J. Specification and Compositional Verification of Real Time Systems, PhD Thesis, Eindhoven University of Technology, 1991.Google Scholar
- [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
- [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 - [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
- [Koy89]Koymans, R., Specifying Message Passing and Time Critical Systems with Temporal Logic, PhD Thesis, Eindhoven University of Technology, 1989.Google Scholar
- [Koy90]Koymans, R. Specifying Real Time Properties with Metric Temporal Logic,
*Real Time Systems*, vol. 2, no. 4., pp. 255–299, 1990.CrossRefGoogle Scholar - [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
- [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 - [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
- [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 - [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 - [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 - [Os90]Ostroff, J., Temporal Logic of Real-Time Systems, Research Studies Press, 1990.Google Scholar
- [Pn77]Pnueli, A., The Temporal Logic of Programs,
*18th Annual Symp. on Foundations of Computer Science*, Providence, pp. 46–57,1977.Google Scholar - [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
- [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 - [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 - [Pr81]Pratt, V., A Decidable Mu-Calculus, 22nd FOCS, pp. 421–427, 1981.Google Scholar
- [SdeB69]Scott, D., and de Bakker, J., A Theory of Programs, unpublished notes, IBM seminar, Vienna, 1969.Google Scholar
- [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 - [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
- [vB83]van Benthem, J., The Logic of Time, D. Reidel Pub. Co., 1983.Google Scholar
- [Wo83]Wolper, P., Temporal Logic can be More Expressive, Information and Control, 1983.Google Scholar
- [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