Temporal logic of actions (TLA) is a logic developed by
Leslie Lamport
Leslie B. Lamport (born February 7, 1941 in Brooklyn) is an American computer scientist and mathematician. Lamport is best known for his seminal work in distributed systems, and as the initial developer of the document preparation system LaTeX an ...
, which combines
temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
with a
logic of actions.
It is used to describe behaviours of
concurrent
Concurrent means happening at the same time. Concurrency, concurrent, or concurrence may refer to:
Law
* Concurrence, in jurisprudence, the need to prove both ''actus reus'' and ''mens rea''
* Concurring opinion (also called a "concurrence"), a ...
and
distributed systems
A distributed system is a system whose components are located on different networked computers, which communicate and coordinate their actions by passing messages to one another from any system. Distributed computing is a field of computer sci ...
. It is the logic underlying the specification language
TLA+
TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-t ...
.
Details
Statements in the temporal logic of actions are of the form
, where ''A'' is an action and ''t'' contains a subset of the variables appearing in ''A''. An action is an expression containing primed and non-primed variables, such as
. The meaning of the non-primed variables is ''the variable's value in this state''. The meaning of primed variables is ''the variable's value in the next state''.
The above expression means the value of ''x'' ''today'', plus the value of ''x'' ''tomorrow'' times the value of ''y'' ''today'', equals the value of ''y'' ''tomorrow''.
The meaning of
is that either ''A'' is valid now, or the variables appearing in ''t'' do not change. This allows for stuttering steps, in which none of the program variables change their values.
See also
*
Dynamic logic (modal logic)
In logic, philosophy, and theoretical computer science, dynamic logic is an extension of modal logic capable of encoding properties of computer programs.
A simple example of a statement in dynamic logic is
:\text \to text\text,
which states that ...
*
Temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
*
PlusCal
PlusCal (formerly called +CAL) is a formal specification language created by Leslie Lamport, which transpiles to TLA+. In contrast to TLA+'s action-oriented focus on distributed systems, PlusCal most resembles an imperative programming language ...
*
TLA+
TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-t ...
References
*
*
External links
*
*
*
Temporal logic
Concurrency (computer science)
{{formalmethods-stub