Concurrency and automata on infinite sequences

A general method for proving/deciding equivalences between omega-regular languages, whose recognizers are modified forms of Buchi or Muller-McNaughton automata, derived from Milner's notion of “simulation” is obtained.

Abstract

The paper is concerned with ways in which fair concurrency can be modelled using notations for omega-regular languages — languages containing infinite sequences, whose recognizers are modified forms of Büchi or Muller-McNaughton automata. There are characterization of these languages in terms of recursion equation sets which involve both minimal and maximal fixpoint operators. The class of ω-regular languages is closed under a fair concurrency operator. A general method for proving/deciding equivalences between such languages is obtained, derived from Milner's notion of "simulation".