Timed propositional temporal logic: Difference between revisions

Revision as of 19:24, 6 February 2025

Revision as of 19:26, 6 February 2025

Line 33:

* <math>\gamma,t,\nu\models\phi\mathbin\mathcal S\psi</math> holds if there exists <math>t''</math> such that <math>t''< t</math> and <math>\gamma,t'',\nu\models\psi</math> and for each <math>t'</math> with <math>t''<t'<t</math>, &nbsp; <math>\gamma,t',\nu\models\phi</math>,

* <math>\gamma,t,\nu\models x\sim c</math> holds if <math>t-\nu(y)\sim c</math>,{{clarify|reason='y' should be 'x'?}}

* <math>\gamma,t,\nu\models y.\xi</math> holds if <math>\gamma,t,\nu[y\to t]\models\phi</math> holds.{{clarify|reason='\phi' should be '\xi'?}}

== Metric temporal logic ==