Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic

Normann Decker, Anton Pirogov

This paper presents an approximation approach to verifying counter systems with respect to properties formulated in an expressive counting extension of linear temporal logic. It ca…