LTL axiomatic system

[fl]

Can somebody confirm me that the following formula may be regarded as an axiom of LTL?

http://us2.metamath.org:88/mpegif/ax-ltl5.html

--
FL

[ka...@cse.unsw.edu.au]

What you wrote is an axiom for the weak until or unless operator, typically written W, not to be confused with the (strong) until operator denoted by U.

[fl]

What you wrote is an axiom for the weak until or unless operator, typically written W, not to be confused with the (strong) until operator denoted by U.

Thank you.

Here is a system of axioms for LTL (slide 7)

http://www.csc.kth.se/~mfd/Courses/Temporal_logic/lecture2.pdf 

Can you validate its accuracy?

--

FL

[Stephan Merz]

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

Fred Kröger, Stephan Merz. Temporal Logic and State Systems. Texts in Theoretical Computer Science, Springer, 2008.

http://www.springer.com/us/book/9783540674016

Best regards,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[fl]

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

Fred Kröger, Stephan Merz. Temporal Logic and State Systems. Texts in Theoretical Computer Science, Springer, 2008.

http://www.springer.com/us/book/9783540674016

Hi Stephan,

I've tried to buy it. Only Eyrolles accepted to order it for me.  They needed to make it come from the USA. When

I asked for the price they answered they couldn't know because the exchange rate dollar fluctuates and at the end I had

to fill in a complete form. I had the impression to apply to a job as a civil servant. I gave up.

It is called globalization I suppose.

But well maybe I must muster up the courage to try again.

-- 

FL

[fl]

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 ) ) 

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

-- 

FL

[Stephan Merz]

On 12 Aug 2016, at 12:47, 'fl' via tlaplus <tla...@googlegroups.com> 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,

Stephan

[fl]

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) )

Hi Stephan,

thank you for answer. LS4 is no longer available apparently. Since you plugged it into TLAPLUS, if I enter the formula will I have the answer? Because in that case I will often use it this way.

Another question and then I dfefinitely go and buy books: why have you added the [] operators to your formula because
in the inference rule you don't need them either in the premisser or in the conclusion.

--
FL

[fl]

First-order temporal logic is easy to define semantically, but hard to axiomatize.

But can we find such a system of axioms somewhere?

--
FL
 

[Stephan Merz]

On 15 Aug 2016, at 19:41, 'fl' via tlaplus <tla...@googlegroups.com> wrote:

First-order temporal logic is easy to define semantically, but hard to axiomatize.

But can we find such a system of axioms somewhere?

Here are the (necessarily incomplete) rules, in addition to those for PTL, that we use in our book:

A(t) => \E x : A(x)  if t is substitutable for x [1]

(next \E x : A) => \E x : next A

A => next A  if A is rigid (i.e., does not contain any state variable)

x = x

x = y => (A(x) => A(y))

A => B |- (\E x : A) => B  if there is no free occurrence of x in B

Most of these are standard from classical first-order logic (modulo the additional proviso in the first axiom). The second and third axiom bring in an aspect of temporal logic, expressing that quantification (over rigid variables, i.e. constants in TLA jargon) and temporal operators commute (similar laws for [], <>, and the "until" operator are then derivable), and that the interpretation of all symbols except state variables is the same in all states.

For TLA, you'll need additional rules governing flexible quantification (the \EE operator).

Stephan

[1] The term t is called substitutable for x in formula A(x) if A(t) has no new occurrences of state variables in the scope of a temporal operator as compared with A(x). For example, consider the formula A == (x=0) /\ <>(x # 0) and a state variable v. Then v is not substitutable for x because the substitution would introduce an additional occurrence of state variable v in the scope of the <> operator. And indeed, the instance

  v=0 /\ <>(v # 0) => \E x : (x=0) /\ <>(x # 0)

would be unsound, as the right-hand formula is equivalent to false (remember that x is a rigid variable) whereas the left-hand formula may be true in some execution.

[Stephan Merz]

On 15 Aug 2016, at 19:29, 'fl' via tlaplus <tla...@googlegroups.com> wrote:

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) )

Hi Stephan,

thank you for answer. LS4 is no longer available apparently.

Indeed, but there are similar decision procedures, e.g. TRP++ (https://cgi.csc.liv.ac.uk/~konev/software/trp++/) or the Logics Workbench (http://www.lwb.unibe.ch, you can even enter your formula via a Web form).

Since you plugged it into TLAPLUS, if I enter the formula will I have the answer? Because in that case I will often use it this way.

Yes, you can (except that "until" is not accepted):

LEMMA 

  ASSUME NEW TEMPORAL P, NEW TEMPORAL Q

  PROVE  [](P <=> Q) => ([]<>P <=> []<>Q)

BY PTL

Another question and then I dfefinitely go and buy books: why have you added the [] operators to your formula because
in the inference rule you don't need them either in the premisser or in the conclusion.

The sensible interpretation of the inference rule that you gave is that the formulas stated in the antecedent are supposed to hold everywhere (i.e., always in the future), hence they must be boxed in the formula. The formula

  (P <=> Q) => ([]<>P <=> []<>Q)

is not valid since P and Q are assumed to be equivalent only in the initial state, and nothing is known about their relationship in other states. More generally, a rule (temporal sequent)

  Gamma, F |- B

for some set of formulas Gamma is equivalent to the sequent

  Gamma |- []F => B

but not the sequent

  Gamma |- F => B

In other words, the standard deduction theorem of classical logic has to be modified for temporal (and similar modal) logics. Leslie often refers to this as "temporal logic being evil".

Best,

Stephan

[Ioannis Filippidis]

On Monday, August 15, 2016 at 10:29:30 AM UTC-7, fl wrote:

 

 LS4 is no longer available apparently.

--
FL

Hi FL,

The temporal logic prover `ls4` is available at [1].

[1] https://github.com/quickbeam123/ls4

Ioannis

[fl]

 

Hi Ioannis,

The temporal logic prover `ls4` is available at [1].

Thank you very much. I download it now. It is referenced by my toolbox but

since it was no longer available...  And anyway it deserves to be used by itself.

(There is a library that is already compiled I just hope it is not compiled with the

most recent linux libraries because my box is about 5 years old. I sometimes try to

persuade people to use old libraries but with no success until now.)

-- 

FL