Making Metric Temporal Logic Rational

Abstract: We study an extension of

m t l

in pointwise time with rational expression guarded modality

e g_{I} (e)

where

e

is a rational expression over subformulae. We study the decidability and expressiveness of this extension (

m t l

+

v a r p h i u r e g_{I, e} v a r p h i

+

e g_{I, e} v a r p h i

), called

e g m t l

, as well as its fragment

s f m t l

where only star-free rational expressions are allowed. Using the technique of temporal projections, we show that

e g m t l

has decidable satisfiability by giving an equisatisfiable reduction to

m t l

. We also identify a subclass

m i t l + u r e g

of

e g m t l

for which our equi-satisfiable reduction gives rise to formulae of

m i t l

, yielding elementary decidability. As our second main result, we show a tight automaton-logic connection between

s f m t l

and partially ordered (or very weak) 1-clock alternating timed automata.

Recommendations

Cites Work

Cited In (12)

This page was built for publication: Making Metric Temporal Logic Rational