Algorithmic metatheorems for decidable LTL model checking over infinite systems

Anthony Widjaja To, Leonid Libkin

By algorithmic metatheorems for a model checking problem P over infinite-state systems we mean generic results that can be used to infer decidability (possibly complexity) of P not…