CSC410 Flagship Course Project — An Axiomatic Theorem Prover for LTL

This is a project for a group of up to 3 students.

Overview

Linear temporal logic (LTL) admits an axiomatization. This paper provides one such axiomatization. But there are others. Your task in this project is to use such an axiomatization and build a small theorem prover that can prove goals in LTL based on such an axiomatization.

The emphasis is on proofs, not verdicts. Your tool does not merely answer “is this valid?” — It is meant to provide a third-party verifiable proof of the verdict to support it. In the world of standards such as “Claude is AI and can make mistakes. Please double-check responses.”, we want to provide the alternative “LTL Prover does not make any mistakes and we can prove it!”.

Why proofs, when LTL validity is already decidable?

LTL validity is decidable in PSPACE by automata-theoretic methods. So what is the point of this prover?

First and foremost, the learning value: this project touches on 3 out of 4 topics covered in this course and brings them together to deliver a useful artifact.

Second, a verdict issued by a an algorithmic (automata-theoretic) tool requires you to trust the tool that produces it. Tools are buggy as a matter of fact. In this tool, you give the verdict and enough information for it to be checkable by someone/something else. A derivation can be manually checked or audited by a simple/small program that itself can be independently verified. The search-based methodology, on the other hand, involves thousands of lines of untrusted heuristics, which are much harder to verify.

Background: The Axiom System

The axiom system below is a variant of the one proved complete by Gabbay, Pnueli, Shelah and Stavi (1980), in the presentation given by Wolper, Temporal Logic Can Be More Expressive, §3. The system is as follows, where metavariables like p, q, and w range over all LTL formulas, and ⊢ p is the only judgment form. A1–8 are axiom schemas, and R1–3 are inference rules.

A1   ⊢ ◇p ≡ ¬□¬p                     R1   if w is a propositional tautology, then ⊢ w
A2   ⊢ □(p ⊃ q) ⊃ (□p ⊃ □q)          R2   if ⊢ w₁ ⊃ w₂ and ⊢ w₁, then ⊢ w₂
A3   ⊢ ○¬p ≡ ¬○p                     R3   if ⊢ w, then ⊢ □w
A4   ⊢ ○(p ⊃ q) ⊃ (○p ⊃ ○q)
A5   ⊢ □p ⊃ p ∧ ○p ∧ ○□p
A6   ⊢ □(p ⊃ ○p) ⊃ (p ⊃ □p)
A7   ⊢ □p ⊃ p U q
A8   ⊢ p U q ≡ q ∨ (p ∧ ○(p U q))

with the optional replacements for the two U axioms:

A9   ⊢ p U q ⊃ q ∨ (p ∧ ○(p U q))
A10  ⊢ [u ∧ □(u ⊃ q ∨ (p ∧ ○u))] ⊃ p U q

Study these axioms carefully. Some, like A1, can be combined with R1 and R2 and applied mechanically; one matches the pattern and replaces it with the other side (see Example 1 below). Now consider A6: it involves a formula p that holds now, is preserved by a one step, and then we get the implicaiton that it always holds. This is very much like the discovery of a loop invariant. Hence, now you would expec that its application effectively requires the discovery of a loop invariant, and its automation to be subject to similar difficulties.

Another thing to highlight is that R1 is the sole rule in charge of doing propositional reasoning.

What a derivation looks like

Here is an example derivation; each line is a formula, a justification, and a line number.

Example 1 — validity of □(p ⊃ q) ⊃ (◇p ⊃ ◇q):

⊢ (p ⊃ q) ⊃ (¬q ⊃ ¬p)                     (R1)                  (1)
⊢ □((p ⊃ q) ⊃ (¬q ⊃ ¬p))                  (1, R3)               (2)
⊢ □(p ⊃ q) ⊃ □(¬q ⊃ ¬p)                   (2, A2)               (3)
⊢ □(¬q ⊃ ¬p) ⊃ (□¬q ⊃ □¬p)                (3, A2)               (4)
⊢ (□¬q ⊃ □¬p) ≡ (¬◇q ⊃ ¬◇p)               (A1, R1, R2)          (5)
⊢ (¬◇q ⊃ ¬◇p) ≡ (◇p ⊃ ◇q)                 (R1)                  (6)
⊢ □(¬q ⊃ ¬p) ⊃ (◇p ⊃ ◇q)                  (3, 4, 5, 6, R1, R2)  (7)

In (5), we use the propositional tautology

