Информационная система "Конференции"

Abstracts

Applications of logic in computer science

In this talk we show how definability theory can be fruitfully used for investigating interaction between continuous data and discrete devices. This phenomenon is usually formalised in framework of theory of hybrid systems.

We use first-order formulas with Pfaffian functions to represent continuous dynamic, discrete control and important regions such as initial conditions, invariants, guards and resets. These formalisations are called as Pfaffian hybrid systems.

Pfaffian hybrid systems are a sub-class of o-minimal hybrid systems which capture rich continuous dynamics and yet can be studied using finite bisimulations. Intuitively, if two systems are bisimilar their behavior is indistinguishable w.r.t. properties we consider. Therefore it is desirable to have bisimulations on which we can verify properties effectively, and in particular finite bisimulations.

We show the existence of finite bisimulations for Pfaffian hybrid systems and how the sizes of such bisimulations can be bounded. We also provide an algorithm for computing a finite bisimulation.

References

[KV04] M. Korovina, N. Vorobjov, Pfaffian hybrid systems, in Proc. of Computer Science Logic'04, Springer Lecture Notes in Comp. Sci., 3210, 2004, 430--441.

Mail to Webmaster alc9@math.nsc.ru

|Home Page| |English Part|

Go to Home