Reasoning About Data Trees Using CHCs

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 system of CHCs (Constrained Horn Clauses), and solving the resulting system using off-the-shelf solvers. We also 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, solving certain infinite-state 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 different problem domains.