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

Re: [tlaplus] LTL axiomatic system

On 15 Aug 2016, at 19:41, 'fl' via tlaplus <tla...@xxxxxxxxxxxxxxxx> 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).


[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.