Content deleted Content added
Citation bot (talk | contribs) Alter: title, template type. Add: chapter-url, isbn, volume, series, chapter. Removed or converted URL. | Use this bot. Report bugs. | Suggested by Abductive | Category:Model checking | #UCB_Category 4/24 |
|||
Line 2:
== Syntax ==
The '''future fragment of TPTL''' is defined similarly to [[linear temporal logic]], in which furthermore, [[clock (model checking)|clock]] variables can be introduced and compared to constants. Formally, given a set <math>X</math> of clocks, {{clarify span|MTL|reason=Should be 'TPTL'? MTL is discussed in a later section.}} is built up from:
* a finite set of [[propositional variable]]s ''AP'',
* the [[logical connective|logical operators]] ¬ and ∨, and
Line 14:
* the temporal modal operator '''S'''.
Note that the next operator '''N''' is not considered to be a part of {{clarify span|MTL}} syntax. It will instead be defined from other operators.
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>
| |||