EECS 298-11: CAD Seminar (joint with Programming Language Seminar) Monday, May 12, 1997, 4pm ^^^^^^ ^^^ Soda Hall-- 405 ^^^^^^^^^^^^^^^ History-Dependent Automata Ugo Montanari Dipartimento di Informatica University of Pisa History-dependent (HD) automata are automata whose states are enriched with local names and whose transitions both refer to old names and declare new names. HD-automata are a good operational description of those models of computation which dynamically create new communication channels, like the pi-calculus. The model however is very general, being able to express via name references also causality and locality links. History-dependent automata (or at least some classes of them) can be efficiently mapped to ordinary labelled transition systems, which can then be checked for bisimilarity, model checked and minimized using existing tools. This result opens new perspectives about finite state verification of agents exibiting mobility and/or causality. A verification environment for $\pi$-calculus agents has been recently implemented in Pisa (in collaboration with Gianluigi Ferrari, Giovanni Ferro, Stefania Gnesi and Gioia Ristori) on top of an existing verification environment for process algebras: the JACK environment. It was demonstated at CONCUR'96 and will be soon available for distribution. (joint work with Marco Pistore)