LTL operator precedence rules

Written on 16.12.2022 17:43 by Bernd Finkbeiner

Dear All, During the discussion session today, we discovered that the precedence order on the LTL operators defined in the lecture notes does not match what you may know from popular textbooks like Baier/Katoen. We decided to change the precedence rules in the lecture notes so that unary operators bind stronger than binary operators, Until takes precedence over conjunction, and negation and Next bind equally strongly. Sorry for the confusion! Note that this change affects the interpretation of the formulas in Warm-up Question 4 from the current set of questions. The updated lecture notes are available under Materials, together with a list of all changes we made since the beginning of the course. Thanks for the discussions today, have a great weekend!

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.