Equations between regular terms and an application to process logic

Regular terms with the Kleene operations U,;, and ∗ can be thought of as operators on languages, generating other languages. An equation τ1 = τ2 between two such terms is said to be salisfiable just in case languages exist which make this equation true. We show that the satisfiability problem even for ∗-free regular terms is undecidable. Similar techniques are used to show that a very natural extension of the Process Logic of Harel, Kozen and Parikh is undecidable.