Abstract
Algorithmic properties of nondeterministic programs are studied and axiomatized completely. Nondeterministic programs require two kinds of algorithmic formulas describing their behaviour: ΔKa – all computations of the program K are finite and all results satisfy a and ∇Ka – there exists a finite computation such that its result satisfies the formula a.
Get full access to this article
View all access options for this article.