Reasoning About Data Trees Using CHCs

EasyChair Preprint no. 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: automata, combining decision procedures, Constrained Horn Clauses, Data logics, games, monadic second-order logic, SMT solvers

@Booklet{EasyChair:8615,
  author = {Marco Faella and Gennaro Parlato},
  title = {Reasoning About Data Trees Using CHCs},
  howpublished = {EasyChair Preprint no. 8615},

  year = {EasyChair, 2022}}