Content deleted Content added
Stevey7788 (talk | contribs) mNo edit summary |
Stevey7788 (talk | contribs) mNo edit summary |
||
Line 17:
A '''closed formula''' is a formula over an empty set of clocks.<ref name="Really">{{cite journal |last1=Alur |first1=Rajeev |last2=Henzinger |first2=Thomas A. |title=A really temporal logic|journal=Journal of the ACM (JACM|date=Jan 1994 |volume=41 |issue =1|page=181-203 |doi=10.1145/174644.174651}}</ref>.
== Model ==▼
▲== Model ==
Let <math>T\subseteq\mathbb R_+</math> it intuitively represents a set of time. Let <math>\gamma: T\to \mathcal P(AP)</math> a function which associate to each moment <math>t\in T</math> a set of propositions from ''AP''. A model of a TPTL formula is such a function <math>\gamma</math>. Usually, <math>\gamma</math> is either a [[timed word]] or a [[signal (model checking)|signal]]. In those cases, <math>T</math> is either a discrete subset or an interval containing 0.
== Semantic ==
Let <math>T</math> and <math>\gamma</math> as above. Let <math>X</math> a set of [[clock (model checking)|clocks]]. Let <math>\nu:X\to\mathbb R_{\ge0}</math> a clock valuation over <math>X</math>.
Line 35 ⟶ 34:
* <math>\gamma,t,\nu\models y.\xi</math> holds if <math>\gamma,t,\nu[y\to t]\models\phi</math> holds,
* <math>\gamma,t,\nu\models x\sim c</math> holds if <math>t-\nu(y)\sim c</math>.
== From Metric Temporal Logic to TPTL ==
| |||