In this work we develop an automata framework for patial order structures with branching, for which we use trace systems. The aim is to investigate the prospects of decidable partial order logic of branching time, derivable from an automata framework. On the one hand we define automata ofr trace systems directly, which combine asynchronous automata for liear time with tree automata. On the other hand we develop a branching generalisation of Mazurkiewicz trace theory, which links brandching 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 ordr reduction methods in model checkign for branching time. Also on the automata side there are a few surprises. In particular the emptiness problem is decidable as desired, but turns out to the co-NP complete.
展开▼
