Let's Learn Their Language? A Case for Planning with Automata-Network Languages from Model Checking

  • Jorg Hoffmann Saarland University
  • Holger Hermanns Saarland University
  • Michaela Klauck Saarland University
  • Marcel Steinmetz Saarland University
  • Erez Karpas Technion Israel Institute of Technology
  • Daniele Magazzeni King's College London


It is widely known that AI planning and model checking are closely related. Compilations have been devised between various pairs of language fragments. What has barely been voiced yet, though, is the idea to let go of one's own modeling language, and use one from the other area instead. We advocate that idea here – to use automata-network languages from model checking instead of PDDL – motivated by modeling difficulties relating to planning agents surrounded by exogenous agents in complex environments. One could, of course, address this by designing additional extended planning languages. But one can also leverage decades of work on modeling in the formal methods community, creating potential for deep synergy and integration with their techniques as a side effect. We believe there's a case to be made for the latter, as one modeling alternative in planning among others.

Senior Member Presentation Track: Summary Talks