A Logic of Local Graph Shapes


Rensink, A. (2003) A Logic of Local Graph Shapes. [Report]

open access
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.
Item Type:Report
Copyright:©2003 CTIT
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/47305
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 217633