Non-elementary speed up for model checking synchronous perfect recall
File(s)
Published version
Author(s)
Cohen, Mika
Lomuscio, Alessio
Type
Report
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.
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.
Date Issued
2010-01-01
Citation
Departmental Technical Report: 10/9, 2010, pp.1-6
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
6
Journal / Book Title
Departmental Technical Report: 10/9
Copyright Statement
© 2010 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
10/9