Timed propositional temporal logic: Difference between revisions

Revision as of 21:28, 29 March 2023

Revision as of 13:42, 13 June 2023

Line 1:

In [[model checking]], a field of [[computer science]], '''Timedtimed Propositionalpropositional Temporaltemporal Logiclogic''' ('''TPTL''') is an extension of propositional [[Linearlinear Temporaltemporal Logiclogic]] (LTL) in which variables are introduced to measure times between two events. For example, while LTL allows to state that each event ''p'' is eventually followed by an event ''q'', TPTL furthermore allows to give a time limit for ''q'' to occur.

== Syntax ==

Line 11:

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 journal |last1=Bouyer |first1=Patricia |author1-link=Patricia Bouyer-Decitre|last2=Chevalier |first2=Fabrice |last3=Markey |first3=Nicolas |title=On the Expressiveness of TPTL and MTL |journal=RoceedingsProceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Science |date=2005 |page=436 |doi=10.1007/11590156_3 |url=https://hal.archives-ouvertes.fr/hal-01194615/document}}</ref> is built as the future fragment of '''TLS''' and also contains

* the temporal modal operator '''S'''.

Note that the next operator '''N''' is not considered to be a part of 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>

== Model ==