History Dependent Automata for Service Compatibility

  • Vincenzo Ciancia
  • Gian-Luigi Ferrari
  • Marco Pistore
  • Emilio Tuosto
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5065)


We use History Dependent Automata (HD-Automata) as a syntax-indepentend formalism to check compatibility of services at binding time in Service-Oriented Computing.

Informally speaking, service requests are modelled as pairs of HD-Automata \(\langle{C_o,C_r}\rangle\); C r describes the (abstract) behaviour of the searched service and C o the (abstract) behaviour guaranteed by the invoker. Symmetrically, service publication consists of a pair of HD-Automata \(\langle{S_o,S_r}\rangle\) such that S o provides an (abstraction of) of the behaviour guaranteed by the service and S r yields the requirement imposed to invokers. An invocation \(\langle{C_o,C_r}\rangle\) matches a published interface \(\langle{S_o,S_r}\rangle\) when C o simulates S r and S o simulates C r .


Model Check Service Request Garbage Collection Composite Service Label Transition System 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bouali, A., Gnesi, S., Larosa, S.: The Integration Project for the JACK Environment. Bulletin of the EATCS 54, 207–223 (1994)zbMATHGoogle Scholar
  2. 2.
    Ciancia, V., Montanari, U.: A name abstraction functor for named sets. In: Coalgebraic Methods in Computer Science 2008 (to appear, 2008)Google Scholar
  3. 3.
    Ferrari, G.L., Montanari, U., Tuosto, E.: Coalgebraic minimization of hd-automata for the pi-calculus using polymorphic types. Theoretical Computer Science 331(2-3), 325–365 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Ferrari, G., Ferro, G., Gnesi, S., Montanari, U., Pistore, M., Ristori, G.: An Automata Based Verification Environment for Mobile Processes. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 275–289. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  5. 5.
    Ferrari, G., Gnesi, S., Montanari, U., Pistore, M.: A Model Checking Verification Environment for Mobile Processes. ACM Transactions on Software Engineering and Methodology 12(4), 440–473 (2003)CrossRefGoogle Scholar
  6. 6.
    Ferrari, G., Montanari, U., Pistore, M.: Minimizing Transition Systems for Name Passing Calculi: A Co-algebraic Formulation. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 129–143. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Ferrari, G., Montanari, U., Tuosto, E.: From Co-algebraic Specifications to Implementation: The Mihda toolkit. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 319–338. Springer, Heidelberg (2003)Google Scholar
  8. 8.
    Ferrari, G., Montanari, U., Tuosto, E.: Coalgebraic Minimisation of HD-automata for the π-Calculus in a Polymorphic λ-Calculus. Theoretical Computer Science 331, 325–365 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Ferrari, G., Montanari, U., Tuosto, E., Victor, B., Yemane, K.: Modelling and Minimising the Fusion Calculus Using HD-Automata. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 142–156. Springer, Heidelberg (2005)Google Scholar
  10. 10.
    Gabbay, M., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13(3-5), 341–363 (2002)zbMATHCrossRefGoogle Scholar
  11. 11.
    Gadducci, F., Miculan, M., Montanari, U.: About permutation algebras (pre)sheaves and named sets. Higher-Order and Symbolic Computation 19(2-3), 283–304 (2006)zbMATHCrossRefGoogle Scholar
  12. 12.
    Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, I and II. Information and Computation 100(1), 1–40,41–77 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Montanari, U., Buscemi, M.: A First Order Coalgebraic Model of π-Calculus Early Observational Equivalence. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 449–465. Springer, Heidelberg (2002)Google Scholar
  14. 14.
    Montanari, U., Pistore, M.: Checking Bisimilarity for Finitary π-Calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 42–56. Springer, Heidelberg (1995)Google Scholar
  15. 15.
    Montanari, U., Pistore, M.: History Dependent Automata. Technical report, Dipartimento di Informatica, Università di Pisa, TR-11-98 (1998)Google Scholar
  16. 16.
    Montanari, U., Pistore, M.: π-Calculus, Structured Coalgebras, and Minimal HD-Automata. In: Leung, K.-S., Chan, L., Meng, H. (eds.) IDEAL 2000. LNCS, vol. 1983, Springer, Heidelberg (2000); An extended version will be published on Theoretical Computer Science Google Scholar
  17. 17.
    Montanari, U., Pistore, M.: Structured coalgebras and minimal hd-automata for the π-calculus. Theoretical Computer Science 340, 539–576 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Paige, R., Tarjan, R.: Three Partition Refinement Algorithms. SIAM Journal on Computing 16(6), 973–989 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Parrow, J., Victor, B.: The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. In: Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  20. 20.
    Pistore, M.: History Dependent Automata. PhD thesis, Università di Pisa, Dipartimento di Informatica, available at University of Pisa as PhD Thesis TD-5/99 (1999)Google Scholar
  21. 21.
    Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theoretical Computer Science 249(1), 3–80 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Sangiorgi, D., Walker, D.: The π-Calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Vincenzo Ciancia
    • 1
  • Gian-Luigi Ferrari
    • 1
  • Marco Pistore
    • 2
  • Emilio Tuosto
    • 3
  1. 1.Department of Computer ScienceUniversity of Pisa 
  2. 2.Center for Information Technology - IRST, Fondazione Bruno Kessler 
  3. 3.Department of Computer ScienceUniversity of Leicester 

Personalised recommendations