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.
|Semantics (msc 68Q55), Specification and verification (program logics, model checking, etc.) (msc 68Q60), Algebraic theory of languages and automata (msc 68Q70), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)|
|Software Engineering [SEN]|
Ponse, A, & van der Zwaag, M.B. (2002). The logic of ACP. Software Engineering [SEN]. CWI.