Dynamic input/output automata: A formal model for dynamic systems

Paul C. Attie, Nancy A. Lynch

Research output: Chapter in Book/Report/Conference proceedingConference contribution

18 Scopus citations


We present a mathematical state-machine model, the Dynamic I/O Automaton (DIOA) model, for defining and analyzing dynamic systems of interacting components. The systems we consider are dynamic in two senses: (1) components can be created and destroyed as computation proceeds, and (2) the events in which the components may participate may change. The new model admits a notion of external system behavior, based on sets of traces. It also features a parallel composition operator for dynamic systems, which respects external behavior, and a notion of simulation from one dynamic system to another, which can be used to prove that one system implements the other. The DIOA model was defined to support the analysis of mobile agent systems, in a joint project with researchers at Nippon Telephone and Telegraph. It can also be used for other forms of dynamic systems, such as systems described by means of object-oriented programs, and systems containing services with changing access permissions.

Original languageEnglish (US)
Title of host publicationConcurrency Theory - 12th International Conference, CONCUR 2001, Proceedings
EditorsMogens Nielsen, Kim G. Larsen
PublisherSpringer Verlag
Number of pages15
ISBN (Print)3540424970
StatePublished - Jan 1 2001
Externally publishedYes
Event12th International Conference on Concurrency Theory, CONCUR 2001 - Aalborg, Denmark
Duration: Aug 20 2001Aug 25 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference12th International Conference on Concurrency Theory, CONCUR 2001

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Dynamic input/output automata: A formal model for dynamic systems'. Together they form a unique fingerprint.

Cite this