Infinite trees, markings, and well-foundedness

AbstractA necessary and sufficient condition for a given marked tree to have no infinite paths satisfying a given formula is presented. The formulas are taken from a language introduced by Harel, covering a wide scale of properties of infinite paths, including most of the known notions of fairness. This condition underlies a proof rule for proving that a nondeterministic program has no infinite computations satisfying a given formula, interpreted over state sequences. We also show two different forms of seemingly more natural necessary and sufficient conditions to be inadequate