Decidabil ity Results in Automata and Process Theory
Yoram Hirshfeld, Faron Moller · 2015
The study of Process Algebra has received a great deal of attention since the pioneering work in the 1970s of the likes of R. Milner and C.A.R. Hoare. This attention has been merited as the formalism provides a natural framework for describing and analysing systems: concurrent systems are described naturally using constructs which have intuitive interpretations, such as notions of abstrac-tions and sequential nd parallel composition. The goal of such a formalism is to provide techniques for verifying the cor-rectness of a system. Typically this verification takes the form of demonstrat-ing the equivalence of two systems expressed within the formalism, respectively representing an abstract specification of the system in question and its imple-mentation. However, any reasonable process algebra allows the description of any computable function, and the equivalence problem--regardless of what rea-sonable notion of equivalence you consider--is readily seen to be undecidable in general. Much can be accomplished by restricting attention to (communicating) finite-state systems where the equivalence problem is just as quickly seen to be