Abstract
An open system is a system whose behavior is jointly determined by its internal structure, and by the input it receives from the environment. To solve control and verification problems, open systems have often been modeled as games between the system and the environment; we argue that the game view of open systems should be extended also to the definitions of system refinement and composition. We give a symmetrical interpretation to games between system and environment: the moves of the system represent the outputs that the system can generate (the output guarantees), and symmetrically, the moves of the environment represent the inputs that the system can accept (the input assumptions). We argue in favor of defining refinement of open systems in terms of alternating simulation, which is the relation between games that plays the same role of simulation between transition systems. Alternating simulation captures the principle that a component refines another if it has weaker input assumptions, and stronger output guarantees. Furthermore, we argue in favor of a notion of composition that accounts for the compatibility between input assumptions and output guarantees, and that enables the synthesis of new input guarantees for the composed system. These game-theoretical notions of refinement and compatibility are related to the type-theoretical notions of subtyping and type compatibility, and give rise to an expressive modeling framework for component-based design and verification.
This research was supported in part by the NSF CAREER award CCR-0132780, the NSF grant CCR-0234690, and the ONR grant N00014-02-1-0671.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable concurrent program specifications. In Proc. 16th Int. Colloq. Aut. Lang. Prog., volume 372 of Lect. Notes in Comp. Sci., pages 1-17. Springer-Verlag, 1989.
S. Abramsky. Semantics of interaction. In Trees in Algebra and Programming — CAAP’96, Proc. 21st Int. Coll., Linküping, volume 1059 of Lect. Notes in Comp. Sci. Springer-Verlag, 1996.
S. Abramsky. Games in the semantics of programming languages. In Proc. of the 11th Amsterdam Colloquium, pages 1-6. ILLC, Dept. of Phylosophy, University of Amsterdam, 1997.
S. Abramsky, S. Gay, and R. Nagarajan. A type-theoretic approach to deadlock-freedom of asynchronous systems. In TACS’97: Theoretical Aspects of Comp uter Software. Third International Symposium, 1997.
S. Abramsky, K. Honda, and G. McCusker. A fully abstract game semantics for general references. In Proc. 13th IEEE Symp. Logic in Comp. Sci., pages 334-344. IEEE Computer Society Press, 1998.
S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Information and Computation, 163(2):409–470, 2000.
R. Alur and T. Henzinger. Reactive modules. Formal Methods in System Design, 15:7–48, 1999.
R. Alur, T. Henzinger, O. Kupferman, and M. Vardi. Alternating refinement relations. In CONCUR 98: Concurrency Theory. 9th Int. Conf., volume 1466 of Lect. Notes in Comp. Sci., pages 163-178. Springer-Verlag, 1998.
J. Baeten and W. Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.
A. Chakrabarti, L. de Alfaro, T. Henzinger, and F. Mang. Synchronous and bidirectional component interfaces. In CAV 02: Proc. of 14th Conf. on Computer Aided Verification, volume 2404 of Lect. Notes in Comp. Sci., pages 414-427. Springer-Verlag, 2002.
A. Chakrabarti, L. de Alfaro, T. Henzinger, and M. Stoelinga. Resource interfaces. In Proceedings of the Third International Workshop on Embedded Software (EMSOFT 2003), Lect. Notes in Comp. Sci. Springer-Verlag, 2003.
E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. In Proc. 19th ACM Symp. Princ. of Prog. Lang., pages 343-354, 1992.
E. Clarke, K. McMillan, S. Campos, and V. Hartonas-Garmhausen. Symbolic model checking. In CAV 96: Proc. of 8th Conf. on Computer Aided Verification, Lect. Notes in Comp. Sci., pages 419-422. Springer-Verlag, 1996.
L. de Alfaro and T. Henzinger. Interface automata. In Proceedings of the 8th European Software Engineering Conference and the 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 109-120. ACM Press, 2001.
L. de Alfaro and T. Henzinger. Interface theories for component-based design. In EMSOFT 01: 1st Intl. Workshop on Embedded Software, volume 2211 of Lect. Notes in Comp. Sci., pages 148-165. Springer-Verlag, 2001.
L. de Alfaro, T. Henzinger, and F. Mang. Detecting errors before reaching them. In CAV 00: Proc. of 12th Conf. on Computer Aided Verification, volume 1855 of Lect. Notes in Comp. Sci., pages 186-201. Springer-Verlag, 2000.
L. de Alfaro, T. Henzinger, and M. Stoelinga. Timed interfaces. In Proceedings of the Second International Workshop on Embedded Software (EMSOFT 2002), volume 2491 of Lect. Notes in Comp. Sci., pages 108-122. Springer-Verlag, 2002.
D. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, 1988.
T. Henzinger and R. Alur. Alternating-time temporal logic. J. ACM, 49:672–713, 2002.
T. Henzinger, S. Qadeer, and S. Rajamani. You assume, we guarantee: methodology and case studies. In CAV 98: Computer-aided Verification, volume 1427 of Lect. Notes in Comp. Sci., pages 440-451. Springer-Verlag, 1998.
T. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran. An assume-guarantee rule for checking simulation. In G. Gopalakrishnan and P. Windley, editors, FMCAD 98: Formal Methods in Computer-aided Design, Lecture Notes in Computer Science 1522, pages 421-432. Springer-Verlag, 1998.
C. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
R. Keller. Formal verification of parallel programs. Comm. ACM, 19(7):371–384, 1976.
O. Kupferman and M. Vardi. Module checking. In CAV 96: Proc. of 8th Conf. on Computer Aided Verification, volume 1102 of Lect. Notes in Comp. Sci., pages 75-86. Springer-Verlag, 1996.
N. Lynch. Distributed Algorithms. Morgan-Kaufmann, 1996.
N. Lynch and M. Tuttle. Hierarcical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. Princ. of Dist. Comp., pages 137-151, 1987.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.
Z. Manna and A. Pnueli. Models for reactivity. Acta Informatica, 30:609–678, 1993.
R. Milner. A Calculus of Communicating Systems, volume 92 of Lect. Notes in Comp. Sci. Springer-Verlag, 1980.
R. Milner. Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 1202–1242. Elsevier Science Publishers (North-Holland), Amsterdam, 1990.
J. Mitchell. Foundations for Programming Languages. MIT Press, 1996.
A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symp. Princ. of Prog. Lang., pages 179-190. ACM Press, 1989.
A. Pnueli and R. Rosner. On the synthesis of an asunchronous reactive module. In Proc. 16th Int. Colloq. Aut. Lang. Prog., volume 372 of Lect. Notes in Comp. Sci., pages 652-671, 1989.
W. Thomas. On the synthesis of strategies in infinite games. In Proc. of 12th Annual Symp. on Theor. Asp. of Comp. Sci., volume 900 of Lect. Notes in Comp. Sci., pages 1-13. Springer-Verlag, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
de Alfaro, L. (2003). Game Models for Open Systems. In: Dershowitz, N. (eds) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39910-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-39910-0_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21002-3
Online ISBN: 978-3-540-39910-0
eBook Packages: Springer Book Archive