Trace-based semantics for probabilistic timed I/O automata

Sayan Mitra, Nancy Lynch

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


We describe the main features of the Probabilistic Timed I/O Automata (PTIOA) - a framework for modeling and analyzing discretely communicating probabilistic hybrid systems. A PTIOA can choose the post-state of a discrete transition either nondeterministically or according to (possibly continuous) probability distributions. The framework supports modeling of large systems as compositions of concurrently executing PTIOAs, which interact through shared transition labels. We develop a trace-based semantics for PTIOAs and show that PTIOAs are compositional with respect a new notion of external behavior.

Original languageEnglish (US)
Title of host publicationHybrid Systems
Subtitle of host publicationComputation and Control - 10th International Conference, HSCC 2007, Proceedings
Number of pages5
ISBN (Print)9783540714927
StatePublished - 2007
Externally publishedYes
Event10th International Conference on Hybrid Systems: Computation and Control, HSCC 2007 - Pisa, Italy
Duration: Apr 3 2007Apr 5 2007

Publication series

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


Other10th International Conference on Hybrid Systems: Computation and Control, HSCC 2007

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Trace-based semantics for probabilistic timed I/O automata'. Together they form a unique fingerprint.

Cite this