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 suitable 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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Bergstra, J. A., & Middelburg, C. A. (2005). Model theory for process algebra. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3838 LNCS, 445–495. https://doi.org/10.1007/11601548_21
Mendeley helps you to discover research relevant for your work.