zbMATH — the first resource for mathematics

Expressing iterative properties logically in a symbolic setting. (English) Zbl 1108.68412
Rattray, Charles (ed.) et al., Algebraic methodology and software technology. 10th international conference, AMAST 2004, Stirling, Scotland, UK, July 12–16, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22381-9/pbk). Lecture Notes in Computer Science 3116, 460-474 (2004).
Summary: We present a logic for reasoning about state transition systems (LOTOS behaviours) which allows properties involving repeated patterns over actions and data to be expressed. The state transition systems are derived from LOTOS behaviours; however, the logic is applicable to any similar formalism. The semantics of the logic is given with respect to symbolic transition systems, allowing reasoning about data to be separated from reasoning about flow of control. Several motivational examples are included.
For the entire collection see [Zbl 1053.68007].
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI