Abstract
We propose a coalgebraic model of the Fusion calculus based on HD-automata. The main advantage of the approach is that the partition refinement algorithm designed for HD-automata is easily adapted to handle Fusion calculus processes. Hence, the transition systems of Fusion calculus processes can be minimised according to the notion of observational semantics of the calculus. As a beneficial side effect, this also provides a bisimulation checker for Fusion calculus.
Work supported by the PROFUNDIS FET-GC project.
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
Abadi, M., Gordon, A.: A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation 148(1), 1–70 (1999)
Benton, N., Cardelli, L., Fournet, C.: Modern Concurrency Abstractions for C#. ACM Transactions on Programming Languages and Systems 26(5), 269–304 (2004)
Boreale, M., De Nicola, R.: A Symbolic Semantics for the π-calculus. Information and Computation 126(1), 34–52 (1996)
Bruni, R., Melgratti, H., Montanari, U.: Theoretical Foundations for Compensations in Flow Composition Languages. In: Annual Symposium on Principles of Programming Languages POPL 2005, pp. 209–220. ACM Press, New York (2005) (to appear)
Cattani, G.L., Sewell, P.: Models for Name-Passing Processes: Interleaving and Causal (Extended Abstract). In: Proceedings of the Fifteenth Annual IEEE Symposium on Logic in Computer Science, LICS 2000, pp. 322–333. IEEE Computer Society Press, Los Alamitos (2000)
Conchon, S., Le Fessant, F.: Jocaml: Mobile Agents for Objective-Caml. In: International Symposium on Agent Systems and Applications, October 1999, pp. 22–29. Palm Springs, California (1999)
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)
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)
Ferrari, G., Montanari, U., Tuosto, E.: Modular Verification of Systems via Service Coordination. In: Monterey Workshop 2004 (October 2004); To appear on the workshop post-proceedings
Ferrari, G., Montanari, U., Tuosto, E.: Coalgebraic Minimisation of HD-automata for the π-Calculus in a Polymorphic λ-Calculus. Theoretical Computer Science 331, 325–365 (2004) (to appear)
Fiore, M., Staton, S.: Comparing Operational Models of Name-Passing Process Calculi. In: Adamek, J. (ed.) Proc. CMCS 2004. ENTCS. Elsevier, Amsterdam (2004)
Gadducci, F., Miculan, M., Montanari, U.: About permutation algebras and sheaves (and named sets, too!). Technical Report UDMI/26/2003/RR, Department of Mathematics and Computer Science, University of Udine (2003)
Ghani, N., Victor, B., Yemane, K.: Relationally Staged Computation in the π-calculus. In: Procedings of CMCS 2004. ENTCS, vol. 11(106), pp. 105–120 (2004)
Hennessy, M., Lin, H.: Symbolic Bisimulations. Theoretical Computer Science 138(2), 353–389 (1995)
Laneve, C., Zavattaro, G.: Foundations of Web Transactions. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 282–298. Springer, Heidelberg (2005)
Lin, H.: Complete Inference Systems for Weak Bisimulation Equivalences in the π-Calculus. Information and Computation 180(1), 1–29 (2003)
Montanari, U., Pistore, M.: History Dependent Automata. Technical report, Computer Science Department, Università di Pisa, TR-11-98 (1998)
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, pp. 569–578. Springer, Heidelberg (2000)
Orava, F., Parrow, J.: An Algebraic Verification of a Mobile Network. Formal Aspects of Computing 4(5), 497–543 (1992)
Parrow, J., Victor, B.: The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. In: Proceedings of LICS 1998, pp. 176–185. IEEE Computer Society Press, Los Alamitos (1998)
Pistore, M.: History Dependent Automata. PhD thesis, Computer Science Department, Università di Pisa (1999)
Pistore, M., Sangiorgi, D.: A Partition Refinement Algorithm for the π-Calculus. Information and Computation 164(2), 467–509 (2001)
Roxburgh, U.: BizTalk Orchestration: Transactions, Exceptions, and Debugging (2001), Microsoft Corporation, Available at http://msdn.microsoft.com/library/en-us/dnbiz/html/bizorchestr.asp
Sangiorgi, D.: A Theory of Bisimulation for the π-Calculus. Acta Informatica 33(1), 69–97 (1996)
Tuosto, E., Victor, B., Yemane, K.: Polyadic History-Dependent Automata for the Fusion Calculus. Technical Report 2003-62, Department of Information Technology, Uppsala, Sweden (December 2003), Available at http://www.it.uu.se/research/reports/
Victor, B., Moller, F.: The Mobility Workbench — A Tool for the π-Calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 428–440. Springer, Heidelberg (1994)
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
Ferrari, G., Montanari, U., Tuosto, E., Victor, B., Yemane, K. (2005). Modelling Fusion Calculus using HD-Automata. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J. (eds) Algebra and Coalgebra in Computer Science. CALCO 2005. Lecture Notes in Computer Science, vol 3629. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11548133_10
Download citation
DOI: https://doi.org/10.1007/11548133_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28620-2
Online ISBN: 978-3-540-31876-7
eBook Packages: Computer ScienceComputer Science (R0)