Elements of an automata theory over partial orders.
Wolfgang H Thomas · 1996
. A model of nondeterministic finite automaton over (finite) partial orders is introduced. It captures existential monadic second-order logic in expressive power and generalizes classical word automata and tree automata. Special forms, such as deterministic automata, are discussed, and logical and algorithmic properties are analyzed, like closure under complement and decidability of the nonemptiness problem. These questions are studied in the context of different classes of partial orders, such as trees, Mazurkiewicz traces, or rectangular grids. 1. Introduction While automata over strings and trees are a well-known, widely used, and robust model, with many applications in the specification and verification of concurrent programs, the area of "finite automata over partial orders" cannot be called an established subject, despite the fact that partial orders are a natural domain for the study of concurrency. A possible reason for this is that many properties of finite automata which are...