A Logic of Local Graph Shapes

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.