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

Re: LTL axiomatic system




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