Decidability of Second-Order Theories and Automata on Infinite Trees

From MaRDI portal
Publication:5625141

DOI10.2307/1995086zbMath0221.02031OpenAlexW4240244556WikidataQ30052266 ScholiaQ30052266MaRDI QIDQ5625141

Michael O. Rabin

Publication date: 1969

Published in: Transactions of the American Mathematical Society (Search for Journal in Brave)

Full work available at URL: https://projecteuclid.org/euclid.bams/1183529958



Related Items

Index Problems for Game Automata, On Composing Finite Forests with Modal Logics, Solving Infinite Games in the Baire Space, Measure Quantifier in Monadic Second Order Logic, A propositional dense time logic, Conditional rewrite rule systems with built-in arithmetic and induction, Multi-Valued Reasoning about Reactive Systems, Unnamed Item, Unnamed Item, Unnamed Item, Deciding equivalence of finite tree automata, Automatic presentations of structures, Algebraic characterizations and block product decompositions for first order logic and its infinitary quantifier extensions over countable words, On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic, Reachability games and parity games, Reasoning about Quality and Fuzziness of Strategic Behaviors, Model completion of scaled lattices and co‐Heyting algebras of p‐adic semi‐algebraic sets, The lattice of definability: origins, recent developments, and further directions, On the Boolean Closure of Deterministic Top-Down Tree Automata, An interval temporal logic characterization of extended \(\omega\)-regular languages, Generalized quantifiers and well orderings, Unnamed Item, Liminf progress measures, Compatibility of refining and controlling plant automata with bisimulation quotients, First-order separation over countable ordinals, Modal logics and local quantifiers: a zoo in the elementary hierarchy, Unnamed Item, Unnamed Item, Unnamed Item, A hierarchy of tree-automatic structures, Complete theories of unars, Deciding low levels of tree-automata hierarchy, Pebble Weighted Automata and Weighted Logics, Monadic Second Order Logic And Its Fragments, On Expressive Power of Regular Expressions over Infinite Orders, Further Generalizations of Results on Structures of Continuous Functions, Grid structures and undecidable constraint theories, A list of arithmetical structures complete with respect to the first-order definability, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Free \(\mu\)-lattices, Automata on infinite trees with counting constraints, Computing the Rabin Index of a Parity Automaton, Unnamed Item, Tree Automata over Infinite Alphabets, Selection and Uniformization Problems in the Monadic Theory of Ordinals: A Survey, Church’s Problem and a Tour through Automata Theory, Incremental reasoning on monadic second-order logics with logic programming, Stone duality, topological algebra, and recognition., Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure, Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure, Decidable Expansions of Labelled Linear Orderings, An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning, Logic and rational languages of scattered and countable series-parallel posets, An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning, Monoidal-closed categories of tree automata, On Repetition Languages, A Survey of Bidding Games on Graphs (Invited Paper), Unnamed Item, COMPLETE ADDITIVITY AND MODAL INCOMPLETENESS, A Characterisation of Pi^0_2 Regular Tree Languages, Unambiguity in Automata Theory, A Tentative Approach for the Wadge-Wagner Hierarchy of Regular Tree Languages of Index [0, 2], An upper bound on the complexity of recognizable tree languages, Towards Efficient Verification of Systems with Dynamic Process Creation, Unnamed Item, Projection for Büchi Tree Automata with Constraints between Siblings, Rabin vs. Streett Automata, Backward Deterministic Büchi Automata on Infinite Words, Recursive unary algebras and trees, The finite graph problem for two-way alternating automata., Future temporal logic needs infinitely many modalities, The monadic second order logic of graphs. VI: On several representations of graphs by relational structures, A branching time logic with past operators, Progress measures, immediate determinacy, and a subset construction for tree automata, Memoryless determinacy of parity and mean payoff games: a simple proof, Rabin tree automata and finite monoids, Graded modalities in strategy logic, Chain automata, Somewhat finite approaches to infinite sentences., The \(\mu\)-calculus alternation depth hierarchy is infinite over finite planar graphs, Determinization and memoryless winning strategies, On control of systems modelled as deterministic Rabin automata, Order-couniversality of the complete infinitary tree: an application of zero-divisor graphs, A first-order axiomatization of the theory of finite trees, The Lindenbaum-Tarski algebra for Boolean algebras with distinguished ideals, Propositional quantification in the topological semantics for \(\mathbf S4\), Finite-state strategies in delay games, Fixed point characterization of infinite behavior of finite-state systems, A first order logic of effects, Program schemata vs. automata for decidability of program logics, Finite automata on timed \(\omega\)-trees, Infinite-duration poorman-bidding games, The complexity of the temporal logic with ``until over general linear time, From bidirectionality to alternation., Unambiguous Büchi automata., A gap property of deterministic tree languages., Effective categoricity of automatic equivalence and nested equivalence structures, A note on ordinal DFAs, On the mosaic method for many-dimensional modal logics: a case study combining tense and modal operators, Mathematical modal logic: A view of its evolution, Model checking the full modal mu-calculus for infinite sequential processes, Program schemata technique for propositional program logics: a 30-year history, Certifying inexpressibility, Inverse monoids and rational Schreier subsets of the free group, On automata on infinite trees, Quantum \(\omega\)-automata over infinite words and their relationships, Finite automata on directed graphs, The monadic second-order logic of graphs. VII: Graphs as relational structures, Alternating automata, the weak monadic theory of trees and its complexity, Moderate families in Boolean algebras, Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics, Infinite trees and automaton-definable relations over \(\omega\)-words, Rabin's theorem in the concurrency setting: a conjecture, Model-theoretic properties of \(\omega\)-automatic structures, On the descriptional complexity of finite automata with modified acceptance conditions, The Borel hierarchy is infinite in the class of regular sets of trees, Theories of automata on \(\omega\)-tapes: a simplified approach, The decision problem for some finite extensions of the intuitionistic theory of abelian groups, Pure-irreducible mono-unary algebras, Weak Muller acceptance conditions for tree automata, Lattice-theoretic decision problems in universal algebra, Boolean powers, Decidable locally finite discriminator varieties arising from dihedral varieties of groups, Timer formulas and decidable metric temporal logic, \(\aleph_0\)-categoricity for rings without nilpotent elements and for Boolean structures, Monadic theory of order and topology, I, Theory of \(\omega\)-languages. I: Characterizations of \(\omega\)-context- free languages, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, \(\omega\)-computations on Turing machines, Decidability of a portion of the predicate calculus, Finite automata, definable sets, and regular expressions over \(\omega^n\)- tapes, An axiom system for the weak monadic second order theory of two successors, Using partial orders for the efficient verification of deadlock freedom and safety properties, A system of dynamic modal logic, Combining temporal logic systems, A sufficient condition for finite decidability, Infinite games on finitely coloured graphs with applications to automata on infinite trees, Algebras for querying text regions: Expressive power and optimization, Decidability of quantified propositional intuitionistic logic and S4 on trees of height and arity \(\leq \omega\), \( \omega \)-automata, Automata on finite trees, Automata on infinite trees, Set constraints and automata, A language hierarchy and kitchens-type theorem for self-similar groups, Monadic second-order logic, graph coverings and unfoldings of transition systems, Weak essentially undecidable theories of concatenation, On decidability of list structures, A logic-based approach to incremental reasoning on multi-agent systems, First order theory of permutation groups, Decidability results in non-classical logic. III: Systems with statability operators, A characterization of Büchi tree automata, Decidable fragments of first-order temporal logics, Guarded fixed point logics and the monadic theory of countable trees., On infinite transition graphs having a decidable monadic theory, Sequentiality, monadic second-order logic and tree automata., Ordering constraints over feature trees expressed in second-order monadic logic., Counting modulo quantifiers on finite structures, Module checking, An infinite hierarchy of temporal logics over branching time, A formal theory of simulations between infinite automata, Thue trees, The evaluation of first-order substitution is monadic second-order compatible, Axiomatisation and decidability of \(F\) and \(P\) in cyclical time, Finite variability interpretation of monadic logic of order, Monadic second-order logic on tree-like structures, A second-order formulation of non-termination, Shelah-Stupp's and Muchnik's iterations revisited, wMSO theories as grammar formalisms, Tree-automatic scattered linear orders, Trees, grids, and MSO decidability: from graphs to matroids, Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints, Variétés d'automates descendants d'arbres infinis, Construction of decidable singular theories of two successor functions with an extra predicate, Infinite-word languages and continuous mappings, The greatest fixed-points and rational omega-tree languages, Elementary and algebraic properties of the Arens-Kaplansky constructions, The theory of ends, pushdown automata, and second-order logic, Recursive categoricity and recursive stability, Decidable unary varieties, Matching regular expressions on uncertain data, Regular languages of thin trees, Alternation and \(\omega\)-type Turing acceptors, The complementation problem for Büchi automata with applications to temporal logic, Automata-theoretic techniques for modal logics of programs, Topological characterizations of infinite tree languages, Undecidability of theories of Boolean algebras with selected ideals, The word problem for \(Heyting^ *\) algebras, Automata-based verification of programs with tree updates, Factorization forests for infinite words and applications to countable scattered linear orderings, Alternating automata on infinite trees, Countably-categorical Boolean algebras with distinguished ideals, On a subclass of \(\infty\)-regular languages, On the complexity of the two-variable guarded fragment with transitive guards, On alternating \(\omega\)-automata, Some general incompleteness results for partial correctness logics, Logic programming approach to automata-based decision procedures, Finitely axiomatizable Boolean algebras with distinguished ideals, Logical definability of fixed points, Complementing deterministic Büchi automata in polynomial time, Reduced sub-powers and the decision problem for finite algebras in arithmetical varieties, An automata theoretic decision procedure for the propositional mu- calculus, Algorithmic uses of the Feferman-Vaught theorem, On translations of temporal logic of actions into monadic second-order logic, Choice functions and well-orderings over the infinite binary tree, Automata-theoretic decision of timed games, Cellular automata between sofic tree shifts, Preface to the special issue: Temporal logics of agency, Prevarieties of associative rings whose elementary theory is decidable, Monadic theory of order and topology. II, The decidability of some classes of Stone algebras, Büchi context-free languages, Temporal logics over linear time domains are in PSPACE, On the almighty wand, On the expressive power of univariate equations over sets of natural numbers, The first order theory of Boolean algebras with a distinguished group of automorphisms, Automata and logics over finitely varying functions, Model-theoretic complexity of automatic structures, The complexity of temporal logic over the reals, Decidability for branching time, Synthesis from scenario-based specifications, Coalgebraic semantics of modal logics: an overview, Petri nets and regular languages, Groups, graphs, languages, automata, games and second-order monadic logic, A dynamic deontic logic for complex contracts, SnS can be modally characterized, A uniform method for proving lower bounds on the computational complexity of logical theories, On direct products of automaton decidable theories, Classification of finite coloured linear orderings, Process logic: Expressiveness, decidability, completeness, Constructivizations of Boolean algebras, A regular characterization of graph languages definable in monadic second-order logic, Generalized automata on infinite trees and Muller-McNaughton's theorem, Weak theories of concatenation and minimal essentially undecidable theories. An encounter of \(\mathsf{WTC}\) and \(\mathsf{S2S}\), Deductive verification of alternating systems, Interval logics and their decision procedures. I: An interval logic, Recognizable languages in concurrency monoids, An initial semantics for the \(\mu\)-calculus on trees and Rabin's complementation lemma, Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra, On the equivalence of recursive and nonrecursive Datalog programs, Dynamical systems in categories, Weighted automata and logics for infinite nested words, A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata, Partially commutative inverse monoids., Doomsday equilibria for omega-regular games, Series-parallel languages on scattered and countable posets, Logical aspects of Cayley-graphs: the group case, Queries on XML streams with bounded delay and concurrency, \(\omega\)-regular languages are testable with a constant number of queries, Strategy logic, On mathematical contributions of Paul E. Schupp, Logic and rational languages of words indexed by linear orderings, Automata on infinite objects and their applications to logic and programming, Counting branches in trees using games, A Rice-style theorem for parallel automata, Program repair without regret, Mathematical logic and quantum finite state automata, Regular sets over extended tree structures, From liveness to promptness, On relation between linear temporal logic and quantum finite automata, A view of computability on term algebras, Infinitary tree languages recognized by \(\omega\)-automata, Alternating finite automata on \(\omega\)-words, Graded modalities. I, The monadic second-order logic of graphs. IV: Definability properties of equational graphs, Determinacy of sinking automata on infinite trees and inequalities between various Rabin's pair indices, The structure of the models of decidable monadic theories of graphs, Decidability of extended theories of addition of the natural numbers and the integers, Unresolved systems of language equations: expressive power and decision problems, On Vaught’s Conjecture and finitely valued MV algebras, Succinct definitions in the first order theory of graphs, Simple monadic theories and partition width, Limited Set quantifiers over Countable Linear Orderings, Trading Bounds for Memory in Games with Counters, Baire Category Quantifier in Monadic Second Order Logic, Hyperfinite MV-algebras, Automata Theory and Model Checking, The mu-calculus and Model Checking, Graph Games and Reactive Synthesis, Unnamed Item, Changing a Semantics: Opportunism or Courage?, Complementation of rational sets on scattered linear orderings of finite rank, Inverse monoids: decidability and complexity of algebraic questions., A logic of reachable patterns in linked data-structures, Asymptotic Monadic Second-Order Logic, The monadic second-order logic of graphs, II: Infinite graphs of bounded width, Some new results in monadic second-order arithmetic, Sheaf Constructions and Their Elementary Properties, Bidding mechanisms in graph games, Measure properties of regular sets of trees, Deciding the unguarded modal -calculus, Randomization in Automata on Infinite Trees, Reasoning About Strategies, Composition Over the Natural Number Ordering with an Extra Binary Relation, Separation logics and modalities: a survey, Typing Weak MSOL Properties, Regular prefix relations, Index appearance record with preorders, Model Theoretic Complexity of Automatic Structures (Extended Abstract), Decidability of the Clark's completion semantics for monadic programs and queries, Contribution of Warsaw logicians to computational logic, Two-Variable Separation Logic and Its Inner Circle, Descriptive complexity of \(\mathsf{qc} \mathsf{b}_0\)-spaces, Reasoning About Substructures and Games, On frontiers of regular trees, Church-Rosser property and decidability of monadic theories of unary algebras, The Non-deterministic Mostowski Hierarchy and Distance-Parity Automata, Logics and Automata for Totally Ordered Trees, Unnamed Item, Distributed synthesis is simply undecidable, Model Transformations in Decidability Proofs for Monadic Theories, On the Almighty Wand, Description of restricted automata by first-order formulae, Decidability of a partial order based temporal logic, A kleene theorem for recognizable languages over concurrency monoids, Decidability of equivalence for a class of non-deterministic tree transducers, On the strength of some topological lattices, Model-interpretability into trees and applications, The recursive sets in certain monadic second order fragments of arithmetic, The Modal μ-Calculus Caught Off Guard, Regular Languages of Words over Countable Linear Orderings, Walther recursion, Unnamed Item, Stack and locally finite transformations on structures with reversible transitions, The Quest for a Tight Translation of Büchi to co-Büchi Automata, On Monadic Theories of Monadic Predicates, An Automata-Theoretic Approach to Infinite-State Systems, Computing by commuting., The monadic second-order logic of graphs. XV: On a conjecture by D. Seese, Automata and fixed point logic: a coalgebraic perspective, Iterated pushdown automata and sequences of rational numbers, Expressivity of second order propositional modal logic, \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\), Quantification over sets of possible worlds in branching-time semantics, Complementation of Branching Automata for Scattered and Countable N-Free Posets, Logic and Bounded-Width Rational Languages of Posets over Countable Scattered Linear Orderings, A general method for proving decidability of intuitionistic modal logics, AN ALGEBRAIC APPROACH TO MSO-DEFINABILITY ON COUNTABLE LINEAR ORDERINGS, On Distributed Program Specification and Synthesis in Architectures with Cycles, Unary automatic graphs: an algorithmic perspective, Facets of Synthesis: Revisiting Church’s Problem, Tighter Bounds for the Determinisation of Büchi Automata, Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata, Beyond Shapes: Lists with Ordered Data, Unnamed Item, Theories of orders on the set of words, Tree Automata and Automata on Linear Orderings, Decidable Discriminator Varieties from Unary Classes, Complementation of Branching Automata for Scattered and Countable Series-Parallel Posets, Weighted Automata and Logics on Infinite Graphs, Definability in the Infix Order on Words, Tree acceptors and some of their applications, Unnamed Item, Cardinality Quantifiers in MLO over Trees, Linear Game Automata: Decidable Hierarchy Problems for Stripped-Down Alternating Tree Automata, On the Complexity of Branching-Time Logics, MSO-definable Properties of Muller Context-Free Languages Are Decidable, On decidable, finitely axiomatizable, modal and tense logics without the finite model property. I, II, Bounded sets of nodes in transfinite trees, Monadic Second Order Logic with Measure and Category Quantifiers, A generalization of Ehrenfeucht's game and some applications, On the theory of convex subsets, Model checking the full modal mu-calculus for infinite sequential processes, A Characterization of Finitely Decidable Congruence Modular Varieties, Relating word and tree automata, Monadic <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si1.gif" overflow="scroll"><mml:msubsup><mml:mi mathvariant="normal">Σ</mml:mi><mml:mn>1</mml:mn><mml:mn>1</mml:mn></mml:msubsup></mml:math> and Modal Logic with Quantified Binary Relations, Context-free languages, groups, the theory of ends, second-order logic, tiling problems, cellular automata, and vector addition systems, Synthesis for continuous time, Locally finite properties of data structures and their computation