Expressive Completeness for LTL With Modulo Counting and Group Quantifiers

摘要

Kamp showed that linear temporal logic is expressively complete for first order logic over words. We give a Gabbay style proof to show that linear temporal logic extended with modulo counting and group quantifiers (introduced by Baziramwabo, McKenzie, Thérien) is expressively complete for first order logic with modulo counting (introduced by Straubing, Thérien, Thomas) and group quantifiers (introduced by Barrington, Immerman, Straubing).