A Coinductive Equational Characterisation of Trace Inclusion for Regular Processes.

In 1966 Arto Salomaa gave a complete axiomatisation of regular expressions. It can be viewed as a sound and complete proof system for regular processes with respect to the behavioural equivalence called language equivalence. This proof system consists of a finite set of axioms together with one inductive proof rule. We show that the behavioural preorder called language containment or trace inclusion can be characterised in a similar manner, but using a coinductive rather than an inductive proof rule.