waashk/dblp huggingface dataset:
modular verification of multithreaded programs. multithreaded software systems are prone to errors due to the difficulty of reasoning about multiple interleaved threads operating on shared data. static checkers that analyze a program's behavior over all execution paths and all thread interleavings are a powerful approach to identifying bugs in such systems. in this paper, we present calvin, a scalable and expressive static checker for multithreaded programs based on automatic theorem proving. to handle realistic programs, calvin performs modular checking of each procedure called by a thread using specifications of other procedures and other threads. our experience applying calvin to several real-world programs indicates that calvin has a moderate annotation overhead and can catch common defects in multithreaded programs, such as synchronization errors and violations of data invariants.
results related to threshold phenomena research in satisfiability: lower bounds. we present a history of results related to the threhold phenomena which arise in the study of random conjunctive normal form (cnf) formulas. in a companion paper (d. achlioptas, theoret. comput. sci., this volume) the major ideas used to achieve many of the lower bounds results on the location of the threshold are described in an informal, intuitive manner.
efficient algorithms for robustness in resource allocation and scheduling problems. the robustness function of an optimization (minimization) problem measures the maximum increase in the value of its optimal solution that can be produced by spending a given amount of resources increasing the values of the elements in its input. we present efficient algorithms for computing the robustness function of resource allocation and scheduling problems that can be modeled with partition and scheduling matroids. for the case of scheduling matroids, we give an o(m2n2) time algorithm for computing a complete description of the robustness function, where m is the number of elements in the matroid and n is its rank. for partition matroids, we give two algorithms: one that computes the complete robustness function in o(m log m) time, and other that optimally evaluates the robustness function at only a specified point.
sequential and indexed two-dimensional combinatorial template matching allowing rotations. we present new and faster algorithms to search for a two-dimensional pattern in a two-dimensional text allowing any rotation of the pattern. this has applications such as image databases and computational biology. we consider the cases of exact and approximate matching under several matching models, using a combinatorial approach that generalizes string matching techniques. we focus on sequential algorithms, where only the pattern can be preprocessed, as well as on indexed algorithms, where the text is preprocessed and an index built on it. on sequential searching we derive average-case lower bounds and then obtain optimal average-case algorithms for all the matching models. at the same time, these algorithms are worst-case optimal. on indexed searching we obtain search time polylogarithmic on the text size, as well as sublinear time in general for approximate searching.
computationally universal p systems without priorities: two catalysts are sufficient. the original model of p systems with symbol objects introduced by paun was shown to be computationally universal, provided that catalysts and priorities of rules are used. by reduction via register machines sosík and freund proved that the priorities may be omitted from the model without loss of computational power. freund, oswald, and sosík considered several variants of p systems with catalysts (but without priorities) and investigated the number of catalysts needed for these specific variants to be computationally universal. it was shown that for the classic model of p systems with the minimal number of two membranes the number of catalysts can be reduced from six to five; using the idea of final states the number of catalysts could even be reduced to four. in this paper we are able to reduce the number of catalysts again: two catalysts are already sufficient. for extended p systems we even need only one membrane and two catalysts. for the (purely) catalytic systems considered by ibarra only three catalysts are already enough.
from regulated rewriting to computing with membranes: collapsing hierarchies. in addressing certain problems about membrane computing, a recent and active branch of natural computing, it first was necessary to address certain problems from the area of regulated rewriting. thus, the present paper is a contribution to both these domains.a central problem in membrane computing is that of the hierarchy with respect to the number of membranes: are systems with n + 1 membranes more powerful than systems with n membranes? does the number of membranes induce an infinite hierarchy of the computed functions? usually, when proving the universality of membrane systems (also called p systems), one starts from a matrix grammar and the number of membranes depends on the number of non-terminal symbols used by this grammar in the so-called appearance checking mode. we first prove that recursively enumerable languages can be generated by matrix grammars with only two non-terminal symbols being used in the appearance checking mode. the proofs of this fact and of several related results are based on a simulation of register machines by means of graph-controlled grammars.then, we consider three classes of membrane systems, and in all the three cases the hierarchies with respect to the number of membranes are shown to collapse at level four: systems with four membranes are computationally universal (but we do not know whether or not this result is optimal).
tissue p systems with channel states. we consider tissue-like p systems with states associated with the links (we call them synapses) between cells, controlling the passage of objects across the links. we investigate the computing power of such devices for the case of using--in a sequential manner--antiport rules of small weights. systems with two cells are proved to be universal when having arbitrarily many states and minimal antiport rules, or one state and antiport rules of weight two. also the systems with arbitrarily many cells, three states, and minimal antiport rules are universal. in contrast, the systems with one cell and any number of states and rules of any weight only compute parikh sets of matrix languages (generated by matrix grammars without appearance checking); characterizations of parikh images of matrix languages are obtained for such one-cell systems with antiport rules of a reduced weight.
satisfying subtype inequalities in polynomial space. this paper studies the complexity of type inference in &lgr;-calculus with subtyping. infering types is equivalent to solving systems of subtype inequalities. these inequalities are solved over simple types ordered structurally from an arbitrary set of base subtype assumptions. in this case, we give a new pspace upper bound. together with the previously known lower bound, this result settles completely the complexity of the problem, which is pspace-complete. we use a technique of independent theoretical interest that simplifies existing methods developed in the literature. finally, we show how our polynomial space algorithm, although mainly theoretical, can lead to a slight practical improvement of existing implementations. copyright 2002 elsevier science b.v.
finite-state transducer cascades to extract named entities in texts. a lot of named entity extraction systems were created in english thanks to the impulse of muc conferences. this article describes a finite-state transducer cascade for the extraction of named entities in french journalistic texts. finite-state cascades are widely used for natural language processing: a cascade is a series of finite-state transducers applied to a text transforming it. such transducer cascades allow implementation of syntactic analysis, translation memory and information extraction. we present our general system named cassys: this system uses the intex natural language processing features to realize a transducer cascade. cassys is not dedicated to the extraction of named entity; we use it for this task but thanks to intex, it allows syntactic analyses, information extraction or other tasks.
arithmetical complexity of symmetric d0l words. we characterize and count words which occur in arithmetical subsequences of fixed points of symmetric morphisms.
sequences of linear arithmetical complexity. arithmetical complexity of infinite sequences is the number of all words of a given length whose symbols occur in the sequence at positions which constitute arithmetical progressions. we show that uniformly recurrent sequences whose arithmetical complexity grows linearly are precisely toeplitz words of a specific form.
data structures and algorithms for tilings i. based on the mathematical theory of delaney symbols, data structures and algorithms are presented for the analysis and manipulation of generalized periodic tilings in arbitrary dimensions.
a modal proof theory for final polynomial coalgebras. an infinitary proof theory is developed for modal logics whose models are coalgebras of polynomial functors on the category of sets. the canonical model method from modal logic is adapted to construct a final coalgebra for any polynomial functor. the states of this final coalgebra are certain "maximal" sets of formulas that have natural syntactic closure properties.the syntax of these logics extends that of previously developed modal languages for polynomial coalgebras by adding formulas that express the "termination" of certain functions induced by transition paths. a completeness theorem is proven for the logic of functors which have the lindenbaum property that every consistent set of formulas has a maximal extension. this property is shown to hold if the deducibility relation is generated by countably many inference rules.a counter-example to completeness is also given. this is a polynomial functor that is not lindenbaum: it has an uncountable set of formulas that is deductively consistent but has no maximal extension and is unsatisfiable, even though all of its countable subsets are satisfiable.
direct constructions of universal extended h systems. a direct universal extended h system receives as input the coding of an extended h system with a particular control mechanism and simulates it. we present a direct construction for five kinds of control for the extended h systems under consideration. it is the first time that a direct construction is described: universal results obtained until now were based on the simulation of universal type-0 grammars or turing machine.
the conformon-p system: a molecular and cell biology-inspired computability model. a new theoretical computational model, called conformon-p system, based on simple and basic concepts inspired from a theoretical model of the living cell and membrane computing is presented.the computational power of it and of some natural variants are studied.links with petri nets, reversible computation, other interpretations and variants of the model are briefly outlined.
hypothesis finding with proof theoretical appropriateness criteria. for two given formulae b and e with b≠e hypothesis finding means to produce a formula s such that b ∨ s ?? c. hypothesis finding, or variants thereof, is central to various types of inference, e.g., abductive inference, inductive inference, machine learning, and machine discovery. clarifying the nature of hypothesis finding is still in its infancy, a situation similar to the establishment of logical foundations of inference related to induction and discovery. although trivial solutions to hypothesis finding are easy to give, finding appropriate hypotheses still remains as a great challenge. a central role in this context plays the question, what it means for a hypothesis to be appropriate? in this paper we propose an answer to this question, which is based on proof theoretical criteria. this is in contrast to most previous approaches where appropriateness of hypotheses was based on concepts of semantical weakness in classical logic. more precisely, we use provability in relevance logic instead of classical semantical entailment, we demand utmost exploitation of the inferential potential (deductive content) inherent in b → c and we demand s to be a minimal deductive supplement to b → c. along these lines we developed the concept of a minimized residue hypothesis which also constitutes an interesting trade-off between 'logical smallness' and 'syntactical smallness'.
an introduction to periodical discrete sets from a tomographical perspective. in this paper we introduce a new class of binary matrices whose entries show periodical configurations, and we furnish a first approach to their analysis from a tomographical point of view. in particular we propose a polynomial-time algorithm for reconstructing matrices with a special periodical behavior from their horizontal and vertical projections. we succeeded in our aim by using a reduction involving polyominoes which can be characterized by means of 2 - sat formulas.
the np-completeness of a tomographical problem on bicolored domino tilings. in this paper we study the problem of reconstructing a bicolored domino tiling of a rectangular surface from its horizontal and vertical projections. we use a reduction from the np-complete problem numerical matching with target sums in order to prove that, unless p = np, this task cannot be performed in polynomial time. the reconstruction of monochromatic domino tilings is still open.
on-line digit set conversion in real base. let β be a real number > 1. the digit set conversion between real numbers represented in fixed base β is shown to be computable by an on-line algorithm, and thus is a continuous function. when β is a pisot number the digit set conversion is computable by an on-line finite automaton.
additive and multiplicative properties of point sets based on beta-integers. to each number β > 1 correspond abelian groups in rd, of the form λβ = σi=1d zβei, which obey βλβ ⊂ λβ. the set zβ of beta-integers is a countable set of numbers: it is precisely the set of real numbers which are polynomial in β when they are written in "basis β", and zβ = z when β ∈ n. we prove here a list of arithmetic properties of zβ: addition, multiplication, relation with integers, when β is a quadratic pisot-vijayaraghavan unit (quasicrystallographic inflation factors are particular examples). we also consider the case of a cubic pisot-vijayaraghavan unit associated with the seven-fold cyclotomic ring. at the end, we show how the point sets λβ are vertices of d-dimensional tilings.
conversation protocols: a formalism for specification and verification of reactive electronic services. this paper focuses on the realizability problem of a framework for modeling and specifying the global behaviors of reactive electronic services (e-services). in this framework, web accessible programs (peers) communicate by asynchronous message passing, and a virtual global watcher silently listens to the network. the global behavior is characterized by a "conversation", which is the infinite sequence of messages observed by the watcher. we show that given a büchi automaton specifying the desired set of conversations, called a "conversation protocol", it is possible to realize the protocol using a set of finite state peers if three realizability conditions are satisfied. in particular, the synthesized peers will conform to the protocol by generating only those conversations specified by the protocol. our results enable a top-down verification strategy where (1) a conversation protocol is specified by a realizable büchi automaton, (2) the properties of the protocol are verified on the büchi automaton specification, and (3) the peer implementations are synthesized from the protocol via projection.
tau laws for pi calculus. the paper investigates the nonsymbolic algebraic semantics of the weak bisimulation congruences on finite pi processes. the weak bisimulation congruences are studied both in the absence and in the presence of the mismatch operator. some interesting phenomena about the open congruences are revealed. several new tau laws are discovered and their relationship is discussed. the contributions of the paper are mainly as follows: 1. it is proved that milner's three tau laws fail to lift a complete system for the strong open congruence to a complete system for the weak open congruence in the absence of both the mismatch operator and the restriction operator. a fourth tau law is proposed to deal with the match operator under the prefix operation. it is shown that for this calculus a complete system for the strong open congruence extended with all the four tau laws is complete for the weak open congruence. 2. it is verified that the four tau laws are also enough for the weak open congruence of the pi calculus without the mismatch operator. a complete system using distinctions is given. 3. it is pointed out that the standard definition of the weak open congruence gives rise to a bad equivalence relation in the presence of the mismatch operator. two alternatives are proposed. these are the late open congruence and the early open congruence. their difference is similar to that between the weak late congruence and the weak early congruence. complete axiomatic systems for the two weak open congruences are given.
online matching on a line. given a set s ⊆ r of points on the line, we consider the task of matching a sequence (r1, r1,... ) of requests in r to points in s. it has been conjectured [online algorithms: the state of the art, lecture notes in computer science, vol. 1442, springer, berlin, 1998, pp. 268-280] that there exists a 9-competitive online algorithm for this problem, similar to the so-called "cow path" problem [inform. and comput. 106 (1993) 234-252]. we disprove this conjecture and show that no online algorithm can achieve a competitive ratio strictly less than 9.001.our argument is based on a new proof for the optimality of the competitive ratio 9 for the "cow path" problem.
time-minimal paths amidst moving obstacles in three dimensions. a path-planning problem is considered in the presence of moving polygonal obstacles in three dimensions. a particle is to be moved from a given initial position to a destination position amidst polygonal disjoint barriers moving along known linear trajectories. the particle can move in any direction in space with a single constraint that it cannot move faster than a given speed bound. all obstacles are slowly moving, i.e., their speeds are strictly slower than the maximum speed of the particle. the destination point is also permitted to move along a known trajectory and is assumed to be collision-free at all times. three properties are stated and proved for a time-minimal path amidst moving polygonal barriers. a few extensions are considered, including piecewise linear motions of the obstacle
two-dimensional on-line bin packing problem with rotatable items. in this paper, we consider a two-dimensional version of the on-line bin packing problem, in which each rectangular item that should be packed into unit square bins is "rotatable" by 90°. two on-line algorithms for solving the problem are proposed. the second algorithm is an extension of the first algorithms, and the worst-case ratio of the second one is at least 2.25 and at most 2.565.
notes on acyclic orientations and the shelling lemma. in this paper we study two lemmas on acyclic orientations and totally cyclic orientations of a graph, which can be derived from the shelling lemma in vector subspaces. we give simple graph theoretical proofs as well as a proof by the interpretations of the shelling lemma in the special setting of graphs. furthermore, we present similar interpretations of closely related theorems in vector subspaces, which do not seem to admit simple graph theoretical proofs.
a nim game played on graphs. we propose a new impartial game played by two players, which can be compared to the well-known nim game (winning ways for your mathematical plays, academic press, new york, 1982; on numbers and games, academic press, london and new york, 1976; combinatorial games: back and front, springer, tokyo, 1989) played on graphs. in this paper, we consider this game and investigate its winning strategies. in the proof, menger's theorem (graph theory, an introductory course, springer, new york, 1979) noted in graph theory plays a crucial role.
a nim game played on graphs ii. we consider a nim game played on graphs, which was proposed and was named nim on graphs in [4], and investigate its grundy number using matchings of graphs. especially, by virtue of this investigation, we can find the grundy number of nim on trees completely. another result is that the problem of finding the grundy number of nim on cycles is resolved into that of nim on trees. thus, we find also the grundy number of nim on cycles completely.
shape preserving top-down tree transducers. as top-down tree transducers generalize generalized sequential machines, shape preserving top-down tree transducers naturally generalize length preserving generalized sequential machines. for instance, top-down relabeling tree transducers are shape preserving top-down tree transducers. we show that a top-down tree transducer is shape preserving if and only if it is equivalent to a top-down relabeling tree transducer. we also prove that it is decidable if a top-down tree transducer is shape preserving.
hierarchies of tree series transformations. we study bottom-up and top-down tree series transducers over a semiring a and denote the tree series transformation classes computed by them by bott-ts(a) and topt-ts(a), respectively. we present the inclusion diagram of the classes p-bott-tsn(a), p-topt-tsn(a), p-botn+1t-ts(a), and p-topn+1t-ts(a) and prove its correctness, where a is a commutative izz-semiring (izz=idempotent, zero-divisor free, and zero-sum free) and the prefix p stands for polynomial. this inclusion diagram implies the properness of the following four hierarchies: p, topt-ts(a) ⊆ p-top2t-ts(a) ⊆ p-top3t-ts(a) ⊆ ..., p, bott-ts(a) ⊆ p-bot2t-ts(a) ⊆ p-bot3t-ts(a) ⊆ ..., p, topt-ts(a) ⊆ p-bot2t-ts(a) ⊆ p-top3t-ts(a) ⊆ p-bot4t-ts(a) ⊆ ..., p, bott-ts(a) ⊆ p-top2t-ts(a) ⊆ p-bot3t-ts(a) ⊆ p-top4t-ts(a) ⊆ ..., where the first hierarchy generalizes the famous top-down tree transformation hierarchy of engelfriet (math. systems theory 15 (1982) 92-125). as the second main result we prove that the first two hierarchies are proper even for arbitrary (i.e., not necessarily commutative) izz-semirings.
linear deterministic multi bottom-up tree transducers. in general, top-down and bottom-up tree transducers lead to incomparable classes of tree transformations, both for the nondeterministic and the deterministic case. if deterministic top-down tree transducers are extended by the capability to recognize regular tree properties and deterministic bottom-up tree transducers are generalized by allowing states with arbitrary finite rank, then the two devices, now called deterministic top-down tree transducers with regular look-ahead and deterministic multi bottom-up tree transducers, respectively, become equivalent [z. fülöp, a. kühnemann, h. vogler, a bottom-up characterization of deterministic top-down tree transducers with regular look-ahead, inform. process. lett. 91 (2004) 57-67].in this paper we focus on the class ld-mbot of tree transformations which are computed by linear deterministic multi bottom-up tree transducers. we investigate the relationship among ld-mbot and the classes of tree transformations computed by (restricted) deterministic bottom-up tree transducers and by (restricted) deterministic top-down tree transducers with regular look-ahead. in fact, we show the inclusion diagram of nine such classes.