Advertisement

Games I/O automata play

Extended abstract
  • Nick Reingold
  • Da -Wei Wang
  • Lenore D. Zuck
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)

Abstract

We introduce a game approach for specifying reactive systems. In particular, we define a simple two-player game between System and Environment, and consider the outcomes of such a game as a specification of a reactive system. We introduce six classes of game languages. We then show that the class of languages generated by I/O automata equals one of our game classes. An immediate corollary to the proof is that the fairness condition of I/O automata, which is defined as an extrinsic property by Lynch and Tuttle, can be incorporated as an intrinsic part of the automata. We also show closure properties of the six game classes. For example, we show that the class of languages defined by I/O automata is closed under union and hiding but not under intersection or complementation. The closure results are obtained by reasoning directly about games, thus demonstrating the advantage of the game-based approach.

Keywords

Expressive Power Parallel Composition Input Action Closure Property Countable Union 
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. 1.
    M. Abadi and L. Lamport. Composing specifications. Research Report 66, DEC SRC, October 1990.Google Scholar
  2. 2.
    J.A. Bergstra and J.W. Klop. Process theory based on bisimulation semantics. In LNCS 345, 1989.Google Scholar
  3. 3.
    B. Bloom. Constructing two-writer atomic registers. In Proc. 6th ACM Symp. on Principles of Distributed Computing, pages 249–259, 1987.Google Scholar
  4. 4.
    M. Broy, F. Dederichs, C. Dendorfer, and R. Weber. Characterizing the behavior of reactive systems by trace sets (extended abstract). In Third Workshop on Concurrency and Compositionality, March 1991.Google Scholar
  5. 5.
    A. Fekete, N. Lynch, M. Merritt, and W. Weihl. Commutativity-based locking for nested transactions. Journal of Computer and System Science. to appear.Google Scholar
  6. 6.
    A. Fekete, N. Lynch, and L. Shrira. A Modular Proof of Correctness for a Network Synchronizer, volume 312 of Lecture Notes in Computer Science, pages 219–256. Springer-Verlag, Amsterdam, Netherlands, July 1987.Google Scholar
  7. 7.
    J. Y. Halpern and R. Fagin. Modeling knowledge and action in distributed systems. Technical Report, IBM, RJ6303, 1988.Google Scholar
  8. 8.
    J. Y. Halpern and L. D. Zuck, A little knowledge goes a long way: Simple knowledgebased derivations and correctness proofs for a family of protocols. In Proc. 6th ACM Symp. on Principles of Distributed Computing, pages 269–280, 1987. To appear in JACM.Google Scholar
  9. 9.
    D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(33):231–278, 6 1987.zbMATHMathSciNetCrossRefGoogle Scholar
  10. 10.
    M. Hennessy. Algebraic Theory of Process. MIT Press, 1988.Google Scholar
  11. 11.
    M. Herlihy. Impossibility and universality results for wait-free synchronization. In Proc. 7th ACM Symp. on Principles of Distributed Computing, pages 276–290, 1988.Google Scholar
  12. 12.
    C.A.R. Hoare. Communicating Sequential Process. Prentice-Hall, 1985.Google Scholar
  13. 13.
    L. Lamport. Specifying concurrent program modules. ACM Trans. on Programming Languages and Systems, 5(2):190–222, 4 1983.zbMATHCrossRefGoogle Scholar
  14. 14.
    N. Lynch and M. Tuttle. An introduction to input/output automata. CWI Quarterly, 2(3):219–246, September 1989.zbMATHMathSciNetGoogle Scholar
  15. 15.
    N. A. Lynch, Y. Mansour, and A. Fekete. Data link layer: Two impossibility results. In Proc. 7th ACM Symp. on Principles of Distributed Computing, pages 149–170, August 1988.Google Scholar
  16. 16.
    N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. on Principles of Distributed Computing, pages 137–151, August 1987.Google Scholar
  17. 17.
    Z. Manna and A. Pnueli. The anchored version of temporal logic. In LNCS 354, pages 201–284, 1989.zbMATHMathSciNetGoogle Scholar
  18. 18.
    R. Milner. Concurrency and Communication. Prentice-Hall, 1989.Google Scholar
  19. 19.
    Y. N. Moschovakis. A game-theoretic modeling of concurrency. In Proc. of the 4th annual Symp. on Logic in Computer Science, pages 154–163. IEEE Computer Society Press, 1989.Google Scholar
  20. 20.
    Y. N. Moschovakis. Computable processes. In Proc. 18th ACM Symp. on Principles of Programming Languages, pages 72–80. IEEE Computer Society Press, 1990.Google Scholar
  21. 21.
    D.-W. Wang and L. D. Zuck. Real-time sequence transmission problem. In Proc. 10th ACM Symp. on Principles of Distributed Computing, August 1991.Google Scholar
  22. 22.
    D.-W. Wang, L. D. Zuck, and Nick Reingold. The power of I/O automata. Unpublished manuscript, December 1990.Google Scholar
  23. 23.
    J. Welch, L. Lamport, and N. Lynch. A lattice-structured proof of a minimum spanning tree algorithm. In Proc. 7th ACM Symp. on Principles of Distributed Computing, pages 28–43, August 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Nick Reingold
    • 1
  • Da -Wei Wang
    • 2
  • Lenore D. Zuck
    • 1
  1. 1.Department of Computer ScienceYale UniversityUSA
  2. 2.Department of Computer ScienceUniversity of DelawareUSA

Personalised recommendations