Who is pointing when to whom?

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

19 Citations (Scopus)

Abstract

This paper introduces an extension of linear temporal logic that allows to express properties about systems that are composed of entities (like objects) that can refer to each other via pointers. Our logic is focused on specifying properties about the dynamic evolution (such as creation, adaptation, and removal) of such pointer structures. The semantics is based on automata on infinite words, extended with appropriate means to model evolving pointer structures in an abstract manner. A tableau-based model-checking algorithm is proposed to automatically verify these automata against formulae in our logic.
Original languageUndefined
Title of host publicationFSTTCS 2004: foundations of software technology and theoretical computer science
EditorsK. Lodaya, M. Mahajan
Place of PublicationBerlin
PublisherSpringer
Pages250-262
ISBN (Print)3-540-24058-6
Publication statusPublished - 16 Dec 2004

Publication series

Name
NumberXVI
Volume3328
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • METIS-221294

Cite this

Distefano, D. S., Katoen, J. P., & Rensink, A. (2004). Who is pointing when to whom? In K. Lodaya, & M. Mahajan (Eds.), FSTTCS 2004: foundations of software technology and theoretical computer science (pp. 250-262). Berlin: Springer.
Distefano, D.S. ; Katoen, Joost P. ; Rensink, Arend. / Who is pointing when to whom?. FSTTCS 2004: foundations of software technology and theoretical computer science. editor / K. Lodaya ; M. Mahajan. Berlin : Springer, 2004. pp. 250-262
@inproceedings{a66abffe3d1140368176557f0cc05787,
title = "Who is pointing when to whom?",
abstract = "This paper introduces an extension of linear temporal logic that allows to express properties about systems that are composed of entities (like objects) that can refer to each other via pointers. Our logic is focused on specifying properties about the dynamic evolution (such as creation, adaptation, and removal) of such pointer structures. The semantics is based on automata on infinite words, extended with appropriate means to model evolving pointer structures in an abstract manner. A tableau-based model-checking algorithm is proposed to automatically verify these automata against formulae in our logic.",
keywords = "METIS-221294",
author = "D.S. Distefano and Katoen, {Joost P.} and Arend Rensink",
year = "2004",
month = "12",
day = "16",
language = "Undefined",
isbn = "3-540-24058-6",
publisher = "Springer",
number = "XVI",
pages = "250--262",
editor = "K. Lodaya and M. Mahajan",
booktitle = "FSTTCS 2004: foundations of software technology and theoretical computer science",

}

Distefano, DS, Katoen, JP & Rensink, A 2004, Who is pointing when to whom? in K Lodaya & M Mahajan (eds), FSTTCS 2004: foundations of software technology and theoretical computer science. Springer, Berlin, pp. 250-262.

Who is pointing when to whom? / Distefano, D.S.; Katoen, Joost P.; Rensink, Arend.

FSTTCS 2004: foundations of software technology and theoretical computer science. ed. / K. Lodaya; M. Mahajan. Berlin : Springer, 2004. p. 250-262.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Who is pointing when to whom?

AU - Distefano, D.S.

AU - Katoen, Joost P.

AU - Rensink, Arend

PY - 2004/12/16

Y1 - 2004/12/16

N2 - This paper introduces an extension of linear temporal logic that allows to express properties about systems that are composed of entities (like objects) that can refer to each other via pointers. Our logic is focused on specifying properties about the dynamic evolution (such as creation, adaptation, and removal) of such pointer structures. The semantics is based on automata on infinite words, extended with appropriate means to model evolving pointer structures in an abstract manner. A tableau-based model-checking algorithm is proposed to automatically verify these automata against formulae in our logic.

AB - This paper introduces an extension of linear temporal logic that allows to express properties about systems that are composed of entities (like objects) that can refer to each other via pointers. Our logic is focused on specifying properties about the dynamic evolution (such as creation, adaptation, and removal) of such pointer structures. The semantics is based on automata on infinite words, extended with appropriate means to model evolving pointer structures in an abstract manner. A tableau-based model-checking algorithm is proposed to automatically verify these automata against formulae in our logic.

KW - METIS-221294

M3 - Conference contribution

SN - 3-540-24058-6

SP - 250

EP - 262

BT - FSTTCS 2004: foundations of software technology and theoretical computer science

A2 - Lodaya, K.

A2 - Mahajan, M.

PB - Springer

CY - Berlin

ER -

Distefano DS, Katoen JP, Rensink A. Who is pointing when to whom? In Lodaya K, Mahajan M, editors, FSTTCS 2004: foundations of software technology and theoretical computer science. Berlin: Springer. 2004. p. 250-262