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

摘要

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 λ{sup}(→,Π,Σ), a polymorphic λ-calculus with dependent types. The convergence of the algorithm is proved; moreover, the correspondence of the specification and the implementation is shown.