An Introduction to History Dependent Automata

AbstractAutomata (or labeled transition systems) are widely used as operational models in the field of process description languages like CCS [13]. There are however classes of formalisms that are not modelled adequately by the automata. This is the case, for instance, of the π-calculus [15,14], an extension of CCS where channels can be used as values in the communications and new channels can be created dynamically. Due to the necessity to represent the creation of new channels infinite automata are obtained in this case also for very simple agents and a non-standard definition of bisimulation is required.In this paper we present an enhanced version of automata, called history dependent automata, that are adequate to represent the operational semantics of π-calculus and of other history dependent formalisms. We also define a bisimulation equivalence on history dependent automata, that captures π-calculus bisimulation. The results presented here are discussed in more detail in [21]