Both LTL and CTL are fragments of propositional logic and parts of CTL*.
Linear Temporal Logic (LTL)
LTL is a modal temporal logic with modalities referring to time [1]. In the context of smart contracts, LTL can be used to specify and verify properties that must hold over the sequences of states that a contract might pass through.
For example, it allows developers to make assertions like, “If condition $X$ is $true$, then condition $Y$ will eventually be $true$” (expressed as $X \implies \lozenge Y$ in LTL). This is particularly useful for smart contracts, which may need to guarantee certain outcomes after a sequence of events.
Imagine a smart contract that has a critical function to ensure that once a user deposits a certain amount of assets, they will eventually receive interest payments. With LTL, we could formally verify this property by expressing it as:
$$ G(\text{deposit} \implies F\text{ interest payment}) $$
This LTL formula states that it is globally $true$ ($G$) that if a deposit action occurs, it will be followed eventually ($F$) by an interest payment. This kind of temporal logic allows developers and security analysts to prove that the smart contract will behave as intended over time.
LTL uses temporal operators to express logical statements about the future, such as:
- $G$ (Globally): A condition must hold in all future states.
- $F$ (Finally): A condition will eventually hold in some future state.
- $X$ (neXt): A condition will hold in the next state.
- $U$ (Until): A condition will hold until another condition holds.
Computation Tree Logic (CTL)
While LTL is linear and considers the flow of time as a single path, CTL allows for branching time, where multiple future possibilities can be considered from any given point [2]. CTL introduces path quantifiers to specify properties of computation trees — structures representing all possible executions of a system from any given state.
The two path quantifiers are:
- $A$ (for All paths): Specifies that a property must hold on all possible future paths.
- $E$ (there Exists a path): Specifies that there is at least one possible future path where a property holds.
CTL uses the same temporal operators as LTL, but prefixed with path quantifiers. So, you might see formulas like $AG$ (on all paths, globally) or $EF$ (there exists a path where finally).
For instance, a smart contract might have a function that only allows funds to be withdrawn by a specific party after a certain date. CTL can be used to validate this by expressing properties like “For all paths, if the withdrawal function is called, then for every possible continuation of that path, either the caller is the authorized party, and the date is correct, or the withdrawal fails.”
In CTL, this could be expressed as:
$$ A[\text{withdraw} \implies (E[\text{caller} = \text{authorized} \land \text{date} \geq \text{specified}] \lor E[\text{transaction reverted}])] $$
This states that along all paths ($A$), if a withdrawal attempt occurs, there exists a path ($E$) where either the caller is authorized and the date is on or after the specified date, or there exists a path where the transaction is reverted, ensuring funds can’t be incorrectly withdrawn.
Keeping in mind: LTL synthesis and the problem of verification of games against an LTL winning condition is 2EXPTIME-complete [3].
We think these logics can be used to verify; hence, cover high-level logical scenarios for smart-contract as within a single transaction as in a sequence of blocks.
Of course, for such digital systems as smart contracts, design and modelling based on temporal logic should be done before the actual implementation. [The same is true of any other considered digital system]. This is a part of the Verification-Driven Development process [4] and to reduce the number of possible errors, it must be a predecessor of code.
References
Join this blog discussion:
