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.
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