Verifying graph rewriting: coinductive techniques for nested conditions

Graphs are data structures that can be used to model a variety of concepts in computer science. To describe and analyze how such systems evolve over time, graph rewriting can be employed. Nested graph conditions can be used to characterize sets of graphs in a way similar to logical formulae, in order to restrict rule applications, define safety conditions, or specify contexts for comparing system behaviour. In this thesis, we will explore several methods for verification of graph rewriting systems, and generalizations thereof in the categorical framework of reactive systems. A basic building block for many verification tasks is an algorithm that checks whether a given condition is satisfiable or unsatisfiable. Since conditions have the expressive power of first-order logic, this is an undecidable problem. We describe a sound and complete procedure that semi-decides this problem: It can detect all unsatisfiable conditions having neither finite nor infinite models, and (in certain categories) all conditions with finite models. Due to undecidability, it is not possible to detect all conditions with only infinite models. However, witnesses for certain types of infinite models can still be generated. For verification, we apply counterexample-guided abstraction refinement (CEGAR) to graph rewriting. CEGAR is a program analysis technique based on predicate abstraction that can be used for reachability analysis and invariant checks. We use the satisfiability algorithm as part of the machinery to detect and eliminate spurious counterexamples. Furthermore, we investigate the notion of conditional bisimilarity, a type of behavioural equivalence which can be used to characterize and compare how systems behave in environments that satisfy a certain condition (as opposed to arbitrary environments). This is useful in situations where it is expected that their behaviour differs in certain contexts, yet equivalence in other contexts holds. To make the analysis of infinite state spaces feasible, we use representative squares and up-to techniques to make it easier to obtain finite and finitely branching conditional bisimulation relations (up-to context). For satisfiability checking and CEGAR, we present prototype tools and evaluate their performance compared to previous work. Compared to prior research, we obtain three major contributions: First, we use the framework of reactive systems that covers additional categories beyond graph categories, in particular cospan categories, in which weakest preconditions and strongest postconditions are much easier to compute compared to standard graph categories. Second, we can apply counterexample-guided abstraction refinement to graph rewriting. Third, we use techniques and up-to techniques for two distinct applications: to generate witnesses for infinite models and obtain a new perspective on the proofs of satisfiability checking procedures, and to obtain finite conditional bisimulation relations (up-to context) for infinite state spaces.