Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn the complexity of the correctness problem for non-zeroness test instruction sequences
298
0
0.0
(
0
)
Added by
Kees Middelburg
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
This paper concerns the question to what extent it can be efficiently determined whether an arbitrary program correctly solves a given problem. This question is investigated with programs of a very simple form, namely instruction sequences, and a very simple problem, namely the non-zeroness test on natural numbers. The instruction sequences concerned are of a kind by which, for each $n > 0$, each function from ${0,1}^n$ to ${0,1}$ can be computed. The established results include the time complexities of the problem of determining whether an arbitrary instruction sequence correctly implements the restriction to ${0,1}^n$ of the function from ${0,1}^*$ to ${0,1}$ that models the non-zeroness test function, for $n > 0$, under several restrictions on the arbitrary instruction sequence.
rate research
Read More
We develop theory concerning non-uniform complexity in a setting in which the notion of single-pass instruction sequence considered in program algebra is the central notion. We define counterparts of the complexity classes P/poly and NP/poly and formulate a counterpart of the complexity theoretic conjecture that NP is not included in P/poly. In addition, we define a notion of completeness for the counterpart of NP/poly using a non-uniform reducibility relation and formulate complexity hypotheses which concern restrictions on the instruction sequences used for computation. We think that the theory developed opens up an additional way of investigating issues concerning non-uniform complexity.
We show that there are $Sigma_3^0$-complete languages of infinite words accepted by non-deterministic Petri nets with Buchi acceptance condition, or equivalently by Buchi blind counter automata. This shows that omega-languages accepted by non-deterministic Petri nets are topologically more complex than those accepted by deterministic Petri nets.
Satisfiability Modulo Theories (SMT) and SAT solvers are critical components in many formal software tools, primarily due to the fact that they are able to easily solve logical problem instances with millions of variables and clauses. This efficiency of solvers is in surprising contrast to the traditional complexity theory position that the problems that these solvers address are believed to be hard in the worst case. In an attempt to resolve this apparent discrepancy between theory and practice, theorists have proposed the study of these solvers as proof systems that would enable establishing appropriate lower and upper bounds on their complexity. For example, in recent years it has been shown that (idealized models of) SAT solvers are polynomially equivalent to the general resolution proof system for propositional logic, and SMT solvers that use the CDCL(T) architecture are polynomially equivalent to the Res*(T) proof system. In this paper, we extend this program to the MCSAT approach for SMT solving by showing that the MCSAT architecture is polynomially equivalent to the Res*(T) proof system. Thus, we establish an equivalence between CDCL(T) and MCSAT from a proof-complexity theoretic point of view. This is a first and essential step towards a richer theory that may help (parametrically) characterize the kinds of formulas for which MCSAT-based SMT solvers can perform well.
Every partial function from bit strings of a given length to bit strings of a possibly different given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We look for an equivalence relation on instruction sequences of this kind that captures to a reasonable degree the intuitive notion that two instruction sequences express the same algorithm.
This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. Fixing values for all parameters yields MDPs. In particular, this paper studies the complexity of finding values for these parameters such that the induced MDP satisfies some reachability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably provide ETR-completeness results for distinct variants of this problem. Furthermore, we provide insights in the functions describing the induced reachability probabilities, and how pMDPs generalise concurrent stochastic reachability games.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
