Introduction

Computer systems, and their interactions with the real world, are becoming increasingly complicated. To model and analyze such systems, one needs a mathematical framework with the following features:

1. It should be based on some type of interacting state machines, to enable direct description of interacting system components.
2. It should be able to express a variety of features of real systems, for example, timing assumptions and guarantees, continuous evolution of real-world system components, and probabilistic behavior. It should be able to express any combination of these features.
3. It should support description of systems in a modular manner. Of course, it should support description of components and their interactions. In addition, it should allow description of systems at different levels of abstraction.
4. It should provide a basis for practical methods for proving correctness and performance properties of the modeled systems.

Examples of systems that can benefit from such a framework include Internet communication protocols, wireless ad hoc network systems, security protocols, and safety-critical real-time control systems.

Good models for timed systems and hybrid continuous/discrete systems have already been developed. For example, the new monograph by Kaynar, Lynch, Segala, and Vaandrager [1] contains a comprehensive description of our Timed I/O Automata modeling framework, complete with many examples, and the papers by Lynch, Segala, and Vaandrager [2,3] contain our Hybrid I/O Automaton framework. Both of these frameworks have excellent support for composition and abstraction.

On the other hand, we are still working on frameworks that incorporate probabilistic behavior. The key difficulty in constructing such frameworks is that the models need to include a combination of probabilistic and nondeterministic choice. This combination poses difficulties for composition results.

Approach

Since including probabilistic choice in the modeling framework poses problems, we are beginning by adding probabilistic choices to a simple untimed modeling framework---basic I/O Automata (without any facilities for expressing liveness). After we understand this case, we will add probabilities to our Timed and Hybrid I/O Automata frameworks.

The starting point for our probabilistic modeling work is the Probabilistic I/O Automata modeling framework described in Roberto Segala's PhD thesis and related papers [4,5,6,7] PIOAs are simple discrete state transition systems, in which several transitions may be enabled from the same state, and in which a transition may lead to a probability distribution on new state.

Segala's framework is quite natural and powerful; however, his treatment of composition is incomplete. For instance, he does not give a satisfactory definition for the ``external behavior'' of a Probabilistic I/O Automaton, nor for "implementation'' relationships between PIOAs. The nondeterministic choices of steps within each PIOA in a system, and among the different PIOAs in a system, are resolved by a powerful, omniscient "scheduler'' mechanism, which exposes much of the internal behavior of the system components. The exposed information must be taken into account in the external behavior and implementation definitions.

We are trying to restrict the scheduler mechanism so that it does not depend on internal behavior of the system components, in the hopes of obtaining simple and natural definitions for external behavior and implementation, with associated composition results.

Once we have done this, we will attempt to add probabilities to Timed and Hybrid I/O Automata. In those automata, states can changes as a result of both discrete transitions and continuous "trajectories''. At least initially, we will consider probabilistic choices in discrete transitions only, not in trajectories.

Progress

The Timed and Hybrid frameworks are essentially completed [1,2,3]. In our probabilistic work, Lynch, Segala, and Vaandrager [8,9] have proved a theorem that exactly characterizes Segala's notions of external behavior and implementation for PIOAs. We showed that these notions make extremely fine distinctions, essentially exposing the complete internal branching structure---both nondeterministic and probabilistic.

This limitation has led us to consider weaker scheduling mechanisms for resolving the nondeterministic choices in systems of PIOAs. In particular, we are interested in scheduling mechanisms that are restricted to use only information about the component PIOAs that is normally externally available: the sequence of external actions (trace) that has occurred so far, but not the internal actions, nor the states, nor the internal branching structure.

We have been considering a variety of such definitions, and are trying to determine which ones support composition results.

In particular, we identified a special case of PIOAs: "switched PIOAs'' [10]. Switched PIOAs have control actions that explicitly pass control between automata, thus resolving the nondeterministic choices of which component takes the next step. Each switched PIOA also has a local scheduler, which resolves nondeterministic choices within the automaton. For this special case, we have defined external behavior and implementation notions and proved compositionality results. We are now working on a journal version of this paper.

Another special case we are considering is that of "task-PIOAs", which are PIOAs augmented with a "task'' structure that describes different activities the PIOAs can perform. In a task-PIOA, the only nondeterministic choices are the choice of the next task. We are currently using task-PIOAs as the basis for modeling and analyzing an Oblivious Transfer security protocol. In that work, tasks are selected by a simple oblivious scheduler.

Future

We hope to settle on a nice set of definitions for scheduling, external behavior, and implementation for PIOAs. We will test the utility of our definitions by using them to analyze Oblivious Transfer and other security protocols. We then plan to develop a combined model that includes timing, hybrid, and probabilistic behavior.

Research Support

This research is supported by DARPA/AFOSR MURI Award F49620-02-1-0325 and NSF Award number: CCR-0326277

References

[1] Dilsun K. Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager. The Theory of Timed I/O Automata. Revised and shortened version of Technical MIT-LCS-TR-917a (from 2004), March, 2005.

[2] Nancy Lynch, Roberto Segala, and Frits Vaandrager. Compositionality for Probabilistic Automata. Technical Report MIT-LCS-TR-907, MIT Laboratory for Computer Science, Cambridge, MA 02139, September 2003.

[3] Nancy Lynch, Roberto Segala, and Frits Vaandraager. Hybrid I/O Automata. Information and Computation, 185()1:105-157, August, 2003.

[4] Roberto Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD Thesis, MIT Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA, May 1995. Also, Technical Report MIT/LCS/TR-676.

[5] Roberto Segala. A Compositional Trace-Based Semantics for Probabilistic Automata. In Insup Lee and Scott A. Smolka, editors, CONCUR 95: Concurrency Theory (6th International Conference, Philadelphia, Pennsylvania, August 1995), volume 962 of Lecture Notes in Computer Science, pages 234-248. Springer-Verlag 1995.

[6] Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250--273, August, 1995.

[7] Roberto Segala and Nancy Lynch. In Bengt Jonsson and Joachim Parrow, editors, 5th International Conference on Concurrency Theory (CONCUR'94, Uppsala, Sweden, August 1994), volume 836 of Lecture Notes in Computer Science, pages 481-496. Springer-Verlag 1994.

[8] Nancy Lynch, Roberto Segala, and Frits Vaandrager. Compositionality for Probabilistic Automata. In Roberto Amadio and Denis Lugiez, editors, CONCUR 2003 - Concurrency Theory (14th International Conference on Concurrency Theory, Marseille, France, September, 2003), volume 2761 of Lecture Notes in Computer Science, pages 208-221, Springer-Verlag, 2003.

[9] Nancy Lynch, Roberto Segala, and Frits Vaandrager. Compositionality for Probabilistic Automata. Submitted for journal publication.

[10] Ling Cheung, Nancy Lynch, Roberto Segala, and Frits Vaandrager. Switched Probabilistic I/O Automata. First International Colloquium on Theoretical Aspects of Computing, Guiyang, China, September 2004.