Model checking LTL with regular valuations for pushdown systems
scientific article; zbMATH DE number 2118422