En logique, la logique temporelle linéaire (LTL) est une logique temporelle modale avec des modalités se référant au temps. En LTL, on peut coder des formules sur l'avenir d'un chemin infini dans un système de transitions, par exemple une condition finira par être vraie, une condition sera vraie jusqu'à ce qu'une autre devienne vraie, etc. Cette logique est plus faible que la logique CTL*, qui permet d'exprimer des conditions sur des ramifications de chemins et pas seulement sur un seul chemin. LTL est aussi parfois appelée logique temporelle propositionnelle, abrégé LTP (PTL en anglais). La logique temporelle linéraire (LTL) est un fragment de S1S (pour second-order with 1 successor), la logique monadique du second ordre avec un successeur.

Property Value
dbo:abstract
  • En logique, la logique temporelle linéaire (LTL) est une logique temporelle modale avec des modalités se référant au temps. En LTL, on peut coder des formules sur l'avenir d'un chemin infini dans un système de transitions, par exemple une condition finira par être vraie, une condition sera vraie jusqu'à ce qu'une autre devienne vraie, etc. Cette logique est plus faible que la logique CTL*, qui permet d'exprimer des conditions sur des ramifications de chemins et pas seulement sur un seul chemin. LTL est aussi parfois appelée logique temporelle propositionnelle, abrégé LTP (PTL en anglais). La logique temporelle linéraire (LTL) est un fragment de S1S (pour second-order with 1 successor), la logique monadique du second ordre avec un successeur. LTL a d'abord été proposé pour la vérification formelle des programmes informatiques par Amir Pnueli en 1977. (fr)
  • En logique, la logique temporelle linéaire (LTL) est une logique temporelle modale avec des modalités se référant au temps. En LTL, on peut coder des formules sur l'avenir d'un chemin infini dans un système de transitions, par exemple une condition finira par être vraie, une condition sera vraie jusqu'à ce qu'une autre devienne vraie, etc. Cette logique est plus faible que la logique CTL*, qui permet d'exprimer des conditions sur des ramifications de chemins et pas seulement sur un seul chemin. LTL est aussi parfois appelée logique temporelle propositionnelle, abrégé LTP (PTL en anglais). La logique temporelle linéraire (LTL) est un fragment de S1S (pour second-order with 1 successor), la logique monadique du second ordre avec un successeur. LTL a d'abord été proposé pour la vérification formelle des programmes informatiques par Amir Pnueli en 1977. (fr)
dbo:thumbnail
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 10354678 (xsd:integer)
dbo:wikiPageLength
  • 14708 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 187294627 (xsd:integer)
dbo:wikiPageWikiLink
prop-fr:art
  • Linear temporal logic (fr)
  • Linear temporal logic (fr)
prop-fr:id
  • 740762378 (xsd:integer)
prop-fr:lang
  • en (fr)
  • en (fr)
prop-fr:wikiPageUsesTemplate
dct:subject
rdfs:comment
  • En logique, la logique temporelle linéaire (LTL) est une logique temporelle modale avec des modalités se référant au temps. En LTL, on peut coder des formules sur l'avenir d'un chemin infini dans un système de transitions, par exemple une condition finira par être vraie, une condition sera vraie jusqu'à ce qu'une autre devienne vraie, etc. Cette logique est plus faible que la logique CTL*, qui permet d'exprimer des conditions sur des ramifications de chemins et pas seulement sur un seul chemin. LTL est aussi parfois appelée logique temporelle propositionnelle, abrégé LTP (PTL en anglais). La logique temporelle linéraire (LTL) est un fragment de S1S (pour second-order with 1 successor), la logique monadique du second ordre avec un successeur. (fr)
  • En logique, la logique temporelle linéaire (LTL) est une logique temporelle modale avec des modalités se référant au temps. En LTL, on peut coder des formules sur l'avenir d'un chemin infini dans un système de transitions, par exemple une condition finira par être vraie, une condition sera vraie jusqu'à ce qu'une autre devienne vraie, etc. Cette logique est plus faible que la logique CTL*, qui permet d'exprimer des conditions sur des ramifications de chemins et pas seulement sur un seul chemin. LTL est aussi parfois appelée logique temporelle propositionnelle, abrégé LTP (PTL en anglais). La logique temporelle linéraire (LTL) est un fragment de S1S (pour second-order with 1 successor), la logique monadique du second ordre avec un successeur. (fr)
rdfs:label
  • Logica temporale lineare (it)
  • Logique temporelle linéaire (fr)
  • 線形時相論理 (ja)
  • Logica temporale lineare (it)
  • Logique temporelle linéaire (fr)
  • 線形時相論理 (ja)
rdfs:seeAlso
owl:sameAs
prov:wasDerivedFrom
foaf:depiction
foaf:isPrimaryTopicOf
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is oa:hasTarget of
is foaf:primaryTopic of