Skip to content

Tree Automizer

Jump to bottom
alexandernutz edited this page May 11, 2016 · 8 revisions

= Components =

  • Convert Horn clauses (in some text format) to a graph stucture (let's call it HornClauseGraph, HCG)
  • Convert the Horn Clause Graph to a Tree Automaton, analogous to the "Program Automaton" in Automizer\
  • Adapt the CegarLoop from Automizer for working on Tree Automata
  • Construct a Tree Automaton from a Horn clause ground derivation, analogous to the "Interpolant Automaton" or "Data Automaton"
Clone this wiki locally