Church's Problem Revisited

DOI10.2307/421091zbMath0932.03029OpenAlexW2024941371MaRDI QIDQ4262605

Moshe Y. Vardi, Orna Kupferman

Publication date: 22 September 1999

Published in: Bulletin of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/4470e014837a60ede7678296d7ac2ff1dc35bdc4

zbMATH Keywords

specificationalternationalternating tree automataprogram synthesisopen systemclosed systembranching temporal logicslinear temporal logicssynthesis with incomplete information

Mathematics Subject Classification ID

Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (21)

Modular strategies for recursive game graphs ⋮ Distributed synthesis for well-connected architectures ⋮ Synthesis with rational environments ⋮ Latticed-LTL synthesis in the presence of noisy inputs ⋮ Supervisory control and reactive synthesis: a comparative introduction ⋮ Finding and fixing faults ⋮ Distributed Synthesis for Alternating-Time Logics ⋮ ATL* Satisfiability Is 2EXPTIME-Complete ⋮ Unnamed Item ⋮ GR(1)*: GR(1) specifications extended with existential guarantees ⋮ Distributed synthesis for regular and contextfree specifications ⋮ Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems ⋮ CTL\(^\ast\) with graded path modalities ⋮ Sensing as a Complexity Measure ⋮ DEL-sequents for progression ⋮ DEL-sequents for progression ⋮ Synthesis of Fault-Tolerant Distributed Systems ⋮ SEMI-AUTOMATIC DISTRIBUTED SYNTHESIS ⋮ Synthesizing structured reactive programs via deterministic tree automata ⋮ Synthesis in presence of dynamic links ⋮ Automated Synthesis: a Distributed Viewpoint

Cites Work

• Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
• Using branching time temporal logic to synthesize synchronization skeletons
• Alternating automata on infinite trees
• The temporal semantics of concurrent programs
• Decision procedures and expressiveness in the temporal logic of branching time
• Deciding full branching time logic
• “Sometimes” and “not never” revisited
• A Deductive Approach to Program Synthesis

This page was built for publication: Church's Problem Revisited