| Bochvar-McCarthy logic and process algebra. Notre Dame (1998) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract We propose a combination of Bochvar’s strict three-valued logic, McCarthy’s sequential three-valued logic, and process algebra via the conditional guard construct. This combination entails the introduction of a new constant meaningless in process algebra. We present an operational semantics in SOS-style, and a completeness result for ACP with conditional guard construct and the proposed logic. 1Introduction An (immediate) error in an algorithm or program, such as reference to a nonexisting instruction, or a type clash, is often easily detectable. In order to model this feature in a concurrent setting, we consider process algebra with conditional guard construct and a variant of three-valued logic as a means to represent concurrent algorithms and programs. (Some motivation is given in Section 3.) In general, errors can be classified in at least two categories: divergencies which can be hard to detect and more simple ones, such as described above. In this paper we propose how to deal with the occurrence of the latter sort, which we further call meaningless, notation M. Inparticular, evaluation of a proposition ϕ may now lead to M, in which case the evaluation of ¬ϕ should of course also result in M. Thus the first logical identity we adopt is ¬M = M. In process algebra we introduce µ as a process representing the effect of the logical (error-)value M. The new constant µ is axiomatized 1 by x + µ = µ, µ · x = µ. Here + is the commutative operation denoting choice, and · represents sequential composition. So the process µ ruins each (future) alternative. We recall the conditional guard construct ϕ: → from Dijkstra [13] (roughly: if ϕ holds, then), which was introduced in process algebra with two-valued logic in Baeten and Bergstra [2] with the following typical laws where T denotes the value | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||