Some Recent Results in Metric Temporal Logics

【文件属性】：
文件名称：Some Recent Results in Metric Temporal Logics
文件大小：499KB
文件格式：PDF
更新时间：2015-03-14 13:50:33
Metric Temporal Logics MTL JoÅNel Ouaknine and James Worrell Abstract. 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.