On Concurrent Program Algebra and Demonic Automata

Regular expressions describe languages accepted by finite state automata with angelic nondeterminism. Regular expressions obey the axioms of Kleene algebra. We consider automata with demonic nondeterminism, using a different criterion for acceptance. The demonic nondeterminism corresponds to that of predicate transformers; it allows nondeterministic sequential and concurrent programs to be modelled. The corresponding regular expressions obey the axioms of the left (lazy) Kleene algebra. The algebra is extended with operators for parallel composition, intersection (to express that a program must satisfy multiple properties), complement (to express that a program must not have a certain property), and difference (to express that certain properties must be excluded). The “naive” algorithm for the equivalence of two automata is adapted to automata with demonic nondeterminism. The theory is implemented in an interactive notebook.