Recently, several authors have been interested in exploiting possible independencies between transitions of a concurrent program in order to improve state-space exploration techniques. It has been shown that carefully tracking local (in-)dependencies can yield improvements in the performances of such techniques. In our talk, we will present an automaton model for such situations. We show how to represent concurrent computations by partial orders and how to use various logics to specify these orders and thus properties of the computations. In particular, we show that formulas of monadic second order logic only define languages of concurrent computations which are recognizable (and viceversa), and these can be constructed from finite languages using c-rational expressions. This generalizes various recent results in trace theory.
| Page d'accueil Irisa | Manifestations
scientifiques | Comment se rendre
ŕ l'Irisa ? |
webmaster@irisa.fr, déc. 1997