A Formal Axiomatization for Alphabet Reasoning with Parametrized Processes

In the process-algebraic veri cation of systems with three or more components put in parallel, alphabet axioms are considered to be very useful. These are rules that exploit the information about the alphabets of the processes involved. The alphabet of a process is the set of actions it can perform. In this paper, we extend CRL (a formal proof system for ACP + data) with such axioms. The alphabet axioms that are added to the proof theory are completely formal and therefore highly suited for computer-checked veri cation. This is new compared to previous papers where the formulation of alphabet axioms relies for a considerable extend on informal data parameters and implicit (in nite) set theory.

• Type: Journal
• Year: 1998
• Where: FAC
• Authors: Henri Korver, M. P. A. Sellink
• Keywords: Computer-checked Veri Cation, FAC 1998, Process-algebraic Veri Cation, Veri Cation