waashk/dblp huggingface dataset:
weak muller acceptance conditions for tree automata. over the last decades the theory of automata on infinite objects has been an important source of tools for the specification and the verification of computer programs. trees are more suitable than words to model nondeterminism and concurrency. in the literature, there are several examples of acceptance conditions that have been proposed for automata on infinite words and then have been fruitfully extended to infinite trees. the type of acceptance condition can influence both the succinctness of the language acceptors and the computational complexity of the decision problems. here we consider, relatively to automata on infinite trees, two acceptance conditions that are obtained by a relaxation of the muller acceptance condition: the landweber and the muller-superset conditions. we prove that muller-superset tree automata accept the same class of languages as büchi tree automata. also, we show that for such languages the minimal muller-superset acceptor is at least as succinct as the minimal büchi acceptor and, in some cases, it can be exponentially more succinct. landweber tree automata, instead, define a class of languages that is not comparable with that defined by büchi tree automata. the main result we prove is that the emptiness problem for this class of automata is decidable in polynomial time, and thus we extend the class of automata with a tractable emptiness problem.
compact representations as a search strategy: compression edas. the choice of representation crucially determines the capability of search processes to find complex solutions in which many variables interact. the question is how good representations can be found and how they can be adapted online to account for what can be learned about the structure of the problem from previous samples. we address these questions in a scenario that we term indirect estimation-of-distribution: we consider a decorrelated search distribution (mutational variability) on a variable length genotype space. a one-to-one encoding onto the phenotype space then needs to induce an adapted phenotypic search distribution incorporating the dependencies between phenotypic variables that have been observed successful previously. formalizing this in the framework of estimation-of-distribution algorithms, an adapted phenotypic search distribution can be characterized as minimizing the kullback-leibler divergence (kld) to a population of previously selected samples (parents). the paper derives a relation between this kld and the description length of the encoding, stating that compact representations provide a way to minimize the divergence. a proposed class of compression evolutionary algorithms and experiments with an grammar-based compression scheme illustrate the new concept.
reducing the time complexity of testing for local threshold testability. a locally threshold testable language l is a language with the property that for some non-negative integers k and l and for some word u from l, a word v belongs to l iff: (1) the prefixes [suffixes] of length k - 1 of words u and v coincide, (2) the number of occurrences of every factor of length k in both words u and v are either the same or greater than l - 1.a deterministic finite automaton is called locally threshold testable if the automaton accepts a locally threshold testable language for some l and k.new necessary and sufficient conditions for a deterministic finite automaton to be locally threshold testable are found. on the basis of these conditions, we modify the algorithm to verify local threshold testability of the automaton, and to reduce the time complexity of the algorithm. the algorithm is implemented as a part of the c/c++ package testas. http://www.cs.biu.ac.il/ ~trakht/testas.html.
the finiteness of synchronous, tabled picture languages is decidable. in the present paper, synchronous, tabled chain code picture systems based on lindenmayer systems (stol system) are studied with respect to the finiteness of their picture languages. the finiteness is proved to be decidable. additionally, a method is given for deciding whether or not an stol system generates a finite picture language.
linear array and ring embeddings in conditional faulty hypercubes. the n-dimensional hypercube qn is a graph having 2n vertices labeled from 0 to 2n - 1. two vertices are connected by an edge if their binary labels differ in exactly one bit position. in this paper, we consider the faulty hypercube qn with n ≥ 3 that each vertex of qn is incident to at least two nonfaulty edges. based on this requirement, we prove that qn contains a hamiltonian path joining any two different colored vertices even if it has up to 2n - 5 edge faults, moreover, we show that there exists a path of length 2n - 2 between any two the same colored vertices in this faulty qn. furthermore, we also prove that the faulty qn still contains a cycle of every even length from 4 to 2n inclusive.
new bounds for multi-label interval routing. interval routing (ir) is a space-efficient routing method for computer networks. for longest routing path analysis, researchers have focused on lower bounds for many years. for any n-node graph g of diameter d, there exists an upper bound of 2d for ir using one or more labels, and an upper bound of ⌈3/2d⌉ for ir using o(√nlogn) or more labels. we present two upper bounds in the first part of the paper. we show that for every integer i > 0, every n-node graph of diameter d has a k-dominating set of size o(i+1√n) for k ≤ (1 - 1/3i)d. this result implies a new upper bound of ⌈(2 - 1/3i)d⌉ for ir using o(i+1√n) or more labels, where i is any positive integer constant. we apply the result by kutten and peleg [7] to achieve an upper bound of (1 + α)d for ir using o(n/d) or more labels, where α is any constant in (0, 1). the second part of the paper offers some lower bounds for planar graphs. for any m-label interval routing scheme (m-irs), where m = o(3√n), we derive a lower bound of [(2m + 1)/(2m)]d - 1 on the longest path for m = o(√n), and a lower bound of [(2(1 + δ)m + 1)/(2(1 + δ)m)]d, where δ ∈ (0, 1], for m = o(√n). the latter result implies a lower bound of ω(√n) on the number of labels needed to achieve optimality.
real number computation through gray code embedding. we propose an embedding g of the unit open interval to the set {0, 1}⊥,1ω of infinite sequences of {0, 1} with at most one undefined element. this embedding is based on gray code and it is a topological embedding with a natural topology on {0, 1}⊥,1ω. we also define a machine called an indeterministic multihead type 2 machine which input/output sequences in {0, 1}ω⊥,1, and show that the computability notion induced on real functions through the embedding g is equivalent to the one induced by the signed digit representation and type 2 machines. we also show that basic algorithms can be expressed naturally with respect to this embedding.
a domain-theoretic semantics of lax generic functions. the semantic structure of a polymorphic calculus λm is studied. λm is defined over a hierarchical type structure, and a function in this calculus, called a generic function, can be composed from more than one lambda expression and the ways it behaves on each type are weakly related in that it lax commutes with the coercion functions defined from the subtypes to the supertypes.since laxness is intermediate between ad hocness (behaviors on each type are not related) and coherency (commuting with the coercion functions), λm has syntactic properties lying between those of calculi with ad hoc generic functions and coherent generic functions studied in tsuiki (math. struct. comput. sci. 8 (1998) 321). that is, although λm allows self application and thus is not normalizing, it does not have any unsolvable terms. for this reason, all the semantic domains are connected by mutually recursive equations and, at the same time, they do not have the least elements. we solve them by considering fibrations and expressing the equations as a recursive equation about fibrations. we also show the adequacy theorem for λm following the construction of pitts and use it to derive some syntactic properties.
computing phylogenetic roots with bounded degrees and errors is np-complete. in this paper we study the computational complexity of the following optimization problem: given a graph g = (v, e), we wish to find a tree t such that (1) the degree of each internal node of t is at least 3 and at most δ, (2) the leaves of t are exactly the elements of v, and (3) the number of errors, that is, the symmetric difference between e and {{u, v} : u, v are leaves of t and dt (u, v) ≤ k}, is as small as possible, where dt (u, v) denotes the distance between u and v in tree t. we show that this problem is np-hard for all fixed constants δ, k ≥ 3.let sδ(k) be the size of the largest clique for which an error-free tree t exists. in the course of our proof, we will determine all trees (possibly with degree 2 nodes) that approximate the (sδ(k) - 1)-clique by errors at most 2.
sequencing by hybridization with errors: handling longer sequences. sequencing by hybridization (sbh) is a method for reconstructing a dna sequence given the set of all subsequences of length k of the target sequence. this set, called the spectrum of the sequence, can be obtained from hybridization with a universal dna chip. however, the hybridization experiments are error prone, so this leads to the computational problem of reconstructing a sequence from a noisy spectrum. halperin et al. gave an algorithm for this problem with provable performance in the presence of both false positive and false negative errors. assuming, for example, that the false positive rate is small, and the probability of false negative is 0.1, the algorithm can reconstruct a random sequence of length o(20.7k) with an arbitrary small probability of failure. in this paper, we give an algorithm that can reconstruct longer sequences: under the assumptions above, our algorithm can reconstruct sequences of length o(20.942k). this bound is almost optimal as the bound for the errorless case is θ(2k).
type inference for set theory. weak set theories are employed for set-theoretic specification. we develop and explore type inference systems for such set theories.
residue polynomial systems. in this paper, we present the basic ideas of the residue polynomial system (rps), a polynomial analog of the familiar residue number systems (rns) of integer arithmetic. many of the properties of the rns are shared by the rps. the main exception is that division of polynomials in the rps is much more tractable than its integer counterpart. examples are included throughout. the underlying field of coefficients for polynomials under consideration can be the reals or the rationals, though extension to the complex field will be needed for division by irreducible quadratic factors.
investigations on the dual calculus. the dual calculus, proposed recently by wadler, is the outcome of two distinct lines of research in theoretical computer science: (a) efforts to extend the curry-howard isomorphism, established between the simply-typed lambda calculus and intuitionistic logic, to classical logic. (b) efforts to establish the tacit conjecture that call-by-value (cbv) reduction in lambda calculus is dual to call-by-name (cbn) reduction.this paper initially investigates relations of the dual calculus to other calculi, namely the simply-typed lambda calculus and the symmetric lambda calculus. moreover, church-rosser and strong normalization properties are proven for the calculus' cbv reduction relation. finally, extensions of the calculus to second-order types are briefly introduced.
a computable version of the daniell-stone theorem on integration and linear functionals. for every measure µ, the integral i: f ↦ ∫ f dµ is a linear functional on the set of real measurable functions. by the daniell-stone theorem, for every abstract integral λ: f → r on a stone vector lattice f of real functions f: ω → r there is a measure µ such that ∫ f dµ = λ(f) for all f ∈ f. in this paper we prove a computable version of this theorem.
approximate string matching with q-grams and maximal matches. we study approximate string matching in connection with two string distance functions that are computable in linear time. the first function is based on the so-called $q$-grams. an algorithm is given for the associated string matching problem that finds the locally best approximate occurences of pattern $p$, $|p|=m$, in text $t$, $|t|=n$, in time $o(n\log (m-q))$. the occurences with distance $\leq k$ can be found in time $o(n\log k)$. the other distance function is based on finding maximal common substrings and allows a form of approximate string matching in time $o(n)$. both distances give a lower bound for the edit distance (in the unit cost model), which leads to fast hybrid algorithms for the edit distance based string matching.
on the relationship between combinatorial and lp-based lower bounds for np-hard scheduling problems. enumerative approaches to solving optimization problems, such as branch and bound, require a subroutine that produces a lower bound on the value of the optimal solution. in the domain of scheduling problems the requisite lower bound has typically been derived from either the solution to a linear-programming (lp) relaxation of the problem or the solution to a combinatorial relaxation. in this paper we investigate, from a theoretical perspective, the relationship between several lp-based lower bounds and combinatorial lower bounds for three scheduling problems in which the goal is to minimize the average weighted completion time of the jobs scheduled.we establish a number of facts about the relationship between these different sorts of lower bounds, including the equivalence of certain lp-based lower bounds for these problems to combinatorial lower bounds used in successful branch-and-bound algorithms. as a result, we obtain the first worst-case analysis of the quality of the lower bounds delivered by these combinatorial relaxations.
nominal unification. we present a generalisation of first-order unification to the practically important case of equations between terms involving binding operations. a substitution of terms for variables solves such an equation if it makes the equated terms α-equivalent, i.e. equal up to renaming bound names. for the applications we have in mind, we must consider the simple, textual form of substitution in which names occurring in terms may be captured within the scope of binders upon substitution. we are able to take a "nominal" approach to binding in which bound entities are explicitly named (rather than using nameless, de bruijn-style representations) and yet get a version of this form of substitution that respects α-equivalence and possesses good algorithmic properties. we achieve this by adapting two existing ideas. the first one is terms involving explicit substitutions of names for names, except that here we only use explicit permutations (bijective substitutions). the second one is that the unification algorithm should solve not only equational problems, but also problems about the freshness of names for terms. there is a simple generalisation of classical first-order unification problems to this setting which retains the latter's pleasant properties: unification problems involving α-equivalence and freshness are decidable; and solvable problems possess most general solutions.
sound generalizations in mathematical induction. many proofs by induction diverge without a suitable generalization of the goal to be proved.the aim of the present paper is to propose a method that automatically finds a generalized form of the goal before the induction sub-goals are generated and failure begins. the method works in the case of monomorphic theories (see section 1). however, in contrast to all heuristic-based methods, our generalization method is sound: a goal is an inductive theorem if and only if its generalization is an inductive theorem. as far as we know this is the first approach that proposes sound generalizations for mathematical induction.
least and greatest fixed points in intuitionistic natural deduction. this paper is a comparative study of a number of (intensional-semantically distinct) least and greatest fixed point operators that natural-deduction proof systems for intuitionistic logics can be extended with in a proof-theoretically defendable way. eight pairs of such operators are analysed. the exposition is centred around a cube-shaped classification where each node stands for an axiomatization of one pair of operators as logical constants by intended proof and reduction rules and each arc for a proof- and reduction-preserving encoding of one pair in terms of another. the three dimensions of the cube reflect three orthogonal binary options: conventional-style vs. mendler-style, basic ("[co]iterative") vs. enhanced ("primitive-[co]recursive"), simple vs. course-of-value [co]induction. some of the axiomatizations and encodings are well known; others, however, are novel; the classification into a cube is also new. the differences between the least fixed point operators considered are illustrated on the example of the corresponding natural number types.
term rewriting restricted to ground terms. we study rewriting of ground terms. for an arbitrary term rewrite system r over a ranked alphabet σ, we restrict the rewriting relation →r to ground terms. we introduce the relation →r,g = →r ∩(tς × tς). we show that ↔r,g* = ↔r* ∩(tς × tς). we show that for a given term rewrite system r and a given ground term rewrite system s over a ranked alphabet σ it is decidable if ↔r,g* ⊆ ↔s* we show that for a given left-linear right-ground term rewrite system r over a ranked alphabet ∑ it is decidable if there is a ground term rewrite system s over σ such that →r,g* = →s*.
intersection of finitely generated congruences over term algebra. we show that it is decidable for any given ground term rewrite systems r and s if there is a ground term rewrite system u such that ↔u* = ↔r* ∩ ↔s*. if the answer is yes, then we can effectively construct such a ground term rewrite system u. in other words, for any given finitely generated congruences ρ and τ over the term algebra, it is decidable if ρ ∩ τ is a finitely generated congruence. if the answer is yes, then we can effectively construct a ground term rewrite system u such that ↔u* = ρ ∩ τ.
right-linear half-monadic term rewrite systems. we show that termination and convergence are decidable properties for right-linear half-monadic term rewrite systems.
a loopless algorithm for generating the permutations of a multiset. many combinatorial structures can be constructed from simpler components. for example, a permutation can be constructed from cycles, or a motzkin word from a dyck word and a combination. in this paper we present a constructor for combinatorial structures, called shuffle on trajectories (defined previously in a non-combinatorial context), and we show how this constructor enables us to obtain a new loopless generating algorithm for multiset permutations from similar results for simpler objects.
decidability of infinite-state timed ccp processes and first-order ltl. the ntcc process calculus is a timed concurrent constraint programming (ccp) model equipped with a first-order linear-temporal logic (ltl) for expressing process specifications. a typical behavioral observation in ccp is the strongest postcondition (sp). the ntcc sp denotes the set of all infinite output sequences that a given process can exhibit. the verification problem is then whether the sequences in the sp of a given process satisfy a given ntcc ltl formula.this paper presents new positive decidability results for timed ccp as well as for ltl. in particular, we shall prove that the following problems are decidable: (1) the sp equivalence for the so-called locally-independent ntcc fragment; unlike other fragments for which similar results have been published, this fragment can specify infinite-state systems, (2) verification for locally-independent processes and negation-free first-order formulae of the ntcc ltl, (3) implication for such formulae, (4) satisfiability for a first-order fragment of manna and pnueli's ltl. the purpose of the last result is to illustrate the applicability of ccp to well-established formalisms for concurrency.
expressiveness of matchgates. matchgates have been used to simulate classically in polynomial time assemblies of quantum gates. in this paper it is shown that every matchgate for 2-input 2-output functions has to obey a certain set of five polynomial identities. it is also shown that no matchgate can realize a nontrivial control gate for any number of inputs. on the other hand, it is proved that classical boolean formulae can be expressed as matchcircuits of polynomial size.
dynamical analysis of a class of euclidean algorithms. we develop a general framework for the analysis of algorithms of a broad euclidean type. the average-case complexity of an algorithm is seen to be related to the analytic behaviour in the complex plane of the set of elementary transformations determined by the algorithm. the methods rely on properties of transfer operators suitably adapted from dynamical systems theory. as a consequence, we obtain precise average-case analyses of algorithms for evaluating the jacobi symbol of computational number theory fame, thereby solving conjectures of bach and shallit. these methods also provide a unifying framework for the analysis of an entire class of gcd-like algorithms together with new results regarding the probable behaviour of their cost functions.
probabilistic event structures and domains. this paper studies how to adjoin probability to event structures, leading to the model of probabilistic event structures. in their simplest form, probabilistic choice is localised to cells, where conflict arises; in which case probabilistic independence coincides with causal independence. an event structure is associated with a domain--that of its configurations ordered by inclusion. in domain theory, probabilistic processes are denoted by continuous valuations on a domain. a key result of this paper is a representation theorem showing how continuous valuations on the domain of a confusion-free event structure correspond to the probabilistic event structures it supports. we explore how to extend probability to event structures which are not confusion-free via two notions of probabilistic runs of a general event structure. finally, we show how probabilistic correlation and probabilistic event structures with confusion can arise from event structures which are originally confusion-free by using morphisms to rename and hide events.