Some Recent Results in Metric Temporal Logic
Metric Temporal Logic (MTL) is a widely-studied real-time extension of Linear Temporal Logic. In this paper we survey results about the complexity of the satisfiability and model checking problems for fragments of MTL with respect to different semantic models. We show that these fragments have widel...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2008
|
| _version_ | 1797088983215243264 |
|---|---|
| author | Ouaknine, J Worrell, J |
| author_facet | Ouaknine, J Worrell, J |
| author_sort | Ouaknine, J |
| collection | OXFORD |
| description | Metric Temporal Logic (MTL) is a widely-studied real-time extension of Linear Temporal Logic. In this paper we survey results about the complexity of the satisfiability and model checking problems for fragments of MTL with respect to different semantic models. We show that these fragments have widely differing complexities: from polynomial space to non-primitive recursive and even undecidable. However we show that the most commonly occurring real-time properties, such as invariance and bounded response, can be expressed in fragments of MTL for which model checking, if not satisfiability, can be decided in polynomial or exponential space. © 2008 Springer-Verlag Berlin Heidelberg. |
| first_indexed | 2024-03-07T02:57:56Z |
| format | Journal article |
| id | oxford-uuid:aff56da2-4ece-424d-9da0-c964c9ebc5f5 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T02:57:56Z |
| publishDate | 2008 |
| record_format | dspace |
| spelling | oxford-uuid:aff56da2-4ece-424d-9da0-c964c9ebc5f52022-03-27T03:52:58ZSome Recent Results in Metric Temporal LogicJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:aff56da2-4ece-424d-9da0-c964c9ebc5f5EnglishSymplectic Elements at Oxford2008Ouaknine, JWorrell, JMetric Temporal Logic (MTL) is a widely-studied real-time extension of Linear Temporal Logic. In this paper we survey results about the complexity of the satisfiability and model checking problems for fragments of MTL with respect to different semantic models. We show that these fragments have widely differing complexities: from polynomial space to non-primitive recursive and even undecidable. However we show that the most commonly occurring real-time properties, such as invariance and bounded response, can be expressed in fragments of MTL for which model checking, if not satisfiability, can be decided in polynomial or exponential space. © 2008 Springer-Verlag Berlin Heidelberg. |
| spellingShingle | Ouaknine, J Worrell, J Some Recent Results in Metric Temporal Logic |
| title | Some Recent Results in Metric Temporal Logic |
| title_full | Some Recent Results in Metric Temporal Logic |
| title_fullStr | Some Recent Results in Metric Temporal Logic |
| title_full_unstemmed | Some Recent Results in Metric Temporal Logic |
| title_short | Some Recent Results in Metric Temporal Logic |
| title_sort | some recent results in metric temporal logic |
| work_keys_str_mv | AT ouakninej somerecentresultsinmetrictemporallogic AT worrellj somerecentresultsinmetrictemporallogic |