HISTORY-DEPENDENT AUTOMATA

			       Marco Pistore
		      (Joint work with Ugo Montanari)

Automata are often used as operational models for process algebras
(e.g., Milner's CCS), since they allow for a simple representation of
process behavior and since preorders and equivalences can be often
defined directly on them; one of the most important of these
equivalences is bisimilarity. Efficient and practical techniques and
tools for verification have been developed for ordinary automata.
Automata can also be easily defined in a categorical context --- as
particular diagrams in the category of sets --- so that an arrow from
automaton A_1 to automaton A_2 represents a simulation in A_2 of the
behaviors of A_1.  Also bisimilarity can be defined in a categorical
framework: the idea is to identify those arrows A_1 ---> A_2 which
guarrantee not only that A_2 can simulate the behavior of A_1, but
also the converse.  A categorical approach for the definition of these
"bisimulation morphisms" has been proposed by Joyal, Nielsen and
Winskel --- they have called the bisimulation morphisms "open maps".

Unfortunately, in many interesting cases ordinary automata cannot be
successfully applied.  A paradigmatic example is provided by
pi-calculus.  This calculus can be considered as a foundational
calculus for concurrent functional languages, as lambda-calculus for
sequential functional languages.  In pi-calculus names are used to
represent channels: transitions can create new channels among the
processes and these channels can then be used for subsequent
communications. Ordinary automata are not adequate to represent
dynamic creation of names, so that also very simple processes give
rise to infinite-state transition systems.  This is a general problem
for the class of history-dependent calculi.  A calculus is history
dependent if the observations labeling the transitions of an agent may
refer to informations --- names in the case of pi-calculus ---
generated in previous transitions of the agent. A richer structure
than ordinary automata is required to deal with these calculi.

HD-automata are a general model for history-dependent calculi. As
ordinary automata, they are composed of states and of transitions
between states. To deal with the peculiar problems of
history-dependent calculi, however, states and transition are enriched
with sets of local names: in particular, each transition can refer to
the names associated to its source state but can also generate new
names, which can then appear in the destination state.  In this
manner, the names are not global and static, as in ordinary automata,
but they are explicitly represented within states and transitions and
can be dynamically created. HD-automata can be defined in a
categorical framework. The category of HD-automata is obtained from
the category of ordinary automata simply by replacing the category of
"sets" with a suitable category of "named sets" in the definition.
Open maps can also be exploited to obtain a HD-bisimilarity relation
on HD-automata.

Pi-calculus agents can be translated into HD-automata and a first sign
of the adequacy of HD-automata for dealing with pi-calculus is that a
large class of pi-calculus agents can be represented by finite-state
HD-automata.  Moreover, HD-bisimulation equates the HD-automata
obtained from two pi-calculus agents if and only if the agents are
bisimilar according to the ordinary (strong, early) pi-calculus
bisimilarity relation.  Hence HD-automata are an interesting model
for history-dependent calculi.