History-dependent automata: An introduction

In this paper we give an overview of History Dependent Automata, an extension of ordinary automata that overcomes their limitations in dealing with named calculi. In a named calculus, the observations labelling the transitions of a system may contain names which represent features such as communication channels, node identifiers, or the locations of the system. An example of named calculus is pi-calculus, which has the ability of sending channel names as messages and thus of dynamically reconfiguring process acquaintances and of modeling agents and code mobility. We show that History-Dependent Automata allow for a compact representation of pi-calculus processes which is suitable both for theoretical investigations and for practical purposes such as verification.