P. Cousot, Methods and Logics for Proving Programs

Parameterized System Verification: Does Process's Knowledge Affect Decidability?

Abstract: It has been well-known that any non-trivial properties of parameterized finite systems is in general undecidable. However all previous undecidability proofs reply on the fact that processes have access to global configuration knowledge (such as system scale) or there is a distinguished (control) process which can collect such type of information. A question arises when we ask if there exists uniform procedure for determining a process's local properties, given a system in which no process can gain global configuration knowledge in any computations. It is shown here that the verification problem on this more restricted class of parameterized systems is still undecidable.The undecidability is established in a specific class of completely identical parameterized finite systems using reduction to \textit{tag systems}.