Reasoning About Data Trees Using CHCs

EasyChair Preprint 8615

Abstract

Reasoning about data structures requires powerful logics supporting the combination of structural and data properties. We define a new logic called MSO-D (Monadic Second Order logic with Data) as an extension of standard MSO on trees with predicates of the desired data logic. We also define a new class of symbolic data tree automata (SDTAs) to deal with data trees using a simple machine. MSO-D and SDTAs are both Turing-powerful, and their high expressiveness is necessary to deal with interesting data structures. We cope with undecidability by encoding SDTA executions as a CHC (Constrained Horn Clause) system, and solving the resulting system using off-the-shelf solvers. In particular, we identify a fragment of MSO-D whose satisfiability can be effectively reduced to the emptiness problem for SDTAs. This fragment is very expressive since it allows us to characterize a variety of data trees from the literature, capture extensions of temporal logics that involve data, games, etc. We implement this reduction in a prototype tool that combines an MSO decision procedure over trees (MONA) with a CHC engine (Z3), and use this tool to conduct several experiments, demonstrating the effectiveness of our approach across multiple problem domains.

Keyphrases: Constrained Horn Clauses, Data logics, SMT solvers, automata, combining decision procedures, games, monadic second-order logic

@booklet{EasyChair:8615,
  author    = {Marco Faella and Gennaro Parlato},
  title     = {Reasoning About Data Trees Using CHCs},
  howpublished = {EasyChair Preprint 8615},
  year      = {EasyChair, 2022}}