Conference Proceeding

Expressing iterative properties logically in a symbolic setting

Citation

Shankland C, Bryans J & Morel L (2004) Expressing iterative properties logically in a symbolic setting. In: Rattray C, Maharaj S & Shankland C (eds.) Algebraic Methodology and Software Technology: Proceedings. Lecture Notes in Computer Science, 3116. Expressing iterative properties logically in a symbolic setting, Stirling, Scotland, 12.07.2004-16.07.2004. Berlin Heidelberg: Springer, pp. 460-474. http://link.springer.com/chapter/10.1007%2F978-3-540-27815-3_35; https://doi.org/10.1007/978-3-540-27815-3_35

Abstract
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.

Keywords
LOTOS; formal verification; temporal logics; infinite state systems; symbolic representation

StatusPublished
Title of seriesLecture Notes in Computer Science
Number in series3116
Publication date31/12/2004
URLhttp://hdl.handle.net/1893/10703
PublisherSpringer
Publisher URLhttp://link.springer.com/…3-540-27815-3_35
Place of publicationBerlin Heidelberg
ISSN of series0302-9743
ISBN978-3-540-22381-8
ConferenceExpressing iterative properties logically in a symbolic setting
Conference locationStirling, Scotland
Dates