A Logic of Local Graph Shapes

Research output: Book/ReportReportProfessional

8 Downloads (Pure)

Abstract

Graphs are an intuitive model for states of a (software) system that involve dynamic resource allocation or pointer structures, such as, for instance, object-oriented programs. However, a straightforward encoding results in large individual states and large, or even unbounded, state spaces. As usual, some form of abstraction is necessary in order to arrive at a tractable model. In this paper we propose a fragment of first-order graph logic that we call local shape logic (LSL) as a possible abstraction mechanism. LSL is inspired by previous work of Sagiv, Reps and Wilhelm. An LSL formula constrains the multiplicities of nodes and edges in state graphs; abstraction is achieved by reasoning not about individual, concrete state graphs but about their characteristic shape properties. We show that the expressiveness of LSL is equal to integer programming, and as a consequence, LSL is decidable. (This is a slight generalisation of the decidability of two-variable first order logic.) We go on to define the concept of the canonical shape of a state graph, which is expressed in a monomorphic sub-fragment of LSL, for which we define a graphical representation. We show that the canonical shapes give rise to a finite abstraction of the state space of a software system, and we give an upper bound to the size of this abstract state space.
Original languageUndefined
Place of PublicationEnschede
PublisherSoftware Engineering (SE)
Number of pages33
Publication statusPublished - Aug 2003

Publication series

NameCTIT-technical reports
No.2003-35

Keywords

  • EWI-5816
  • METIS-217633
  • IR-47305

Cite this

Rensink, A. (2003). A Logic of Local Graph Shapes. (CTIT-technical reports; No. 2003-35). Enschede: Software Engineering (SE).
Rensink, Arend. / A Logic of Local Graph Shapes. Enschede : Software Engineering (SE), 2003. 33 p. (CTIT-technical reports; 2003-35).
@book{906705ae2b944edba36179004298bcc1,
title = "A Logic of Local Graph Shapes",
abstract = "Graphs are an intuitive model for states of a (software) system that involve dynamic resource allocation or pointer structures, such as, for instance, object-oriented programs. However, a straightforward encoding results in large individual states and large, or even unbounded, state spaces. As usual, some form of abstraction is necessary in order to arrive at a tractable model. In this paper we propose a fragment of first-order graph logic that we call local shape logic (LSL) as a possible abstraction mechanism. LSL is inspired by previous work of Sagiv, Reps and Wilhelm. An LSL formula constrains the multiplicities of nodes and edges in state graphs; abstraction is achieved by reasoning not about individual, concrete state graphs but about their characteristic shape properties. We show that the expressiveness of LSL is equal to integer programming, and as a consequence, LSL is decidable. (This is a slight generalisation of the decidability of two-variable first order logic.) We go on to define the concept of the canonical shape of a state graph, which is expressed in a monomorphic sub-fragment of LSL, for which we define a graphical representation. We show that the canonical shapes give rise to a finite abstraction of the state space of a software system, and we give an upper bound to the size of this abstract state space.",
keywords = "EWI-5816, METIS-217633, IR-47305",
author = "Arend Rensink",
note = "Imported from CTIT",
year = "2003",
month = "8",
language = "Undefined",
series = "CTIT-technical reports",
publisher = "Software Engineering (SE)",
number = "2003-35",

}

Rensink, A 2003, A Logic of Local Graph Shapes. CTIT-technical reports, no. 2003-35, Software Engineering (SE), Enschede.

A Logic of Local Graph Shapes. / Rensink, Arend.

Enschede : Software Engineering (SE), 2003. 33 p. (CTIT-technical reports; No. 2003-35).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - A Logic of Local Graph Shapes

AU - Rensink, Arend

N1 - Imported from CTIT

PY - 2003/8

Y1 - 2003/8

N2 - Graphs are an intuitive model for states of a (software) system that involve dynamic resource allocation or pointer structures, such as, for instance, object-oriented programs. However, a straightforward encoding results in large individual states and large, or even unbounded, state spaces. As usual, some form of abstraction is necessary in order to arrive at a tractable model. In this paper we propose a fragment of first-order graph logic that we call local shape logic (LSL) as a possible abstraction mechanism. LSL is inspired by previous work of Sagiv, Reps and Wilhelm. An LSL formula constrains the multiplicities of nodes and edges in state graphs; abstraction is achieved by reasoning not about individual, concrete state graphs but about their characteristic shape properties. We show that the expressiveness of LSL is equal to integer programming, and as a consequence, LSL is decidable. (This is a slight generalisation of the decidability of two-variable first order logic.) We go on to define the concept of the canonical shape of a state graph, which is expressed in a monomorphic sub-fragment of LSL, for which we define a graphical representation. We show that the canonical shapes give rise to a finite abstraction of the state space of a software system, and we give an upper bound to the size of this abstract state space.

AB - Graphs are an intuitive model for states of a (software) system that involve dynamic resource allocation or pointer structures, such as, for instance, object-oriented programs. However, a straightforward encoding results in large individual states and large, or even unbounded, state spaces. As usual, some form of abstraction is necessary in order to arrive at a tractable model. In this paper we propose a fragment of first-order graph logic that we call local shape logic (LSL) as a possible abstraction mechanism. LSL is inspired by previous work of Sagiv, Reps and Wilhelm. An LSL formula constrains the multiplicities of nodes and edges in state graphs; abstraction is achieved by reasoning not about individual, concrete state graphs but about their characteristic shape properties. We show that the expressiveness of LSL is equal to integer programming, and as a consequence, LSL is decidable. (This is a slight generalisation of the decidability of two-variable first order logic.) We go on to define the concept of the canonical shape of a state graph, which is expressed in a monomorphic sub-fragment of LSL, for which we define a graphical representation. We show that the canonical shapes give rise to a finite abstraction of the state space of a software system, and we give an upper bound to the size of this abstract state space.

KW - EWI-5816

KW - METIS-217633

KW - IR-47305

M3 - Report

T3 - CTIT-technical reports

BT - A Logic of Local Graph Shapes

PB - Software Engineering (SE)

CY - Enschede

ER -

Rensink A. A Logic of Local Graph Shapes. Enschede: Software Engineering (SE), 2003. 33 p. (CTIT-technical reports; 2003-35).