The logic of ACP

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.