Marco Pistore
History Dependent Automata
Dipartimento di Informatica, Ph.D. Thesis TD - 5/99, March 1999.
Abstract
In this thesis we present
History-Dependent Automata (HD-automata
in brief). They are an extension
of ordinary automata that overcomes
their limitations in dealing with
history-dependent formalisms. In
a history-dependent formalism the
actions that a system can perform
carry information generated in the
past history of the system. The
most interesting example is the
pi-calculus: channel names can be
created by some actions and they
can then be referenced by successive
actions. Other examples are CCS
with localities and the history
preserving semantics of Petri nets
Ordinary automata are an unsatisfactory
operational model for the history
dependent formalisms: infinite automata
are obtained for all the systems
with infinite computations, even
for very simple ones; moreover, the
ordinary definition of bisimulation
does not apply in these cases, thus
preventing the reusage of standard
theories and algorithms. We define
three versions of HD-automata, that
have different features and different
expressive power. We show that HD
automata are an adequate model for
the history-dependent formalisms
by presenting translations of (early
late, open, and asynchronous) pi-calculus, of CCS with localities
and of Petri nets into HD-automata
Finite HD-automata are obtained
for significant classes of systems
with infinite computations. Moreover
we define HD-bisimulation, both
in a set-theoretical way (that is
suitable for automatic verification
in the case of finite HD-automata
and in a categorical way (via open
maps). HD-bisimulation captures
the classical definitions of bisimulation
on the considered history-dependent
formalisms. We also describe HAL
a verification environment for
history-dependent systems that is
based on HD-automata.
|