Keynote Abstract Timed and Probabilistic I/O Automata

The Timed I/O Automata (TIOA) modeling framework has been used for describing and analyzing many distributed algorithms, ranging from data-management algorithms to clock-synchronization algorithms to robot-coordination algorithms. These algorithms include timing aspects, and both discrete and continuous behavior. In this talk, I will describe the TIOA framework in some detail, and summarize many of the examples to which it has been applied. Then, I will discuss the extensions that are needed to enable it to handle more kinds of algorithms. These extensions will mainly involve adding and integrating features for handling probabilistic choices. I will review the state of the art for Probabilistic Timed I/O Automata models, and describe the work that I think is still needed.