Verification and Design Tools

The conceptual underpining for intelligent, multi-agent systems is the ability to verify that the sensori-motor hierarchies perform as expected. As we have discussed the composite systems are hybrid, in that they have a mixture of discrete protocols and continuous actions. Verification or design for verification is a complex problem. In work in our group, we have produced interesting new approaches involving the use of game theory and differential inclusions. However, it is fair to say that the approaches have the following difficulties:

1. The model checking approaches of theoretical computer science, which are algorithmic grow in computational complexity very rapidly, with the end result that problems are undecidable in all but the simplest classes of hybrid systems: referred to as linear hybrid automata
2. Deductive approaches involving ``theorem proving'' techniques are ad-hoc and require considerable inspiration for deriving invariants associated with these methods.
3. The synthesis approach, which we have pioneered solves the problem of checking, but deriving ``pre-verified'' hybrid systems. However, it is based on a game and hence is verified to be ``worst case'' safe.

In our research on this project we propose a new approach to verification of the accurate functioning of ``safety critical systems''. The heart of the approach is to not verify that every run of the hybrid system satisfies certain safety or liveness parameters, rather to check that the properties are satisfied with a certain probability, given uncertainties of actuation and sensing. In this sense, this is a ``softening'' of the notion of verification and represents the rapproachment between stochastic control, Bayesian decision networks and soft computing that was mentioned above. Since the systems are safety critical, we will be interested in guarantees of performance which are in the percentile and higher category, in the unfaulted mode and slightly lower in the faulted modes.