The Experts below are selected from a list of 309 Experts worldwide ranked by ideXlab platform
Maurice Margenstern - One of the best experts on this subject based on the ideXlab platform.
-
A decidability result for the Halting Problem of cellular automata in the pentagrid.
arXiv: Formal Languages and Automata Theory, 2018Co-Authors: Maurice MargensternAbstract:In this paper, we investigate the Halting Problem for deterministic cellula automata in the pentagrid. We prove that the Problem is decidable when the cellular automaton starts its computation from a finite configuration and when it has at most two states, one of them being a quiescent state.
-
universality and the Halting Problem for cellular automata in hyperbolic spaces the side of the Halting Problem
International Conference on Unconventional Computation, 2012Co-Authors: Maurice MargensternAbstract:In this paper, we remind results on universality for cellular automata in hyperbolic spaces, mainly results about weak universality, and we deal with the Halting Problem in the same settings. This latter Problem is very close to that of strong universality. The paper focuses on the Halting Problem and it can be seen as a preliminary approach to strong universality about cellular automata in hyperbolic spaces.
-
UCNC - Universality and the Halting Problem for cellular automata in hyperbolic spaces: the side of the Halting Problem
Unconventional Computation and Natural Computation, 2012Co-Authors: Maurice MargensternAbstract:In this paper, we remind results on universality for cellular automata in hyperbolic spaces, mainly results about weak universality, and we deal with the Halting Problem in the same settings. This latter Problem is very close to that of strong universality. The paper focuses on the Halting Problem and it can be seen as a preliminary approach to strong universality about cellular automata in hyperbolic spaces.
-
decidability and undecidability of the Halting Problem on turing machines a survey
Foundations of Computer Science, 1997Co-Authors: Maurice MargensternAbstract:The paper surveys the main results obtained for Turing machines about the frontier between a decidable Halting Problem and universality. The notion of decidability criterion is introduced. Techniques for decidability proofs and for contracting universal objects are sketchily explained. A new approach for finding very small universal Turing machines is considered in the last part of the paper.
-
LFCS - Decidability and Undecidability of the Halting Problem on Turing Machines, a Survey
Logical Foundations of Computer Science, 1997Co-Authors: Maurice MargensternAbstract:The paper surveys the main results obtained for Turing machines about the frontier between a decidable Halting Problem and universality. The notion of decidability criterion is introduced. Techniques for decidability proofs and for contracting universal objects are sketchily explained. A new approach for finding very small universal Turing machines is considered in the last part of the paper.
Kristofer Johannisson - One of the best experts on this subject based on the ideXlab platform.
-
TYPES - Formalizing the Halting Problem in a Constructive Type Theory
Lecture Notes in Computer Science, 2002Co-Authors: Kristofer JohannissonAbstract:We present a formalization of the Halting Problem in Agda, a language based on Martin-Lof's intuitionistic type theory. The key features are: - We give a constructive proof of the Halting Problem. The "constructive Halting Problem" is a natural reformulation of the classic variant. - A new abstract model of computation is introduced, in type theory. - The undecidability of the Halting Problem is proved via a theorem similar to Rice's theorem. The central idea of the formalization is to abstract from the details of specific models of computation. This is accomplished by formulating a number of axioms which describe an abstract model of computation, and proving that the Halting Problem is undecidable in any model described by these axioms.
-
formalizing the Halting Problem in a constructive type theory
Types for Proofs and Programs, 2000Co-Authors: Kristofer JohannissonAbstract:We present a formalization of the Halting Problem in Agda, a language based on Martin-Lof's intuitionistic type theory. The key features are: - We give a constructive proof of the Halting Problem. The "constructive Halting Problem" is a natural reformulation of the classic variant. - A new abstract model of computation is introduced, in type theory. - The undecidability of the Halting Problem is proved via a theorem similar to Rice's theorem. The central idea of the formalization is to abstract from the details of specific models of computation. This is accomplished by formulating a number of axioms which describe an abstract model of computation, and proving that the Halting Problem is undecidable in any model described by these axioms.
Yijia Chen - One of the best experts on this subject based on the ideXlab platform.
-
a parameterized Halting Problem the linear time hierarchy and the mrdp theorem
Logic in Computer Science, 2018Co-Authors: Yijia Chen, Moritz Muller, Keita YokoyamaAbstract:The complexity of the parameterized Halting Problem for nondeterministic Turing machines p-Halt is known to be related to the question of whether there are logics capturing various complexity classes [10]. Among others, if p-Halt is in para-AC0, the parameterized version of the circuit complexity class AC0, then AC0, or equivalently, (+, x)-invariant FO, has a logic. Although it is widely believed that p-Halt ∉. para-AC0, we show that the Problem is hard to settle by establishing a connection to the question in classical complexity of whether NE n LINH. Here, LINH denotes the linear time hierarchy. On the other hand, we suggest an approach toward proving NE n LINH using bounded arithmetic. More specifically, we demonstrate that if the much celebrated MRDP (for Matiyasevich-Robinson-Davis-Putnam) theorem can be proved in a certain fragment of arithmetic, then NE n LINH. Interestingly, central to this result is a para-AC0 lower bound for the parameterized model-checking Problem for FO on arithmetical structures.
-
LICS - A parameterized Halting Problem, the linear time hierarchy, and the MRDP theorem
Proceedings of the 33rd Annual ACM IEEE Symposium on Logic in Computer Science, 2018Co-Authors: Yijia Chen, Moritz Muller, Keita YokoyamaAbstract:The complexity of the parameterized Halting Problem for nondeterministic Turing machines p-Halt is known to be related to the question of whether there are logics capturing various complexity classes [10]. Among others, if p-Halt is in para-AC0, the parameterized version of the circuit complexity class AC0, then AC0, or equivalently, (+, x)-invariant FO, has a logic. Although it is widely believed that p-Halt ∉. para-AC0, we show that the Problem is hard to settle by establishing a connection to the question in classical complexity of whether NE n LINH. Here, LINH denotes the linear time hierarchy. On the other hand, we suggest an approach toward proving NE n LINH using bounded arithmetic. More specifically, we demonstrate that if the much celebrated MRDP (for Matiyasevich-Robinson-Davis-Putnam) theorem can be proved in a certain fragment of arithmetic, then NE n LINH. Interestingly, central to this result is a para-AC0 lower bound for the parameterized model-checking Problem for FO on arithmetical structures.
-
From Almost Optimal Algorithms to Logics for Complexity Classes via Listings and a Halting Problem
Journal of the ACM, 2012Co-Authors: Yijia Chen, Jorg FlumAbstract:Let C denote one of the complexity classes “polynomial time,” “logspace,” or “nondeterministic logspace.” We introduce a logic L(C)inv and show generalizations and variants of the equivalence (L(C)inv captures C if and only if there is an almost C-optimal algorithm in C for the set Taut of tautologies of propositional logic). These statements are also equivalent to the existence of a listing of subsets in C of Taut by corresponding Turing machines and equivalent to the fact that a certain parameterized Halting Problem is in the parameterized complexity class XCuni.
-
a parameterized Halting Problem
The Multivariate Algorithmic Revolution and Beyond, 2012Co-Authors: Yijia Chen, Jorg FlumAbstract:The parameterized Problem $p\textsc{-Halt}$ takes as input a nondeterministic Turing machine $\mathbb{M}$ and a natural number n, the size of $\mathbb{M}$ being the parameter. It asks whether every accepting run of $\mathbb{M}$ on empty input tape takes more than n steps. This Problem is in the class XPuni , the class "uniform XP," if there is an algorithm deciding it, which for fixed machine $\mathbb{M}$ runs in time polynomial in n. It turns out that various open Problems of different areas of theoretical computer science are related or even equivalent to $p{\rm \textsc{-Halt}\in{XP}_{uni}}$. Thus this statement forms a bridge which allows to derive equivalences between statements of different areas (proof theory, complexity theory, descriptive complexity, …) which at first glance seem to be unrelated. As our presentation shows, various of these equivalences may be obtained by the same method.
-
a logic for ptime and a parameterized Halting Problem
Fields of logic and computation, 2010Co-Authors: Yijia Chen, Jorg FlumAbstract:In [9] Yuri Gurevich addresses the question whether there is a logic that captures polynomial time. He conjectures that there is no such logic. He considers a logic, we denote it by L≤, that allows to express precisely the polynomial time properties of structures; however, apparently, there is no algorithm "that given an L≤-sentence ϕ produces a polynomial time Turing machine that recognizes the class of models of ϕ." In [12] Nash, Remmel, and Vianu have raised the question whether one can prove that there is no such algorithm. They give a reformulation of this question in terms of a parameterized Halting Problem p-ACC≤ for nondeterministic Turing machines. We analyze the precise relationship between L≤ and p-ACC≤. Moreover, we show that p-ACC≤ is not fixed-parameter tractable if "P ≠ NP holds for all time constructible and increasing functions." A slightly stronger complexity theoretic hypothesis implies that L≤ does not capture polynomial time. Furthermore, we analyze the complexity of various variants of p-ACC≤ and address the construction Problem associated with p-ACC≤.
Marc Schoenauer - One of the best experts on this subject based on the ideXlab platform.
-
Robustness and the Halting Problem for Multicellular Artificial Ontogeny
IEEE Transactions on Evolutionary Computation, 2011Co-Authors: Alexandre Devert, Nicolas Bredeche, Marc SchoenauerAbstract:Most works in multicellular artificial ontogeny solve the Halting Problem by arbitrarily limiting the number of iterations of the developmental process. Hence, the trajectory of the developing organism in the phenotypic space is only required to come close to an accurate solution during a very short developmental period. Because of the well-known opportunism of evolution, there is indeed no reason for the organism to remain close to a good solution in other situations: if the development is continued after the limiting bound; if the environment is perturbed by some noise during the development; if the development takes place in different physical conditions. In order to increase the robustness of the solution against such hazards, a new stopping criterion for the developmental process is proposed, based on the stability of some internal energy of the organism during its development. Such adaptive stopping criterion biases evolution toward solutions in which robustness is an intrinsic property. Experimental results on different “French flag” Problems demonstrate that enforcing stable developmental process makes it possible to produce solutions that not only accurately approximate the target shape, but also demonstrate near-perfect self-healing properties, as well as excellent generalization capabilities.
-
Robustness and the Halting Problem for Multi-Cellular Artificial Ontogeny
IEEE Transactions on Evolutionary Computation, 2011Co-Authors: Alexandre Devert, Nicolas Bredeche, Marc SchoenauerAbstract:Most works in Multi-Cellular Artificial Ontogeny solve the Halting Problem by arbitrarily limiting the number of iterations of the developmental process. Hence, the trajectory of the developing organism in the phenotypic space is only required to come close to an accurate solution during a very short developmental period. Because of the well-known opportunism of evolution, there is indeed no reason for the organism to remain close to a good solution in other situations: if the development is continued after the limiting bound; if the environment is perturbed by some noise during the development; if the development takes place in different physical conditions. In order to increase the robustness of the solution against such hazards, a new stopping criterion for the developmental process is proposed, based on the stability of some internal energy of the organism during its development. Such adaptive stopping criterion biases evolution toward solutions in which robustness is an intrinsic property. Experimental results on different ''French flag'' Problems demonstrate that enforcing stable developmental process makes it possible to produce solutions that not only accurately approximate the target shape, but also demonstrate near-perfect self-healing properties, as well as excellent generalization capabilities.
Jorg Flum - One of the best experts on this subject based on the ideXlab platform.
-
From Almost Optimal Algorithms to Logics for Complexity Classes via Listings and a Halting Problem
Journal of the ACM, 2012Co-Authors: Yijia Chen, Jorg FlumAbstract:Let C denote one of the complexity classes “polynomial time,” “logspace,” or “nondeterministic logspace.” We introduce a logic L(C)inv and show generalizations and variants of the equivalence (L(C)inv captures C if and only if there is an almost C-optimal algorithm in C for the set Taut of tautologies of propositional logic). These statements are also equivalent to the existence of a listing of subsets in C of Taut by corresponding Turing machines and equivalent to the fact that a certain parameterized Halting Problem is in the parameterized complexity class XCuni.
-
a parameterized Halting Problem
The Multivariate Algorithmic Revolution and Beyond, 2012Co-Authors: Yijia Chen, Jorg FlumAbstract:The parameterized Problem $p\textsc{-Halt}$ takes as input a nondeterministic Turing machine $\mathbb{M}$ and a natural number n, the size of $\mathbb{M}$ being the parameter. It asks whether every accepting run of $\mathbb{M}$ on empty input tape takes more than n steps. This Problem is in the class XPuni , the class "uniform XP," if there is an algorithm deciding it, which for fixed machine $\mathbb{M}$ runs in time polynomial in n. It turns out that various open Problems of different areas of theoretical computer science are related or even equivalent to $p{\rm \textsc{-Halt}\in{XP}_{uni}}$. Thus this statement forms a bridge which allows to derive equivalences between statements of different areas (proof theory, complexity theory, descriptive complexity, …) which at first glance seem to be unrelated. As our presentation shows, various of these equivalences may be obtained by the same method.
-
a logic for ptime and a parameterized Halting Problem
Fields of logic and computation, 2010Co-Authors: Yijia Chen, Jorg FlumAbstract:In [9] Yuri Gurevich addresses the question whether there is a logic that captures polynomial time. He conjectures that there is no such logic. He considers a logic, we denote it by L≤, that allows to express precisely the polynomial time properties of structures; however, apparently, there is no algorithm "that given an L≤-sentence ϕ produces a polynomial time Turing machine that recognizes the class of models of ϕ." In [12] Nash, Remmel, and Vianu have raised the question whether one can prove that there is no such algorithm. They give a reformulation of this question in terms of a parameterized Halting Problem p-ACC≤ for nondeterministic Turing machines. We analyze the precise relationship between L≤ and p-ACC≤. Moreover, we show that p-ACC≤ is not fixed-parameter tractable if "P ≠ NP holds for all time constructible and increasing functions." A slightly stronger complexity theoretic hypothesis implies that L≤ does not capture polynomial time. Furthermore, we analyze the complexity of various variants of p-ACC≤ and address the construction Problem associated with p-ACC≤.
-
Fields of Logic and Computation - A logic for PTIME and a parameterized Halting Problem
2010Co-Authors: Yijia Chen, Jorg FlumAbstract:In [9] Yuri Gurevich addresses the question whether there is a logic that captures polynomial time. He conjectures that there is no such logic. He considers a logic, we denote it by L≤, that allows to express precisely the polynomial time properties of structures; however, apparently, there is no algorithm "that given an L≤-sentence ϕ produces a polynomial time Turing machine that recognizes the class of models of ϕ." In [12] Nash, Remmel, and Vianu have raised the question whether one can prove that there is no such algorithm. They give a reformulation of this question in terms of a parameterized Halting Problem p-ACC≤ for nondeterministic Turing machines. We analyze the precise relationship between L≤ and p-ACC≤. Moreover, we show that p-ACC≤ is not fixed-parameter tractable if "P ≠ NP holds for all time constructible and increasing functions." A slightly stronger complexity theoretic hypothesis implies that L≤ does not capture polynomial time. Furthermore, we analyze the complexity of various variants of p-ACC≤ and address the construction Problem associated with p-ACC≤.
-
a logic for ptime and a parameterized Halting Problem
Logic in Computer Science, 2009Co-Authors: Yijia Chen, Jorg FlumAbstract:In \cite{NasRemVia05} Nash, Remmel, and Vianu have raised the question whether a logic L_\le, already introduced by Gurevich in 1988, captures polynomial time, and they give a reformulation of this question in terms of a parameterized Halting Problem p-Acc_\le for nondeterministic Turing machines. We analyze the precise relationship between L_\le and p-Acc_\le. We show that p-Acc_\le is not fixed-parameter tractable if ``P \ne NP holds for all time constructible and increasing functions.'' Moreover, a slightly stronger complexity theoretic hypothesis implies that L_\le does not capture polynomial time. Furthermore, we analyze the complexity of various variants of p-Acc_\le and address its construction Problem.
