Equations between regular terms and an application to process logic
Ashok Kumar Chandra, Joe Halpern, Albert R. Meyer, Rohit Parikh · 1981
Regular terms with the Kleene operations ∪,;, and * can be thought of as operators on languages, generating other languages. An equation r1 = r2 between two such terms is said to be satisfiable 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.