Timed propositional temporal logic: Difference between revisions

Revision as of 19:15, 6 February 2025

Revision as of 19:24, 6 February 2025

Line 30:

* <math>\gamma,t,\nu\models\neg\phi</math> holds if <math>\gamma,t,\nu\not\models\phi</math>

* <math>\gamma,t,\nu\models\phi\lor\psi</math> holds if either <math>\gamma,t,\nu\models\phi</math> or <math>\gamma,t,\nu\models\psi</math>, or both

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

* <math>\gamma,t,\nu\models\phi\mathbin\mathcal S\psi</math> holds if there exists <math>t''< t</math> such that <math>t''< t</math> and <math>\gamma,t'',\nu\models\psi</math> and such that 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.