Towards automata for branching time and partial order

Abstract

In this work we develop an automata framework for partial order structures with branching, for which we use trace systems. The aim is to investigate the prospects of decidable partial order logics of branching time, derivable from an automata framework. On the one hand we define automata for trace systems directly, which combine asynchronous automata for linear time with tree automata. On the other hand we develop a branching generalisation of Mazurkiewicz trace theory, which links branching concurrent behaviour with tree automata directly: the idea is to generalise interleaving sequences for partially ordered runs to interleaving trees for trace systems. This development can also be used for partial order reduction methods in model checking for branching time. The latter approach also exposes a problem for the specification of branching time and concurrent behaviour: the distinction between nondeterministic choice and parallelism cannot be maintained completely in the presence of confusion, a notion known from Petri net theory. We discuss several possible ways of coping with this problem. Also on the automata side there are a few surprises. In particular the emptiness problem is decidable as desired, but turns out to be co-NP-complete.