A note on LTL vs CTL

• Syntax. A quantifier in a CTL formula are in form of a path quantifier $A,E$ following by a state quantifier $F,X,G,U,W$. A quantifier in an LTL is a combination of state quantifiers.
• States and paths. A CTL formula $\phi$ is a state formula, meaning that the temporal operators are state-based in structure: the derivation of a given formula is per-state and depends on the derivation of subformulas for subsequent states. For example, computing the set of states satisfying $AG\,φ$ relies on computing the set of states satisfying $φ$.
  In contrast, LTL formula $\psi$ is a path formula: the derivation of a given formula depends on the derivation of subformulas for suffixes of a path.
• Entailments. We write $M,s \models \phi$ and $M,p \models \psi$ for state $s$ and path $p$. Given a set $I$ of initial states of $M$, we write $M ⊨ φ$ if $M, s ⊨ φ$ for all $s ∈ I$, and write $M ⊨ ψ$ if $M, p ⊨ ψ$ for any path $p$ starting from $I$.
• LTL and CTL are incomparable. The reset property $AG (EF\,φ)$ (i.e. there is always a possibility that $\phi$ could hold, though it may never hold) cannot be expressed in LTL. The stability property $FG\,φ$ cannot be expressed in CTL. Consider a system $M: (s_0,s_0),(s_0,s_1),(s_1,s_2),(s_2,s_2)$ such that $s_0$ is the initial state, $s_0,s_2 \models φ$, and $s_1 \models \neg φ$. Then $M \not\models AFAG\,φ$ but $M \models FG\,φ$.
  It is known that an LTL formula can be over-approximated with ∀CTL [6]: if an ∀CTL property (consisting of AG and AF sub-properties) holds, then an analogous LTL property (where we replace AG with G and AF with F) also holds.
• Structure vs traces. CTL can characterize the structure while LTL only characterizes the traces. Consider the following two systems:
  $A:$ $(s_1,s_2),\ (s_1,s_3),\ (s_2,s_4),\ (s_3,s_5),\ (s_4,s_1),\ (s_5,s_1)$
  $B:$ $(s_1,s_2),\ (s_2,s_4),\ (s_2,s_5),\ (s_4,s_1),\ (s_5,s_1)$
  where $L(s_1)=a,\ L(s_2)=L(s_3)=b,\ L(s_4)=c,\ L(s_5)=d$. Both systems have traces $(ab(c+d))^\omega$ and thus cannot be distinguished in LTL. On the other hand, $B$ is a model of $AG(b\Rightarrow EX\ c)$ while $A$ isn't.
• There are lots of discussions over the best logic to express properties for software verification (cf. [2,5]). LTL can express important properties for software system modelling such as fairness, while the CTL must have a new semantics to express them, for example CTL* [4] or CTL+Fair [3]. But CTL algorithms are usually more efficient and can use BDD-based algorithms. Hence reachers have tried to approximate LTL verification using CTL model checking techniques, e.g., [7].

References

1. Making prophecies with decision predicates, POPL 2011.
2. Branching vs. Linear Time: Final Showdown, TACAS 2001.
3. Fairness for Infinite-State Systems, TACAS 2015.
4. Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems, JACM 2017.
5. Concurrency: the Works of Leslie Lamport, ACM Press 2019.
6. The common fragment of CTL and LTL, FOCS, 2000.
7. Temporal verification of programs, PhD Thesis, 2012.

Enumeration in C#

Enumerating a collection

In C#, a collection class needs to implement IEnumerable to be used in foreach. This interface provides a function GetEnumerator that returns an IEnumerator instance (called an enumerator, which may or may not be the collection itself) supporting operations such as Reset, Current, and MoveNext. An enumerator serves as a proxy to sequentially access the elements in a collection. However, the behavior of a enumerator can be problematic if the underlying collection is modified while the enumeration is in progress. There are several approaches to deal with this problem. One is to take a snapshot of the collection for enumeration. Another approach is to locate the elements on demand, so that the ith enumerated element is always the ith element, if any, in the current collection. To guarantee this, it may take linear time to visit each element and thus quadratic time to enumerate a collection using foreach. The third approach is to throw an exception when the enumerator detects that the contents of the collection changed during enumeration. The last approach is most frequently adopted in C#'s standard libraries for performance concerns. Even so, the first approach can be realized in the call site by creating a snapshot manually using ICollection.CopyTo.
In Java, Iterator.remove is the only safe way to modify a collection during iteration; the behavior of an iterator is unspecified if the underlying collection is modified in any other way. Besides, if you happen to have a ListIterator then you can use ListIterator.add to insert elements in addition to removing them during iteration.

Enumerators are not Enumerable

While it is enumerators that are used for enumeration, foreach has to work with an IEnumerable instance from which an enumerator is obtained. Namely, one can not directly use an enumerator in a foreach loop. In Java, this is not a problem because an anonymous interface instance can be easily created on the fly when it is needed. For example, one common scenario to instantiate an interface anonymously in Java is to create a task for a thread:

new Thread (new Runnable() { public void run() { ... } }).start();

In the snippet, an anonymous Runnable class is created, used and then discarded at runtime. Anonymous classes come in handy when Java programmers want to create classes to serve as workers, listeners, adapters, etc. By contrast, C# programmers are expected to use anonymous functions (delegates or lambdas) for these purposes. While C# does supports anonymous classes, anonymous classes in C# look more like structs than classes, as they can only have public read-only properties and they are not allowed to extend classes (other than object) or implement interfaces.
Although one cannot use an enumerator with foreach, it is almost as easy to use it in a while loop:

while (enum.MoveNext()) { Process(enum.Current); }

However, in situations where an enumerable instance is explicitly required (e.g., by the constructor of a collection), it will take some tricks to convert an enumerator to an enumerable instance at runtime.