Computation tree logic: Difference between revisions

Revision as of 02:21, 10 June 2021

Revision as of 20:24, 16 March 2022

Line 22:

For example, the following is a well-formed CTL formula:

:<math>\mbox{EF }(\mbox{EG } p \Rightarrow \mbox{AF } r )</math>)

The following is not a well-formed CTL formula:

:<math>\mbox{EF }\big(r \mbox{ U } q\big) </math>

The problem with this string is that <math>U</math> can occur only when paired with an <math>A</math> or an <math>E</math>. <!-- TODO: explain it is evaluated over multiple paths /// here is a copy-paste from the LTL page: build up from proposition variables p1,p2,..., LTL formulas are generally evaluated over paths and a position on that path. A LTL formula as such is satisfied if and only if it is satisfied for position 0 on that path. -->