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

Re: [tlaplus] LTL axiomatic system



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

On 11 Aug 2016, at 16:33, 'fl' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:


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)


Can you validate its accuracy?

--
FL

--
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.