Systems of Graph Formulas and their Equivalence to Alternating Graph Automata

TL;DR

This paper introduces systems of graph formulas with recursion, demonstrating their equivalence to alternating graph automata, thereby bridging logic-based and automata-theoretic approaches to graph language specification.

Contribution

It extends previous graph formulas with recursion and proves their expressive equivalence to alternating graph automata, enabling logical representations of automata-based graph languages.

Findings

Equivalence between graph formula systems and alternating graph automata

Bidirectional translation between formulas and automata

Logical representation of automata-based graph languages

Abstract

Graph-based modeling plays a fundamental role in many areas of computer science. In this paper, we introduce systems of graph formulas with variables for specifying graph properties; this notion generalizes the graph formulas introduced in earlier work by incorporating recursion. We show that these formula systems have the same expressive power as alternating graph automata, a computational model that extends traditional finite-state automata to graphs, and allows both existential and universal states. In particular, we provide a bidirectional translation between formula systems and alternating graph automata, proving their equivalence in specifying graph languages. This result implies that alternating graph automata can be naturally represented using logic-based formulations, thus bridging the gap between automata-theoretic and logic-based approaches to graph language specification.