Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / From real-time logic to timed automata

Name: Rising edge of \(p\)
Definition: \(p\land\neg\ominus p\) over timed words
Page: 2, 46
Chapter: (3 C HECKING T IMED AND H YBRID
P ROPERTIES :
T HEORY AND A PPLICATIONS)
Section: (2.1)
Variables: \(p\) a MITL-formula
Notation: \(\uparrow p\)
Definition2: \((p\land(\neg p\mathcal S\top))\lor(\neg p\land(p\mathcal U\top))\)