Basic properties of the algorithm
The algorithm is well-defined: at any time during the computation of the algorithm, the marked arguments are a stage.
If the attack graph is finite and contains no attack loops, the algorithm assigns a status to all arguments and stops.
? An argument that is not assigned a status is the first in a chain ?0, ?1, ... of unmarked arguments such that ?i+1 attacks ?i.