2011/09/20 by Detlef Plump, Plump, Detlef, Robin Suri +3
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Model-Driven Software Engineering Techniques
paper · doi:10.14279/tuj.eceasst.39.658.669
openalex publication_date 2011/09/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/01
GP (for Graph Programs) is a rule-based, nondeterministic programming language for solving graph problems at a high level of abstraction, freeing programmers from dealing with low-level data structures. In this case study, we present a graph program which minimizes finite automata. The program represents an automaton by its transition diagram, computes the state equivalence relation, and merges equivalent states such that the resulting automaton is minimal and equivalent to the input automaton. We illustrate how the program works by a running example and argue that it correctly implements the minimization algorithm of Hopcroft, Motwani and Ullman. We also prove a quadratic upper bound for the number of rule schema applications used by the program.