Abstract
We present a first-order extension of the algebraic theory about
processes known as ACP and its main models.
Useful predicates on processes, such as deadlock freedom and
determinism, can be added to this theory through first-order
definitional extensions.
Model theory is used to analyse the discrepancies between identity in
the models of the first-order extension of ACP and bisimilarity of the
transition systems extracted from these models, and also the
discrepancies between deadlock freedom in the models of a first-order
definitional extension of this theory and deadlock freedom of the
transition systems extracted from these models.
First-order definitions are material to the formalization of an
interpretation of one theory about processes in another.
We give a comprehensive example of such an interpretation too.
Preprint available here.