Abstract
We investigate the problem of synthesising an interface automaton R such that P || R ≼ Q, for given deterministic interface automata P and Q. We show that a solution exists iff P and Q ⊥ are compatible, and the most general solution is given by (P ∥ Q ⊥ ) ⊥ , where P ⊥ is the automaton P with inputs and outputs interchanged. We also characterise solutions in terms of winning input strategies in the automaton (P⊗Q ⊥ ) ⊥ , and the most general solution in terms of the most permissive winning strategy. We apply the synthesis problem for interfaces to the problem of synthesising converters for mismatched protocols.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S.: Semantics of interaction: an introduction to game semantics. In: Proceedings of the 1996 CLiCS Summer School, pp. 1–31. Cambridge University Press, Cambridge (1997)
Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)
Blass, A.: A game semantics for linear logic. Annals of Pure and Applied Logic 56, 183–220 (1992); Special Volume dedicated to the memory of John Myhill
Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, 295–311 (1969)
Calvert, K.L., Lam, S.S.: Formal methods for protocol conversion. IEEE Journal Selected Areas in Communications 8(1), 127–142 (1990)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering, pp. 109–120. ACM Press, New York (2001)
de Alfaro, L.: Game models for open systems. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 269–289. Springer, Heidelberg (2004)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Information and Computation 127(2), 164–185 (1996)
Kumar, R., Nelvagal, S., Marcus, S.I.: A discrete event systems approach for protocol conversion. Discrete Event Dynamic Systems 7(3), 295–315 (1997)
Lam, S.S.: Protocol conversion. IEEE Transactions on Software Engineering 14(3), 353–362 (1988)
Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, August 10–12, pp. 137–151 (1987)
Madhusudan, P., Thiagarajan, P.S.: Controllers for discrete event systems via morphisms. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 18–33. Springer, Heidelberg (1998)
Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995)
Passerone, R., de Alfaro, L., Henzinger, T.A., Sangiovanni-Vincentelli, A.L.: Convertibility verification and converter synthesis: Two faces of the same coin. In: ICCAD 2002: Proceedings of the International Conference on Computer Aided Design, pp. 132–140. ACM, New York (2002)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989. Proceedings of the sixteenth annual ACM symposium on Principles of programming languages, Austin, TX, January 11–13, pp. 179–190. ACM Press, New York (1989)
Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proceedings of the IEEE; Special issue on Dynamics of Discrete Event Systems 77(1), 81–98 (1989)
Tabuada, P.: Open maps, alternating simulations and control synthesis. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 466–480. Springer, Heidelberg (2004)
Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)
Yevtushenko, N., Villa, T., Brayton, R.K., Petrenko, A., Sangiovanni-Vincentelli, A.: Solution of parallel language equations for logic synthesis. In: Proceedings of the 2001 International Conference on Computer-Aided Design (ICCAD 2001), November 4–8, pp. 103–111. IEEE Computer Society Press, Los Alamitos (2001)
Yevtushenko, N., Villa, T., Brayton, R.K., Petrenko, A., Sangiovanni-Vincentelli, A.: Solution of synchronous language equations for logic synthesis. In: Proceedings of the 4th Conference on Computer-Aided Technologies in Applied Mathematics, September 2002, pp. 132–137 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bhaduri, P. (2005). Synthesis of Interface Automata. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_26
Download citation
DOI: https://doi.org/10.1007/11562948_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)