(◇p ≡ ¬□¬p) ⊃ (◇q ≡ ¬□¬q) ⊃ ((□¬q ⊃ □¬p) ≡ (¬◇q ⊃ ¬◇p))

and apply R2 twice. The net effect is to pattern match against A1 and replace one side with the other.

Example 2 — the equivalence □(p ∧ q) ≡ □p ∧ □q:

⊢ (p ∧ q) ⊃ p                                   (R1)                 (1)
⊢ □((p ∧ q) ⊃ p)                                (1, R3)              (2)
⊢ □((p ∧ q) ⊃ p) ⊃ (□(p ∧ q) ⊃ □p)              (A2)                 (3)
⊢ □(p ∧ q) ⊃ □p                                 (2, 3, R2)           (4)
⊢ (p ∧ q) ⊃ q                                   (R1)                 (5)
⊢ □((p ∧ q) ⊃ q)                                (5, R3)              (6)
⊢ □((p ∧ q) ⊃ q) ⊃ (□(p ∧ q) ⊃ □q)              (A2)                 (7)
⊢ □(p ∧ q) ⊃ □q                                 (6, 7, R2)           (8)
⊢ □(p ∧ q) ⊃ (□p ∧ □q)                          (4, 8, R1, R2)       (9)

⊢ p ⊃ (q ⊃ (p ∧ q))                             (R1)                 (10)
⊢ □(p ⊃ (q ⊃ (p ∧ q)))                          (10, R3)             (11)
⊢ □(p ⊃ (q ⊃ (p ∧ q))) ⊃ (□p ⊃ □(q ⊃ (p ∧ q)))  (A2)                 (12)
⊢ □p ⊃ □(q ⊃ (p ∧ q))                            (11, 12, R2)        (13)
⊢ □(q ⊃ (p ∧ q)) ⊃ (□q ⊃ □(p ∧ q))              (A2)                 (14)
⊢ □p ⊃ (□q ⊃ □(p ∧ q))                          (13, 14, R1, R2)     (15)
⊢ (□p ∧ □q) ⊃ □(p ∧ q)                          (15, R1, R2)         (16)

⊢ □(p ∧ q) ≡ (□p ∧ □q)                          (9, 16, R1, R2)      (17)

Note that showing the validity of the formula □(p ∧ q) ≡ (□p ∧ □q) is identical to proving the (now familiar to you) LTL equivalence in Example 2.

This derivation would look much better as a tree, but then the tree cannot be easily drawn in Markdown.

⚠️ Read the notes on the U operator before you write any code. The U in this axiom system is not the one from lecture, and getting this wrong will cost you a milestone.

Components

The project is meant to have five main components:

Component 0 — Soundness of The Proof System

Whichever proof system you use, the first step is for you to show the axioms and inference rules are sound wrt the semantic definitions of the participating temporal operators and standard propositional logic. Verify this formally in a prover of your choice (e.g., Dafny / Velvet / Lean).

You should start by formalizing the syntax and semantics of LTL formulas, the axioms/rules, and the statement of the soundness theorem.

You may implement Component 1–4 in any programming language of your choice. In the report, you will make a connection between your formal proofs and the implementation (see the notes).

Component 1 — The Verified Checker

Input: a formula and a candidate derivation. Output: accept or reject.

A derivation is a list of lines, each a formula together with a justification: an axiom schema plus an instantiation, or an inference rule plus the indices of the earlier lines it uses. The example derivations provided above compress steps like R1 and R2 into a single line for readability, and you should not do that.

The checker walks the list and confirms each line is justified by its stated rule, and that the last line is the goal.

Graduate Students: Additionally, verify this component in a prover of your choice (e.g., Dafny / Velvet / Lean). Note that your delivery here is only as good as your specification. You should define derivability (the ⊢ judgment) as a least fixed point (Dafny) or inductive predicate (Lean/Velvet), where each axiom schema and inference rule corresponds to a disjunct/constructor. Then, prove a theorem that relates your proof checker and this definition. If you choose to implement Component 1–4 in another language, say Python, you will need to model your Python implementation in the prover language and supply a specification for the propositional backend (see Component 2). See the notes.

Component 2 — The Propositional Backend

Rule R1 admits any propositional tautology. Checking if this step has been applied correctly needs generic propositional reasoning. You learn about propositional reasoning in this course. Use what you learn. Make sure to cleanly document the theoretical aspect of your solution of how/what you delegate to an external tool. The design and choices are entirely yours.

Component 3 — Derivation Synthesis

Given a provable goal, produce a derivation that proves it.

