Making Metric Temporal Logic Rational

Por • 13 jun, 2017 • Sección: Leyes

Shankara Narayanan Krishna, Khushraj Madnani, P. K. Pandya

Abstract: We study an extension of MTL in pointwise time with rational expression guarded modality RatI (re) where re is a rational expression over subformulae. We study the decidability and expressiveness of this extension called RatMTL, as well as its fragment SfrMTL where only star-free rational expressions are allowed. Using the technique of temporal projections, we show that RatMTL has decidable satisfiability by giving an equisatisfiable reduction to MTL. We also identify a subclass of RatMTL for which our equi-satisfiable reduction gives rise to formulae of MITL, yielding elementary decidability. As our second main result, we show a tight automaton-logic connection between SfrMTL and partially ordered (or very weak) 1-clock alternating timed autómata.

rXiv:1705.01501v1 [cs.LO]

Logic in Computer Science (cs.LO)

Post to Twitter

Escribe un comentario