Verification of Temporal Properties of Processes in a Setting with Data
Jan Friso Groote and Radu Mateescu
Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology AMAST'98 (Amazonia, Brazil),
January 1999.
Abstract:
We define a value-based modal mu-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 muCRL terms defined by linear process equations. The satisfaction of a temporal formula by a muCRL 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.
| 18 pages | |