Content deleted Content added
→Syntax: more clarify requests |
|||
Line 6:
* the [[logical connective|logical operators]] ¬ and ∨, and
* the [[Temporal logic|temporal]] [[modal operator]] '''U''',
* a clock comparison <math>x\sim c</math>, with <math>x\in X</math>, <math>c</math> a number and <math>\sim</math> a comparison operator such as <, ≤, =, ≥ or >.{{clarify|reason=Since the set of logical connectives is chosen minimal (without e.g. \lor), the same could be done here. If times are ordered totally, \leq would be sufficient.}}
* a freeze quantification operator <math>x.\phi</math>, for <math>\phi</math> a TPTL formula with set of clocks <math>X\cup\{x\}</math>.
Furthermore, for <math>I=(a,b)</math> an interval, <math>x\in I</math> is considered as an abbreviation for <math>x>a\land x<b</math>; and similarly for every other kind of intervals.
The logic '''TPTL+Past'''<ref name="ExpressivenesOfTPTLAndMtl">{{cite book |last1=Bouyer |first1=Patricia |author1-link=Patricia Bouyer-Decitre|last2=Chevalier |first2=Fabrice |last3=Markey |first3=Nicolas |title=FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science |chapter=Developments in Data Structure Research During the First 25 Years of FSTTCS |series=Lecture Notes in Computer Science |journal=Proceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Science |date=2005 |volume=3821 |page=436 |doi=10.1007/11590156_3 |isbn=978-3-540-30495-1 |chapter-url=https://hal.archives-ouvertes.fr/hal-01194615/document}}</ref> is built as the future fragment of {{clarify span|'''TLS'''|reason=Should be introduced or linked.}} and also contains
* the temporal modal operator '''S'''.
A '''closed formula''' is a formula over an empty set of clocks.<ref name="Really">{{cite journal |last1=Alur |first1=Rajeev |author1link = Rajeev Alur|last2=Henzinger |first2=Thomas A. |author2link = Thomas Henzinger|title=A really temporal logic|journal=[[Journal of the ACM]]|date=Jan 1994 |volume=41 |issue =1|pages=181–203 |doi=10.1145/174644.174651|doi-access=free }}</ref>{{clarify|reason=The set of clocks of a formula needs to be introduced (I guess along with the syntax case distinction above).}}
== Models ==
|