Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness
- 2 January 1986
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 33 (1), 224-248
- https://doi.org/10.1145/4904.4993
Abstract
Elementary translations between various kinds of recursive trees are presented. It is shown that trees of either finite or countably infinite branching can be effectively put into one-one correspondence with infinitely branching trees in such a way that the infinite paths of the latter correspond to the “P-abiding” infinite paths of the former. Here P can be any member of a very wide class of properties of infinite paths. For many properties ??, the converse holds too. Two of the applications involve (a) the formulation of large classes of highly undecidable variants of classical computational problems, and in particular, easily describable domino problems that are III11-complete, and (b) the existence of a general method for proving termination of nondeterministic or concurrent programs under any reasonable notion of fairness.Keywords
This publication has 15 references indexed in Scilit:
- Proof rules and transformations dealing with fairnessScience of Computer Programming, 1983
- Propositional dynamic logic of nonregular programsJournal of Computer and System Sciences, 1983
- ScriptPublished by Association for Computing Machinery (ACM) ,1983
- Topological characterizations of infinite behaviours of transition systemsPublished by Springer Nature ,1983
- A Weaker Precondition for LoopsACM Transactions on Programming Languages and Systems, 1982
- A Cook's Tour of Countable NondeterminismDAIMI Report Series, 1981
- Characterizing correctness properties of parallel programs using fixpointsLecture Notes in Computer Science, 1980
- Communicating sequential processesCommunications of the ACM, 1978
- The decision problem for standard classesThe Journal of Symbolic Logic, 1976
- Turing-machines and the EntscheidungsproblemMathematische Annalen, 1962