[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] LTL axiomatic system

On 12 Aug 2016, at 12:47, 'fl' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:

Hi Frédéric,

the axiom system given in the slides that you point to is correct (sound and complete) for LTL. You can also find several variations on LTL proof systems, with different combinations of operators, in our book

Can you prove a theorem likle this one and if not why? 

 ( P <=> Q )                                ( R <=> S )  
      ( ( P until  R ) <=> ( Q until S ) ) 

Yes, of course you can. But most proof systems for temporal logics (including the one in the slides that you pointed to) are Hilbert-style systems that are not exactly easy to use in practice. If you are lucky, temporal logic books show by induction that you can provably substitute a subformula for an equivalent one and then appeal to this lemma in later proofs.

However, one nice aspect of propositional temporal logic (PTL) is that it is decidable. So, you could use some decision procedure for PTL such as ls4 (http://www.cs.man.ac.uk/~sudam/, the system that we use in the TLA+ Proof System) and ask it if the formula

[](P <=> Q) /\ [](R <=> S) => []( (P until R) <=> (Q until S) )

is valid, and it will tell you that it is. The validity of this formula is equivalent to the validity of your sequent.

Why is predicate calculus never explained in slides of the kind mentionned above?

First-order temporal logic is easy to define semantically, but hard to axiomatize. In fact, it is expressive enough to unambiguously define arithmetic with addition and multiplication over the natural numbers and any formal axiom system must therefore be incomplete, by Gödel's incompleteness theorem. So logicians find first-order temporal logic mostly boring, unless they can find a fragment with nice meta-properties such as decidability. For deductive program verification, you cannot avoid it but only use a few basic axioms such as

(\A x : []F(x)) <=> [](\A x : F(x))

and a rule for proving liveness from well-founded orderings such as

(S, <) is well-founded
(\A x \in S : F(x) ~> (G \/ \E y \in S : y < x /\ F(y)) => ((\E x \in S : F(x)) ~> G)

Best regards,