TLA

E467807

TLA is a formal specification language developed by Leslie Lamport for describing and reasoning about concurrent and distributed systems using temporal logic.

All labels observed (1)

Label Occurrences
TLA canonical 1

How this entity was disambiguated

Statements (46)

Predicate Object
instanceOf formal specification language ⓘ
temporal logic ⓘ
approach action-based specification ⓘ
state-based specification ⓘ
basedOn temporal logic ⓘ
contrastsWith operational specification languages ⓘ
process algebras ⓘ
creatorAffiliation Microsoft Research ⓘ
developer Leslie Lamport ⓘ
emphasizes mathematical rigor ⓘ
precise semantics ⓘ
field computer science ⓘ
concurrent systems ⓘ
distributed systems ⓘ
formal methods ⓘ
fullName Temporal Logic of Actions ⓘ
hasExtension TLA+ ⓘ
hasKeyConcept actions as state transitions ⓘ
behaviors as sequences of states ⓘ
specifications as formulas in temporal logic ⓘ
hasNotation mathematical notation ⓘ
influenced TLA+ ⓘ
influencedBy predicate logic ⓘ
set theory ⓘ
temporal logic ⓘ
logicalFoundation linear-time temporal logic ⓘ
purpose modeling algorithms ⓘ
reasoning about system correctness ⓘ
specifying concurrent systems ⓘ
specifying distributed systems ⓘ
relatedTo TLA+ ⓘ
relatedTool TLA+ model checker TLC ⓘ
supports compositional reasoning ⓘ
refinement reasoning ⓘ
stepwise development ⓘ
usedFor designing fault-tolerant systems ⓘ
specifying protocols ⓘ
verifying concurrent algorithms ⓘ
verifying distributed algorithms ⓘ
usesConcept actions ⓘ
behaviors ⓘ
invariants ⓘ
liveness properties ⓘ
safety properties ⓘ
states ⓘ
temporal operators ⓘ

How these facts were elicited

Referenced by (1)

Full triples — surface form annotated when it differs from this entity's canonical label.