If you study the axioms and rules, you will observe that some are basically recipes for nontermination. In other words, blind proof search over a complete axiomatization does not terminate in general. Any algorithmic solution must make a principled compromise between completeness and convergence. Your task for this component is then to define a subproblem you can solve, solve it well, and be articulate about the boundary.

Things you will have to specifically target in your implementation and your report, and properly justify:

• Which fragment of LTL you target, and why.
• How you handle rules like A6, where the search must invent something rather than match a pattern.
• Your termination argument.

A prover that handles a small fragment well, with a clear account of why, will score better than one that handles more by accident and cannot explain itself.

Note that the example derivations provided in this document are meant as illustrations, and not test cases. It is not necessarily the case that these two derivations must be producable by your system.

Guideline: The □ / ◇ / ○ fragment is the required core. Any (partial) treatment of U is a next level goal. A complete, well-evaluated prover for the small fragment is a good submission.

Component 4 — Evaluation & Project Report

Assemble a benchmark of LTL formulas — valid and invalid, easy and hard — and report the performance of your tool.

Your report must include:

• The size and composition of the benchmark set, and your selection criteria.
• A table reporting results on benchmarks with all relevant performance measures.
• The smallest valid formula in your benchmarks that your tool fails on, with an analysis of why — is it a search limitation, a fragment restriction, or a limitation of the axiomatization itself?

Honest negative results are worth more than inflated benchmark set to falsely demonstrate coverage.

Graduate Students: You are expected to do more than the above. You are expected to identify ways of emperically or theoretically arguing for the quality of your solutions. This may be through the systematic/purposeful selection of your benchmark set, or other orthogonal arguments. Note that the evaluation criteria is independent of how well/badly your solution does. It is about properly evaluating a solution as is expected of you for any work you produce in your own line of work. So, you may do badly in Component 3, but an honest evaluation in Component 4 can nevertheless get the full mark for this part.

Notes

The U in this axiom system is weak until

A7 states □p ⊃ p U q. Under the strong until taught in lecture, this is invalid. The paper defines “until with eventuality” separately as p UE q ≡ p U q ∧ ◇q; that conjunct would be redundant if U were already strong.

You may choose to use a different axiomatization. But, if you are using this one, be mindful of this fact.

Identify gaps in verification

Any place where you translate between representations by hand — LTL in Dafny code into a Python dataclass, etc. — is a place no tool is checking you. Flag every such boundary in your report and argue informally that your translation is faithful.

Deliverables

• Source, with a README explaining how to build and run.
• Your verified checker (Dafny and/or Lean sources), with the verification passing.
• An examples/ directory with at least 10 benchmarks.
• A script that runs the benchmark and reproduces the evaluation results.
• A report (≤ 4 pages) that outlines all the technically interesting choices of your tool, including all points mentioned above in this document.

In-Person Delivery & Defense

We will aim for a short in-person delivery of the project by each group duing the last week of classes. We will not fully evaluate your project live on the spot. That will be done offline later. We will ask the group high level questions about various different design choices made for the project and techncial details. All group members must appear in-person for this short (~10 minutes) delivery. Details about this and the specific schedule will be released later in the term. The dates are December 1,2 which are the last scheduled classes for the two sections, and Dec 4 (as a backup) which is the last joint tutorial slot for the course. So, all the times are during valid class hours when you are expected to be available.

Grading

Weights for grading the project:

Bonus marks are available for a prover that stands out in quality in the class. These bonus marks will apply to the course level if the project already receives full mark. So, 1-2 groups that really distinguish themseleves in executing the project have a chance to score more marks from it for their course.

Grad Students

If you have an alternative exciting project in mind that relates to your specific field of study and has a significant and meaningful verification component, you can propose to do the alternative project in place of this default course project. To do this, you need to submit a proposal by October 2nd and we will do our best to give you the verdict within a week. This proposal needs to be detailed and specific in spelling out the components of the projects (similar to this document) and have parallels (within reason) to them. This would basically allow us to evaluate if your proposed project is (1) at least the same amount of work as this project, and (2) has enough verification components to justify the work standing in for part of this course’s grade.

To the rare undergraduate enthusiast who reads this and asks “Why do I not get the same choice?”, talk to your instructor after one of the lectures if you are really keen to have this choice and we will see if we can work something out.

Group Formations

Groups can be formed in any way you wish, from different sections. It is even OK if a group is to be formed as a mix of graduate and undergraduate students, but the moment you have a graduate student in your group, your project will have to be graded on the graduate student scale; that is, the extra components will become a requirement.