Non-elementary speed up for model checking synchronous perfect recall

Abstract

We analyse the time complexity of the model checking problem for a logic of knowledge and past time in synchronous systems with perfect recall. Previously established bounds are k- exponential in the size of the system for specifications with k nested knowledge modalities.We show that the upper bound for positive (respectively, negative) specifications is polynomial (respectively, exponential) in the size of the system irrespective of the nesting depth.