The logic of ACP
Alban Ponse, Mark B. van der Zwaag · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 2002
We distinguish two interpretations for the truth value `undefined' in Kleene's three-valued logic. Combining these two interpretations leads to a four-valued propositional logic that characterizes two particular ingredients of process algebra: ``choice' and ``inaction'. We study two different bases for this logic, and prove some elementary results (on expressiveness and completeness). One has the classical symmetric connective conjunction and negation, while the other one only has a ternary if-then-else connective with a sequential, operational flavor. Combining this four-valued logic with process algebra yields a direct generalization of ACP with conditional composition that establishes the characterization of choice and inaction. For this generalization we present an operational semantics in SOS-style and some completeness results.