From ATP to timed graphs and hybrid systems (Q1323313)

The paper presents results of ongoing work aiming at the unification of some behavioral description formalisms for timed systems. We propose for the algebra of timed processes ATP a very general semantics in terms of a time domain. It is then shown how ATP can be translated into a variant of timed graphs. This result allows the application of existing model- checking techniques to ATP. Finally, we propose a notion of hybrid systems as a generalization of timed graphs. Such systems can evolve, either by executing a discrete transition, or by performing some ``continuous'' transformation. The formalisms studied admit the same class of models: time deterministic and time continuous, possibly infinitely branching transition systems labeled by actions or durations.