First-order logic with reachability for infinite-state systems
Emanuele D’Osualdo, Roland Meyer, Georg Zetzsche · 2016
First-order logic with the reachability predicate (FO[R]) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable).