Non-elementary speed up for model checking synchronous perfect recall

We consider the complexity of the model checking problem for the 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.

Authors

• Mika Cohen
• Alessio Lomuscio

Keywords

No keywords are indexed for this paper.