Verification of temporal properties of processes in a setting with data

Abstract

We define a value-based modal /i-calculus, built from first-order formulas, modalities, and fixed point operators parameterized by data variables, which allows to express temporal properties involving data. We interpret this logic over /kCrl terms defined by linear process equations. The satisfaction of a temporal formula by a /kCrl term is translated to the satisfaction of a first-order formula containing parameterized fixed point operators. We provide proof rules for these fixed point operators and show their applicability on various examples.