A Tool for Implementing Action Graphs

Milner introduced the action calculus framework as a graphical framework for describing many models of interactive behaviour. We describe a specification tool for action graphs, which allows the user to naturally switch between between the syntactic and graphical presentations. The implementation includes a type-checking algorithm on reduction rules, which uses a decision procedure for a variant of word unification, and a general matching algorithm for identifying redexes in a graph. Introduction Milner introduced the action calculus framework as a framework for describing many models of interactive behaviour, where a graph corresponds to a process and the dynamics (or reduction) of a graph corresponds to interaction between processes. Milner's motivation arose in part from analysing natural graphs associated with the ß-calculus [3], which are not immediately apparent from the ß-calculus syntax. In contrast, there is a direct link between action graphs and the corresponding syntax. W..