Research Abstracts - 2006

A Framework for Modeling and Verification of Uncertain Hybrid Systems

Sayan Mitra & Nancy Lynch

Motivation

Many aspects of the behavior of hybrid systems [1] are subject to uncertainties; for example, the measurement of a signal obtained from a sensor is typically within some bound of the actual value, control algorithms often make use of random bits, the values of which are uncertain, and the dynamics of a hybrid system can be affected by an external disturbance, the exact nature of which may not be known. In the past few years, work has begun on developing modeling frameworks that combine probabilistic and hybrid features (see [2] for an overview of the proposed frameworks), however, none of these models allows both nondeterministic and probabilistic choices. We argue that, to capture uncertainties in real systems a modeling framework must allow both nondeterministic and probabilistic choices in describing the evolution of the system model. For instance, if we know that a random bit generator is unbiased, then we should be able to model it as a uniform random choice over {0, 1}. On the other hand, if the maximum error e of a temperature sensor is known but the distribution of the error is not known, then we should be able to model 79 F as a nondeterministic choice over the interval [79 - e, 79 + e]. Various models for hybrid systems are possible that accommodate both probabilistic and nondeterministic behavior. As a first step towards building a general mathematical framework for modeling and verification of uncertain hybrid systems, we develop an extension of the Probabilistic I/O automata model (PIOA) [3] that allows deterministic continuous evolution of state. We call this model Piecewise Deterministic Timed I/O Automaton (PDTIOA) [4]. PDTIOAs can capture, for instance, exponentially distributed transmission delays in communication channels, mobile nodes with inaccurate location information, and hybrid systems with mode switches brought about by a discrete time stochastic process. In this project we develop verification techniques and tools for the PDTIOA framework.

Approach

We develop the semantics of the PDTIOA model as an extension of the PIOA model. Combining continuous probability distributions with nondeterministic state transitions require us to address some fundamental measure-theoretic issues. First we carefully construct a probability measure over the space of executions of a given PDTIOA A. In order to do this, we construct a sigma-algebra on the set of executions of A and then define schedulers that will resolve all the nondeterminism and produce purely probabilistic executions of A. This probability measure over the space of executions automatically give us a corresponding probability measure over the space of traces (a trace is the externally visible part of an execution). We can use these measures over traces to define the notion of implementation for PDTIOAs as follows: consider PDTIOA A and B, we say that A implements B iff the set of trace distributions of A is included in the set of trace distributions of B. We also define the parallel composition operation for PDTIOAs and show that: (1) the class of PDTIOAs is closed under parallel composition, and (2) the parallel composition operation respects the notion of implementation defined above.

In traditional automata theory, simulation relations provide a powerful tool for proving that automaton A implements automaton B. Our next step in the development of the PDTIOA theory will be to define a suitable kind of simulation relations for PDTIOAs and prove that existence of such a relation does indeed guarantee implementation, in the sense of trace distribution inclusion. Another kind of proof technique that we will develop will be for proving safety properties of PDTIOAs. We will apply the PDTIOA model and the above-mentioned proof techniques for verification simple probabilistic hybrid systems.

Future work

The PDTIOA model subsumes several well known classes of stochastic processes like Jump Markov Processes and Randomly Switched Systems. In the future we would like to develop techniques for proving stability and invariance of PTIOAs by extending the analysis techniques that are known for the existing models. In the future we would also like to generalize the PDTIOA model so that we can capture hybrid systems whose trajectories are best described nondeterministically or by stochastic differential equations. Once we have such a model we will extend all the above concepts---trace distributions, simulation relations, implementation---and the proof techniques to fit this new, more general model.

References:

[1] N. Lynch, R. Segala, and F. Vaandrager. Hybrid I/O automata. Information and Computation,185(1):105-157, August 2003.

[2] J. Lygeros and A. van der Schaft, editors. Stochastic Hybrid Systems: Theory and Applications, Atlantis, Paradise Island, Bahamas, 2004. Workshop for the 43rd IEEE Conference on Decision and Control.

[3] R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, and R. Segala. Using probabilistic I/O automata to analyze an oblivious transfer protocol. Technical report, MIT LCS Technical Reports - MIT-LCS-TR-1001, August 2005. Also in MIT CSAIL Technical Reports - MIT-CSAIL-TR-2005-055.

[4] S. Mitra and N. Lynch. Piecewise Deterministic Timed I/O Automaton. Under submission. 2006.

[5] S. Mitra, D. Liberzon and N. Lynch. Verifying average dwell time by solving optimization problems. In Ashish Tiwari and Joao P. Hespanha, editors, Hybrid Systems: Computation and Control (HSCC 06), LNCS, Santa Barbara, CA, March 2006. Springer.