News
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!