Proving Approximate Implementations for Probabilistic I/O Automata

Sayan Mitra, Nancy Lynch

Research output: Contribution to journalArticlepeer-review


In this paper we introduce the notion of approximate implementations for Probabilistic I/O Automata (PIOA) and develop methods for proving such relationships. We employ a task structure on the locally controlled actions and a task scheduler to resolve nondeterminism. The interaction between a scheduler and an automaton gives rise to a trace distribution-a probability distribution over the set of traces. We define a PIOA to be a (discounted) approximate implementation of another PIOA if the set of trace distributions produced by the first is close to that of the latter, where closeness is measured by the (resp. discounted) uniform metric over trace distributions. We propose simulation functions for proving approximate implementations corresponding to each of the above types of approximate implementation relations. Since our notion of similarity of traces is based on a metric on trace distributions, we do not require the state spaces nor the space of external actions of the automata to be metric spaces. We discuss applications of approximate implementations to verification of probabilistic safety and termination.

Original languageEnglish (US)
Pages (from-to)71-93
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
Issue number8
StatePublished - Jun 20 2007
Externally publishedYes


  • Abstraction
  • Approximate implementation
  • Approximate simulation
  • Probabilistic I/O Automata
  • equivalence

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Proving Approximate Implementations for Probabilistic I/O Automata'. Together they form a unique fingerprint.

Cite this