History Dependent Automata: from Location Bisimulation to Network Conscious Pi-Calculus

Often the states of systems include explicit information about resources acquired in the past, and possibly exposed in the observations decorating their transitions. Typically, but not necessarily, resources are atomic and thus can be conveniently represented as names. Among resources actually modeled in the past 18 years we can mention spatial locations, events and their causal links, Petri nets transition instances for history preserving bisimulation (and corresponding versions for contextual nets and graph grammars), pi-calculus free names and, most recently, graphs with nodes and links representing communication nets. Whenever new resources can be recursively created, such transition systems are infinite state, and thus mostly useless for model checking. However, if transitions are equipped with resource isomorphic transformations, finiteness can be achieved whenever the size of states is bounded. Labeled transition systems with this capability are generically named History Dependent (HD) automata. They enjoy a convenient notion of bisimulation and sometimes a minimal HD automaton does exist. In the talk we will present an historical perspective of the various kinds of HD automata, and then we will present in a rather informal way an approach apt to see all the existing HD automata as instances of a unique categorical model based on coalgebras on free coproduct completions (families), indexed by symmetries. The correspondence with more classical models based on coalgebras on functor categories from an index category to category Set (presheaves) has been shown in work by Ciancia, Fiore, Gadducci, Kurz, Miculan, Montanari and Staton. The category of the latter kind of coalgebras is isomorphic to the category of HD automata, and thus they have equivalent terminal objects (minimal automata), but HD automata are often finite while coalgebras on presheaves are almost always infinite state. Furthermore, iterative algorithms based on partition refinement (terminal sequences) do apply. The existing theory allows to smoothly define theory and practice of Network Conscious pi-calculus (NCPi), a proper extension of the pi-calculus with an explicit notion of communication networks as resources. Thus NCPi agents can be equipped with network isomorphisms as symmetries, HD bisimulations and minimal realizations. The PhD thesis by Matteo Sammartino, now under examination at Pisa, introduces NCPi, and models in it Pastry, a generic, scalable and efficient substrate for peer-to-peer applications based on a distributed hash table. In modeling Pastry, the ability of observing routing properties, as allowed by an explicit representation of communication networks, is essential