Graphs and Decidable Transductions based on Edge Constraints

Nils Klarlund and Michael I. Schwartzbach

February 1994

Abstract:

We give examples to show that not even c-edNCE, the most general known notion of context-free graph grammar, is suited for the specification of some common data structures.

To overcome this problem, we use monadic second-order logic and introduce edge constraints as a new means of specifying a large class of graph families. Our notion stems from a natural dichotomy found in programming practice between ordinary pointers forming spanning trees and auxiliary pointers cutting across.

Our main result is that for certain transformations of graphs definable in monadic second-order logic, the question of whether a graph family given by a specification tex2html_wrap_inline23 is mapped to a family given by a specification tex2html_wrap_inline25 is decidable. Thus a decidable Hoare logic arises.

Available as PostScript, PDF, DVI.

 

Last modified: 2003-06-08 by webmaster.