Time-constrained automata | SpringerLink
Skip to main content
Springer Nature Link
Log in

Time-constrained automata

  • Selected Presentations
  • Conference paper
  • First Online:
CONCUR '91 (CONCUR 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 527))

Included in the following conference series:

Abstract

In this paper, we augment the input-output automaton model in order to reason about time in concurrent systems, and we prove simple properties of this augmentation. The input-output automata model is a useful model for reasoning about computation in concurrent and distributed systems because it allows fundamental properties such as fairness and compositionality to be expressed easily and naturally. A unique property of the model is that systems are modeled as the composition of autonomous components. This paper describes a way to add a notion of time to the model in a way that preserves these properties. The result is a simple, compositional model for real-time computation that provides a convenient notation for expressing timing properties such as bounded fairness.

(Extended Abstract)

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking for real-time systems. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pages 414–425. IEEE, June 1990.

    Google Scholar 

  2. Rajeev Alur and Thomas A. Henzinger. Real-time logics: Complexity and expressiveness. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pages 390–401. IEEE, June 1990.

    Google Scholar 

  3. Hagit Attiya and Nancy Lynch. Time bounds for real-time process control in the presence of timing uncertainty. Technical Memo MIT/LCS/TM-403, MIT Laboratory for Computer Science, July 1989.

    Google Scholar 

  4. Bard Bloom. Constructing two-writer atomic registers. In Proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing, pages 249–259. ACM, August 1987.

    Google Scholar 

  5. K. Mani Chandy and Jayadev Misra. The drinking philosophers problem. ACM Transactions on Programming Languages and Systems, 6(4):632–646, 1984.

    Google Scholar 

  6. David L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. PhD thesis, Department of Computer Science, Carnegie Mellon University, February 1988. Available as Technical Report CMU-CS-88-119.

    Google Scholar 

  7. Nissim Francez. Fairness. Springer-Verlag, Berlin, 1986.

    Google Scholar 

  8. Richard Gerber and Insup Lee. CCSR: A calculus for communicating shared resources. In J. C. M. Baeten and J. W. Klop, editors, Lecture Notes in Computer Science, volume 458, Proceedings of Concur '90, pages 263–277. Springer-Verlag, August 1990.

    Google Scholar 

  9. Maurice Herlihy. Impossibility and universality results for wait-free synchronization. In Proceedings of the 7th Annual ACM Symposium on Principles of Distributed Computing, pages 276–290. ACM, August 1988.

    Google Scholar 

  10. Eyal Harel, Orna Lichtenstein, and Amir Pnueli. Explicit clock temporal logic. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pages 401–413. IEEE, June 1990.

    Google Scholar 

  11. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, New Jersey, 1985.

    Google Scholar 

  12. Bengt Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Uppsala University, Uppsala, Sweden, 1987. Published by Direkt Offset, Nyström & Co AB, Uppsala.

    Google Scholar 

  13. [KSdR+88] R. Koymans, R. K. Shyamasundar, W. P. de Roever, R. Gerth, and S. Arun-Kumar. Compositional semantics for real-time distributed computing. Information and Computation, 79:210–256, 1988.

    Google Scholar 

  14. Nancy A. Lynch and Hagit Attiya. Using mappings to prove timing properties. In Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing, pages 265–280. ACM, August 1990.

    Google Scholar 

  15. Leslie Lamport. A temporal logic of actions. Research Report 57, DEC Systems Research Center, January 1991.

    Google Scholar 

  16. Harry R. Lewis. A logic of concrete time intervals. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pages 380–389. IEEE, June 1990. Also available at Harvard Technical Report TR-07-90.

    Google Scholar 

  17. Nancy A. Lynch and Michael J. Fischer. On describing the behavior and implementation of distributed systems. Theoretical Computer Science, 13(1):17–43, January 1981.

    Google Scholar 

  18. Nancy A. Lynch and Michael Merritt. Introduction to the theory of nested transactions. Theoretical Computer Science, 62:123–185, 1988. Earlier versions appeared in Proceedings of the International Conference on Database Theory, 1986, and as MIT Technical Report MIT/LCS/TR-367.

    Google Scholar 

  19. Nancy A. Lynch, Yishay Mansour, and Alan Fekete. Data link layer: Two impossibility results. In Proceedings of the 7th Annual ACM Symposium on Principles of Distributed Computing, pages 149–170. ACM, August 1988. Also available as MIT Technical Report MIT/LCS/TM-355.

    Google Scholar 

  20. Nancy A. Lynch, Michael Merritt, William E. Weihl, and Alan Fekete. A theory of atomic transactions. In Proceedings of the International Conference on Database Theory, 1988. Also available as MIT Technical Memo MIT/LCS/TM-362.

    Google Scholar 

  21. Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing, pages 137–151. ACM, August 1987. A full version is available as MIT Technical Report MIT/LCS/TR-387.

    Google Scholar 

  22. Nancy A. Lynch and Mark R. Tuttle. An introduction to input/output automata. CWI-Quarterly, 2(3), 1989. Also available as MIT Technical Memo MIT/LCS/TM-373.

    Google Scholar 

  23. Robin Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science 92. Springer-Verlag, Berlin, 1980.

    Google Scholar 

  24. Faron Moller and Chris Tofts. A temporal calculus of communicating systems. In J. C. M. Baeten and J. W. Klop, editors, Lecture Notes in Computer Science, volume 458, Proceedings of Concur '90, pages 401–415. Springer-Verlag, August 1990.

    Google Scholar 

  25. A. Udaya Shankar and Simon S. Lam. Time-dependent distributed systems: Proving safety, liveness and real-time properties. Distributed Computing, pages 61–79, 1987.

    Google Scholar 

  26. Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. Master's thesis, Massachusetts Institute of Technology, Laboratory for Computer Science, April 1987. Available as MIT Technical Report MIT/LCS/TR-387.

    Google Scholar 

  27. Jennifer L. Welch, Leslie Lamport, and Nancy A. Lynch. A lattice-structured proof of a minimum spanning tree algorithm. In Proceedings of the 7th Annual ACM Symposium on Principles of Distributed Computing, pages 28–43. ACM, August 1988.

    Google Scholar 

  28. Wang Yi. Real-time behaviour of asynchronous agents. In J. C. M. Baeten and J. W. Klop, editors, Lecture Notes in Computer Science, volume 458, Proceedings of Concur '90, pages 502–520. Springer-Verlag, August 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. AT&T Bell Laboratories, 600 Mountain Avenue, 07974, Murray Hill, NJ

    Michael Merritt

  2. School of Computer Science, Carnegie Mellon University, 15213, Pittsburgh, PA

    Francesmary Modugno

  3. DEC Cambridge Research Lab, One Kendall Sq., Bldg. 700, 02139, Cambridge, MA

    Mark R. Tuttle

Authors
  1. Michael Merritt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Francesmary Modugno
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mark R. Tuttle
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jos C. M. Baeten Jan Frisco Groote

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Merritt, M., Modugno, F., Tuttle, M.R. (1991). Time-constrained automata. In: Baeten, J.C.M., Groote, J.F. (eds) CONCUR '91. CONCUR 1991. Lecture Notes in Computer Science, vol 527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54430-5_103

Download citation

  • DOI: https://doi.org/10.1007/3-540-54430-5_103

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54430-2

  • Online ISBN: 978-3-540-38357-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation