Expressing iterative properties logically in a symbolic setting

Carron Shankland; Jeremy Bryans; Lionel Morel

doi:10.1007/978-3-540-27815-3_35

Expressing iterative properties logically in a symbolic setting

Carron Shankland, Jeremy Bryans, Lionel Morel

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

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.

Original language	English
Title of host publication	Algebraic Methodology and Software Technology
Editors	Charles Rattray, Savitri Maharaj, Carron Shankland
Place of Publication	Berlin
Pages	460-474
Number of pages	15
Volume	3116
ISBN (Electronic)	978-3-540-27815-3
DOIs	https://doi.org/10.1007/978-3-540-27815-3_35
Publication status	Published - 2004

Keywords

LOTOS
formal verification
temporal logics
infinite state systems
symbolic representation

Access to Document

10.1007/978-3-540-27815-3_35

Cite this

@inproceedings{e4aa1a77741e4fdeb618be256be32c70,

title = "Expressing iterative properties logically in a symbolic setting",

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",

author = "Carron Shankland and Jeremy Bryans and Lionel Morel",

year = "2004",

doi = "10.1007/978-3-540-27815-3_35",

language = "English",

isbn = "978-3-540-22381-8",

volume = "3116",

pages = "460--474",

editor = "Charles Rattray and Savitri Maharaj and Carron Shankland",

booktitle = "Algebraic Methodology and Software Technology",

}

TY - GEN

T1 - Expressing iterative properties logically in a symbolic setting

AU - Shankland, Carron

AU - Bryans, Jeremy

AU - Morel, Lionel

PY - 2004

Y1 - 2004

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

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

KW - LOTOS

KW - formal verification

KW - temporal logics

KW - infinite state systems

KW - symbolic representation

U2 - 10.1007/978-3-540-27815-3_35

DO - 10.1007/978-3-540-27815-3_35

M3 - Conference proceeding

SN - 978-3-540-22381-8

VL - 3116

SP - 460

EP - 474

BT - Algebraic Methodology and Software Technology

A2 - Rattray, Charles

A2 - Maharaj, Savitri

A2 - Shankland, Carron

CY - Berlin

ER -

Expressing iterative properties logically in a symbolic setting

Abstract

Keywords

Access to Document

Fingerprint

Cite this