Timed propositional temporal logic: Difference between revisions

Content deleted Content added
TPTL believe to be strictly more expressive than MTL
Correction of a wrong negation
Line 42:
It follows that any other operator introduced in the page [[metric temporal logic#Operators defined from MTL operator|MTL]], such as <math>\Box</math> and <math>\Diamond</math> can also be defined as TPTL formulas.
 
It is believed that TPTL is strictly more expressive than MTL{{r|ExpressivenesOfTPTLAndMtl|p=2}} both over timed words and over signals. NoOver timed words, no MTL formula is equivalent to <math>\Box(pa\implies x.\Diamond(qb\land\Diamond(rc\land x\le 5)))</math>. isOver knownsignal, there are no MTL formula equivalent to <math>x.\Diamond(a\land Howeverx\le 1\land\Box(x\le 1\implies\neg b))</math>, itwhich hasstates notthat beenthe provenlast eitheratomic thatproposition nobefore suchtime formulapoint exists1 is an <math>a</math>.
 
== Comparison with LTL ==