Coalgebraic minimization of HD-automata for the π-calculus using polymorphic types

22Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.

Abstract

We introduce finite-state verification techniques for the π-calculus whose design and correctness are justified coalgebraically. In particular, we formally specify and implement a minimization algorithm for HD-automata derived from π-calculus agents. The algorithm is a generalization of the partition refinement algorithm for classical automata and is specified as a coalgebraic construction defined using λ→,Π,Σ, a polymorphic λ-calculus with dependent types. The convergence of the algorithm is proved; moreover, the correspondence of the specification and the implementation is shown. © 2004 Elsevier B.V. All rights reserved.

Cite

CITATION STYLE

APA

Ferrari, G., Montanari, U., & Tuosto, E. (2005). Coalgebraic minimization of HD-automata for the π-calculus using polymorphic types. In Theoretical Computer Science (Vol. 331, pp. 325–365). https://doi.org/10.1016/j.tcs.2004.09.021

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free