Linear Temporal Logic

Linear temporal logic is a formalism used to describe sequences of events or states over time. It is extensively utilized in computer science for specifying and verifying the behavior of systems, particularly in areas like model checking and formal verification. This tutorial will guide you through the basics of LTL and demonstrate how to implement a solver in Python.

LTL is a modal temporal logic with modalities referring to time. It allows us to encode formulae about the future of paths, such as conditions that will eventually be true or conditions that will be true until another fact becomes true. LTL is a fragment of the more complex CTL*, which additionally allows branching time and quantifiers.

LTL is built from a finite set of propositional variables, logical operators, and temporal modal operators. The basic syntax includes:

• Propositional Variables: Basic atomic propositions.
• Logical Operators: \(\neg\) (not), \(\lor\) (or), \(\land\) (and), \(\to\) (implies), \(\leftrightarrow\) (if and only if).
• Temporal Operators:
  • X (Next): Specifies that a property holds in the next state.
  • U (Until): A property holds until another property becomes true.
  • G (Globally/Always): A property holds in all future states.
  • F (Finally/Eventually): A property will hold at some point in the future.
  • R (Release): A property is true until and including the point where another property becomes true.

An LTL formula can be satisfied by an infinite sequence of truth valuations of variables. These sequences can be viewed as a word on a path of a Kripke structure. The satisfaction relation between a word and an LTL formula is defined as follows:

• X ψ: ψ must be true in the next time step.
• φ U ψ: φ must remain true until ψ becomes true.
• G ψ: ψ always remains true.
• F ψ: ψ eventually becomes true.
• ψ R φ: φ remains true until and including once ψ becomes true.

LTL is commonly used in model checking, a method for formally verifying whether a system meets a given specification. In automata-theoretic model checking, both the system and the specification are expressed as finite-state machines, and then compared to evaluate whether the system is guaranteed to have the specified property.

LTL is also used to express safety and liveness properties in formal verification. Safety properties state that something bad never happens, while liveness properties state that something good keeps happening.

We'll implement a solver that allows you to define LTL formulas and evaluate whether a given sequence of states (called a trace) satisfies the formula.

A trace is a sequence of states, where each state is a set of propositions that are true at that point in time. Here's how you can define a trace in Python:

trace = [
    {'a', 'b'},
    {'b'},
    {'a'},
    {'a', 'c'},
]

# Define an LTL formula, e.g., G a (a is always true)
formula_str = "G a"

formula = parse_formula(formula_str)
result = formula.evaluate(trace, 0)
print(f"The trace {'satisfies' if result else 'does not satisfy'} the formula '{formula_str}'")

The solver includes a parser that converts a string into an LTL formula object. Here's how you can use it:

def parse_formula(formula_str: str) -> LTLFormula:
    tokens = tokenize(formula_str)
    return parse_expression(tokens)

Once parsed, you can evaluate the formula against a trace:

result = formula.evaluate(trace, 0)

The evaluate method checks whether the formula holds starting from the specified index in the trace.

To see the solver in action, you can execute the solver.py script. Based on the example provided, it will output whether the defined trace satisfies the LTL formula.

$ python solver.py
The trace does not satisfy the formula 'G a'

In this output, the solver determines that the trace does not satisfy the formula G a because there are states where proposition a is not present.

You can define more complex LTL formulas using the available operators. For instance:

• Eventually Always: F G a asserts that at some point in the future, proposition a will always be true.
• Next an Event: X b asserts that proposition b will be true in the next state.
• Combination: G (a || b) asserts that always, either a or b is true.

Here's an example of defining and evaluating a more complex formula:

trace = [
    {'a'},
    {'b'},
    {'a', 'c'},
    {'a'},
]

formula_str = "F G a"  # Eventually, a is always true
formula = parse_formula(formula_str)
result = formula.evaluate(trace, 0)
print(f"The trace {'satisfies' if result else 'does not satisfy'} the formula '{formula_str}'")

This will output:

The trace satisfies the formula 'F G a'

indicating that at some point in the trace, proposition a remains true indefinitely.