waashk/dblp huggingface dataset:
watson-crick d0l systems: generative power and undecidable problems. the properties of watson-crick d0l system, a language-theoretical formalism inspired by natural dna processing, are studied. the model incorporates the iterated d0l-like morphism and the dna complementarity principle represented by a letter-to-letter morphism. these two morphisms are connected by a natural condition called the trigger.we show first that this very simple model has rather unexpected power; it can closely and simply simulate any minsky register machine. as a consequence, any recursively enumerable language can be obtained as a projection of the language of some standard watson-crick d0l system. finally, we show that the graph reachability problem, equivalence problems and some other problems of standard watson-crick d0l systems are undecidable.
pert scheduling with convex cost functions. this paper deals with the problem of finding a minimum cost schedule for a set of dependent activities when a convex cost function is attached to the starting time of each activity. a first optimality necessary and sufficient condition bearing on the head and tail blocks of a schedule is first established. a second such condition that uses the spanning active equality trees of a schedule leads to design a generic algorithm for the general case. when the cost function is the usual earliness-tardiness linear function with assymetric and independent penalty coefficients, the problem is shown to be solved in o(n max{n,m}). finally, the special cases when the precedence graph is an intree or a family of chains are then also shown to be solved by efficient polynomial algorithms.
basic process algebra with deadlocking states. bisimilarity and regularity are decidable properties for the class of bpa (or context-free) processes (christensen et al., inform. and comput. 121 (1995) 143-148; burkart et al., proc. concur'96, lecture notes in computer science, vol. 1119, springer, berlin, 1996, pp. 247-262). we extend bpa with a deadlocking state obtaining bpa &dgr;systems. we show that the bpa &dgr; class is more expressive w.r.t. bisimilarity, but it remains language equivalent to bpa. we prove that bisimilarity and regularity remain decidable for bpa &dgr;. finally, we give a characterisation of those bpa&dgr; processes that can be equivalently (up to bisimilarity) described within the "pure" bpa syntax. copyright 2001 elsevier science b.v.
structural similarity within and among languages. linguists rely on intuitive conceptions of structure when comparing expressions and languages. in an algebraic presentation of a language, some natural notions of similarity can be rigorously defined (e.g. among elements of a language, equivalence w.r.t. isomorphisms of the language; and among languages, equivalence w.r.t. isomorphisms of symmetry groups), but it turns out that slightly more complex and nonstandard notions are needed to capture the kinds of comparisons linguists want to make. this paper identifies some of the important notions of structural similarity, with attention to similarity claims that are prominent in the current linguistic tradition of transformational grammar.
fast periodic correction networks. we consider the problem of sorting n-element inputs differing from already sorted sequences by t small changes. to perform this task we construct a constant depth comparator network that is applied periodically. the two constructions for this problem made, by previous authors required o(log n + t) iterations of the network. our construction requires o(log n + (log log n)2(log t)3) iterations which makes it asymptotically faster for t > log n.
formal specification and verification of the c# thread model. we present a high-level abstract state machine (asm) model of cg threads and the .net memory model. we focus on purely managed, fully portable threading features of c#. the sequential model interleaves the computation steps of the currently running threads and is suitable for uniprocessors. the parallel model addresses problems of true concurrency on multi-processor systems. the models provide a sound basis for the development of multi-threaded applications in c#. the thread and memory models complete the abstract operational semantics of c# in [börger et al. theoret. comput. sci., to appear]. the main invariants of the thread model concerning locks, monitors and mutual exclusion are formally verified in the asmtp system, an interactive proof assistant based on asm logic.
local heuristics and the emergence of spanning subgraphs in complex networks. we study the use of local heuristics to determine spanning subgraphs for use in the dissemination of information in complex networks. we introduce two different heuristics and analyze their behavior in giving rise to spanning subgraphs that perform well in terms of allowing every node of the network to be reached, of requiting relatively few messages and small node bandwidth for information dissemination, and also of stretching paths with respect to the underlying network only modestly. we contribute a detailed mathematical analysis of one of the heuristics and provide extensive simulation results on random graphs for both of them. these results indicate that, within certain limits, spanning subgraphs are indeed expected to emerge that perform well in respect to all requirements. we also discuss the spanning subgraphs' inherent resilience to failures and adaptability to topological changes.
formal analysis of pin block attacks. personal identification number (pin) blocks are 64-bit strings that encode a pin ready for encryption and secure transmission in banking networks. these networks employ tamper-proof hardware security modules (hsms) to perform sensitive cryptographic operations, such as checking the correctness of a pin typed by a customer. the use of these hsms is controlled by an api designed to enforce security. pin block attacks are unanticipated sequences of api commands which allow an attacker to determine the value of a pin in an encrypted pin block. this paper describes a framework for formal analysis of such attacks. our analysis is probabilistic, and is automated using constraint logic programming and probabilistic model checking.
on the k-path partition of graphs. the k-path partition problem is to partition a graph into the minimum number of paths, so that none of them has length more than k, for a given positive integer k. the problem is a generalization of the hamiltonian path problem and the problem of partitioning a graph into the minimum number of paths. the k-path partition problem remains np-complete on the class of chordal bipartite graphs if k is part of the input, and we show that it is np-complete on the class of comparability graphs even for k = 3. on the positive side, we present a polynomial-time solution for the problem, with any k, on bipartite permutation graphs, which form a subclass of chordal bipartite graphs.
learning algebraic structures from text. the present work investigates the learnability of classes of substructures of some algebraic structures: submonoids and subgroups of given groups, ideals of given commutative rings, subfields of given vector spaces. the learner sees all positive data but no negative one and converges to a program enumerating or computing the set to be learned. besides semantical (bc) and syntactical (ex) convergence also the more restrictive ordinal bounds on the number of mind changes are considered. the following is shown: (a) learnability depends much on the amount of semantic knowledge given at the synthesis of the learner where this knowledge is represented by programs for the algebraic operations, codes for prominent elements of the algebraic structure (like 0 and 1 fields) and certain parameters (like the dimension of finite-dimensional vector spaces). for several natural examples, good knowledge of the semantics may enable to keep ordinal mind change bounds while restricted knowledge may either allow only bc-convergence or even not permit learnability at all. (b) the class of all ideals of a recursive ring is bc-learnable iff the ring is noetherian. furthermore, one has either only a bc-learner outputting enumerable indices or one can already get an ex-learner converging to decision procedures and respecting an ordinal bound on the number of mind changes. the ring is artinian iff the ideals can be ex-learned with a constant bound on the number of mind changes, this constant is the length of the ring. ex-learnability depends not only on the ring but also on the representation of the ring. polynomial rings over the field of rationals with n variables have exactly the ordinal mind change bound in the standard representation. similar results can be established for unars. noetherian unars with one function can be learned with an ordinal mind change bound a&ohgr; for some a. copyright 2001 elsevier science b.v. all rights reserved.
learning classes of approximations to non-recursive function. blum and blum (inform. and control 28 (1975) 125-155) showed that a class b of suitable recursive approximations to the halting problem k is reliably ex-learnable but left it open whether or not b is in num. by showing b to be not in num we resolve this old problem.moreover, variants of this problem obtained by approximating any given recursively enumerable set a instead of the halting problem k are studied. all corresponding function classes u(a) are still ex-inferable but may fail to be reliably ex-learnable, for example if a is non-high and hypersimple.blum and blum (1975) considered only approximations to k defined by monotone complexity functions. we prove this condition to be necessary for making learnability independent of the underlying complexity measure. the class b of all recursive approximations to k generated by all total complexity functions is shown to be not even behaviorally correct learnable for a class of natural complexity measures. on the other hand, there are complexity measures such that b is ex-learnable. a similar result is obtained for all classes u(a).for natural complexity measures, b is shown to be not robustly learnable, but again there are complexity measures such that b and, more generally, every class u(a) is robustly ex-learnable. this result extends the criticism of jain et al. (j. comput. system sci. 62(1) (2001) 178-212), since the classes defined by artificial complexity measures turn out to be robustly learnable while those defined by natural complexity measures are not robustly learnable.
packing arrays. a packing array is a b × k array of values from a g-ary alphabet such that given any two columns, i and j, and for all ordered pairs of elements from the g-ary alphabet, (g1, g2), there is at most one row, r, such that ar,i = g1, and ar,j = g2. a central question is to determine, for given g and k, the maximum possible b. we develop general direct and recursive constructions and upper bounds on the sizes of packing arrays. we introduce the consideration of a set of disjoint rows in a packing array which allows these constructions and additionally gives a new upper bound on the size of all packing arrays. we also shove the equivalence of the problem to a matching problem on graphs and a class of resolvable pairwise balanced designs. we provide tables of the best known upper and lower bounds.
correctness of substring-preprocessing in boyer-moore's pattern matching algorithm. one of the main reasons for the high efficiency of the fast pattern matching algorithm of boyer and moore is preprocessing. the boyer-moore pattern matching algorithm utilizes two preprocessing algorithms: one on single characters and the other one on substrings. it is the latter which makes the pattern matching algorithm extremely fast (especially on natural language text). in the current paper we present a formal correctness proof of the program describing the substring-preprocessing algorithm. the proof is carried out within linear time temporal logic. during the process of our verification we found that indices of auxiliary arrays, as used in published high-level descriptions of the preprocessing algorithm, may run out of bounds. we demonstrate that this is the case and correct that undesirable aspect in the current paper.
real royal road functions for constant population size. evolutionary and genetic algorithms (eas and gas) are quite successful randomized function optimizers. this success is mainly based on the interaction of different operators like selection, mutation, and crossover. since this interaction is still not well understood, one is interested in the analysis of the single operators. jansen and wegener [proceedings of gecco'2001, 2001, pp. 375-382] have described so-called real royal road functions where simple steady-state gas have a polynomial expected optimization time while the success probability of mutation-based eas is exponentially small even after an exponential number of steps. this success of the ga is based on the crossover operator and a population whose size is moderately increasing with the dimension of the search space. here new real royal road functions are presented where crossover leads to a small optimization time, although the ga works with the smallest possible population size--namely 2.
simple and flexible detection of contiguous repeats using a suffix tree. we study the problem of detecting all occurrences of (primitive) tandem repeats and tandem arrays in a string. we first give a simple time- and space-optimal algorithm to find all tandem repeats, and then modify it to become a time and space-optimal algorithm for finding only the primitive tandem repeats. both of these algorithms are then extended to handle tandem arrays. the contribution of this paper is both pedagogical and practical, giving simple algorithms and implementations based on a suffix tree, using only standard tree traversal techniques
a proof-theoretic characterization of the basic feasible functionals. we provide a natural characterization of the type two mehlhorn-cook-urquhart basic feasible functionals as the provably total type two functionals of our (classical) applicative theory pt introduced in (inform. comput. 185 (2003) 263), thus providing a proof of a result claimed in the conclusion of strahm (2003). this further characterization of the basic feasible functionals underpins their importance as a key candidate for the notion of type two feasibility.
mell in the calculus of structures. the calculus of structures is a new proof theoretical formalism, like natural deduction, the sequent calculus and proof nets, for specifying logical systems syntactically. in a rule in the calculus of structures, the premise as well as the conclusion are structures, which are expressions that share properties of formulae and sequents. in this paper, i study a system for mell, the multiplicative exponential fragment of linear logic, in the calculus of structures. it has the following features: a local promotion rule, no non-deterministic splitting of the context in the times rule and a modular proof for the cut elimination theorem. further, derivations have a new property, called decomposition, that cannot be observed in any other known proof theoretical formalism.
the expected uncertainty of range-free localization protocols in sensor networks. we consider three range-free localization protocols for sensor networks and analyze their accuracy in terms of the expected area of uncertainty of position per sensor. assuming a small set of anchor nodes that know their position and broadcast it, we consider at first the simple intersection protocol. in this protocol a sensor assumes its position is within the part of the plane that is covered by all the broadcasts it can receive. we then extend this protocol by assuming every sensor is preloaded with the entire arrangement of anchors before being deployed. we show that in this case the same expected uncertainty can be achieved with 1/2 the anchor nodes. finally, we propose an approximation for the arrangement-based protocol which does not require any preliminary steps and prove that its expected accuracy converges to that of the arrangement protocol as the number of anchors increases.
lyndon trees. lyndon trees are introduced as a generalization of lyndon words, and the basic properties studied. a correspondence between the sets of lyndon words and lyndon trees is established. a unique factorization theorem for factoring a tree in terms of lyndon trees is proved. as an application of this result, a public key cryptosystem for trees is constructed, for which encryption and decryption are easy but cryptanalysis is hard. &mdash;authors' abstract
the bancomat problem: an example of resource allocation in a partitionable asynchronous system. a partition-aware application is an application that can make progress in multiple connected components. in this paper, we examine a particular partition-aware application to evaluate the properties provided by different partitionable group membership protocols. the application we examine is a simple resource allocation problem that we call the bancomat problem. we define a metric specific to this application, which we call the cushion, that captures the effects of the uncertainty of the global state caused from partitioning. we solve the bancomat problem using four different approaches for building partition-aware applications. we compare the approaches in terms of their cushions and discuss how well different group membership protocols support the different approaches.
cellular automata and intermediate degrees. we study a classification of cellular automata based on the turing degree of the orbits of the automaton. the difficulty of determining the membership of a cellular automaton in any one of these classes is characterized in the arithmetical hierarchy.
the size of power automata. we describe a class of simple transitive semiautomata that exhibit full exponential blowup during deterministic simulation. for arbitrary semiautomata we show that it is pspace-complete to decide whether the size of the accessible part of their power automata exceeds a given bound. we comment on the application of these results to the study of cellular automata.
the complexity of reversible cellular automata. we study the orbits of reversible one-dimensional cellular automata. it is shown that the turing degree structure of the orbits of these automata is the same as for general cellular automata. in particular there are reversible cellular automata whose orbits have arbitrary recursively enumerable degree.
ordered term tree languages which are polynomial time inductively inferable from positive data. in the fields of data mining and knowledge discovery, many semistructured data such as html/xml files are represented by rooted trees t such that all children of each internal vertex of t are ordered and t has edge labels. in order to represent structural features common to such semistructured data, we propose a linear ordered term tree, which is a rooted tree pattern consisting of ordered tree structures and internal structured variables with distinct variable labels. for a set of edge labels λ, let ottλ be the set of all linear ordered term trees. for a linear ordered term tree t in ottλ, the term tree language of t, denoted by lλ (t), is the set of all ordered trees obtained from t by substituting arbitrary ordered trees for all variables in t. given a set of ordered trees s, the minimal language problem for ottlλ = {lλ (t) | t ∈ ottλ} is to find a linear ordered term tree t in ottλ such that lλ (t) is minimal among all term tree languages which contain all ordered trees in s. we show that the class ottlλ is polynomial time inductively inferable from positive data, by giving a polynomial time algorithm for solving the minimal language problem for ottlλ.
optimal binary search trees with costs depending on the access paths. we describe algorithms for constructing optimal binary search trees, in which the access cost of a key depends on the k preceding keys which were reached in the path to it. this problem has applications to searching on secondary memory and robotics. two kinds of optimal trees are considered, namely optimal worst case trees and weighted average case trees. the time and space complexities of both algorithms are o(nk+2) and o(nk+1), respectively. the algorithms are based on a convenient decomposition and characterizations of sequences of keys which are paths of special kinds in binary search trees. finally, using generating functions, we present an exact analysis of the number of steps performed by the algorithms.
metaml and multi-stage programming with explicit annotations. we introduce metaml, a practically-motivated, statically-typed multi-stage programming language. metaml is a ``real'''' language. we have built an implementation and used it to solve multi-stage problems. % metaml allows the programmer to construct, combine, and execute code fragments in a type-safe manner. code fragments can contain free variables, but they obey the static-scoping principle. metaml performs type-checking for all stages once and for all before the execution of the first stage. % certain anomalies with our first metaml implementation has led us to formalize an illustrative subset of the metaml implementation. we present both a big-step semantics and type system for this subset, and prove the type system''s soundness with respect to a big-step semantics. from a software engineering point of view, this means that generators written in the metaml subset never generate unsafe programs. a type system and semantics for full metaml is still ongoing work. we argue that multi-stage languages are useful as programming languages in their own right, that they supply a sound basis for high-level program generation technology, and that they should support features that make it possible for programmers to write staged computations without significantly changing their normal programming style. to illustrate this we provide a simple three stage example elaborating a number of practical issues. % the design of metaml was based on two main principles that we identified as fundamental for high-level program generation, namely, cross-stage persistence and cross-stage safety. we present these principles, explain the technical problems they give rise to, and how we address with these problems in our implementation.
polynomial time learning of simple deterministic languages via queries and a representative sample. we show that simple deterministic languages are polynomial time learnable via membership queries if the learner knows a special finite set of positive examples. this finite set is called a representative sample and has been introduced by angluin inform. control 51 (1981) to show that regular languages are polynomial time learnable via membership queries. if simple deterministic languages are learnable in polynomial time via membership and equivalence queries, we can obtain a representative sample of a target language in polynomial time from a correct hypothesis. thus, our result implies that the polynomial time learning problem of simple deterministic languages via membership and equivalence queries is solvable if and only if we can find a representative sample in polynomial time via these queries. we show the learnability of simple deterministic languages by giving a learning algorithm. the algorithm, at the first stage, makes all possible candidate rules to generate the target language and a set of simple deterministic grammars which are little different each other. then, comparing them, the algorithm eliminates inappropriate rules.