waashk/acm huggingface dataset:
shape analysis for mobile ambients  the ambient calculus is a calculus of computation that allows active processes to move between sites. we present an analysis inspired by state-of-the-art pointer analyses that safety and accurately predicts which processes may turn up at what sites during the execution of a composite system. the analysis models sets of processes by sets of regular tree grammars enhanced with context-dependent counts, and it obtains its precision by combining a powerful redex materialisation with a strong redex reduction (in the manner of the strong updates performed in pointer analyses). the underlying ideas are flexible and scale up to general tree structures admitting powerful restructuring operations.  hanne riis nielson flemming nielson
bisimulation through probabilistic testing (preliminary report)  we propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. by using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm with a probability arbitrary close to 1 can distinguish processes that are not bisimulation equivalent. we also show a similar result (in a slightly stronger form) for a new process relation called 2/3-bisimulation --- lying strictly between that of simulation and bisimulation. finally, the ultimately strength of the testing language is shown to identify an even stronger process relation, called probabilistic bisimulation.  k. g. larsen a. skou
one-way functions and pseudorandom generators  one-way are those functions which are easy to compute, but hard to invert on a non-negligible fraction of instances. the existence of such functions with some additional assumptions was shown to be sufficient for generating perfect pseudorandom strings |blum, micali 82|, |yao 82|, |goldreich, goldwasser, micali 84|. below, among a few other observations, a weaker assumption about one-way functions is suggested, which is not only sufficient, but also necessary for the existence of pseudorandom generators. the main theorem can be understood without reading the sections 3-6.  l a levin
decidability of the purely existential fragment of the theory of term algebras  this paper is concerned with the question of the decidability and the complexity of the decision problem for certain fragments of the theory of free term algebras. the existential fragment of the theory of term algebras is shown to be decidable through the presentation of a nondeterministic algorithm, which, given a quantifier-free formula p, constructs a solution for p if it has one and indicates failure if there are no solutions. it is shown that the decision problem is in np by proving that, if a quantifier-free formula p has a solution, then there is one that can be represented as a dag in space at most cubic in the length of p. the decision problem is shown to be complete for np by reducing 3-sat to that problem. thus it is established that the existential fragment of the theory of pure list structures in the language of nil, cons, car, cdr, =, ≤ (subexpression) is np-complete. it is further shown that even a slightly more expressive fragment of the theory of term algebras, the one that allows bounded universal quantifiers, is undecidable.  k. n. venkataraman
maintenance of geometric extrema  let s be a set, f: s×s-&gt;r a bivariate function, and f (x,s) the maximum value of f(& lt;italic>x,y) over all elements y∈s. we say that f is decomposable with respect with the maximum if f( x,s) = max {f(x,s1),f(x< /italic>,s2), …,f(x,< italic>sk)} for any decomposition s = μ_i=1i< ;/italic>=ks< ;subscrpt>i. computing the maximum (minimum) value of a decomposable function is inherent in many problems of computational geometry and robotics. in this paper, a general technique is presented for updating the maximum (minimum) value of a decomposable function as elements are inserted into and deleted from the set s. our result holds for a semi- online model of dynamization: when an element is inserted, we are told how long it will stay. applications of this technique include efficient algorithms for dynamically computing the diameter or closest pair of a set of points, minimum separation among a set of rectangles, smallest distance between a set of points and a set of hyperplanes, and largest or smallest area (perimeter) retangles determined by a set of points. these problems are fundamental to application areas such as robotics, vlsi masking, and optimization.  david dobkin subhash suri
strongly equivalent logic programs a logic program pi1 is said to be equivalent to a logic program pi2 in the sense of the answer set semantics if pi1 and pi2 have the same answer sets. we are interested in the following stronger condition: for every logic program pi, pi1 ∪ pi has the same answer sets as pi2 ∪ pi. the study of strong equivalence is important, because we learn from it how one can simplify a part of a logic program without looking at the rest of it. the main theorem shows that the verification of strong equivalence can be accomplished by checking the equivalence of formulas in a monotonic logic, called the logic of here-and- there, which is intermediate between classical logic and intuitionistic logic. vladimir lifschitz david pearce agustín valverde
finite state verifiers i: the power of interaction  an investigation of interactive proof systems (ipss) where the verifier is a 2-way probabilistic finite state automaton (2pfa) is initiated. in this model, it is shown:  (1) ipss in which the verifier uses private randomization are strictly more powerful than ipss in which the random choices of the verifier are made public to the prover.  (2) ipss in which the verifier uses public randomization are strictly more powerful than 2pfa's alone, that is, without a prover.  (3) every language which can be accepted by some deterministic turing machine in exponential time can be accepted by some ips.  additional results concern two other classes of verifiers: 2pfa's that halt in polynomial expected time, and 2-way probabilistic pushdown automata that halt in polynomial time. in particular, ipss with verifiers in the latter class are as powerful as ipss where verifiers are polynomial-time probabilistic turing machines. in a companion paper [7], zero knowledge ipss with 2pfa verifiers are investigated.  cynthia dwork larry stockmeyer
approximation schemes for covering and packing problems in image processing and vlsi  a unified and powerful approach is presented for devising polynomial approximation schemes for many strongly np-complete problems. such schemes consist of families of approximation algorithms for each desired performance bound on the relative error ε > , with running time that is polynomial when ε is fixed. though the polynomiality of these algorithms depends on the degree of approximation ε being fixed, they cannot be improved, owing to a negative result stating that there are no fully polynomial approximation schemes for strongly np-complete problems unless np = p.  the unified technique that is introduced here, referred to as the shifting strategy, is applicable to numerous geometric covering and packing problems. the method of using the technique and how it varies with problem parameters are illustrated. a similar technique, independently devised by b. s. baker, was shown to be applicable for covering and packing problems on planar graphs.  dorit s. hochbaum wolfgang maass
entropy and sorting  we reconsider the old problem of sorting under partial information, and give polynomial time algorithms for the following tasks.  (1) given a partial order p, find (adaptively) a sequence of comparisons (questions of the form, "is x < y?") which sorts (i.e. finds an unknown linear extension of) p using o(log(e(p))) comparisons in worst case (where e(p) is the number of linear extensions of p).  (2) compute (on line) answers to any comparison algorithm for sorting a partial order p which force the algorithm to use (log(e(p))) comparisons.  (3) given a partial order p of size n, estimate e(p) to within a factor exponential in n. (we give upper and lower bounds which differ by the factor nn&amp;l; t;/supscrpt>/n!.)  < p>our approach, based on entropy of the comparability graph of p and convex minimization via the ellipsoid method, is completely different from earlier attempts to deal with these questions.  jeff kahn jeong han kim
a single-exponential upper bound for finding shortest paths in three dimensions  we derive a single-exponential time upper bound for finding the shortest path between two points in 3-dimensional euclidean space with (nonnecessarily convex) polyhedral obstacles. prior to this work, the best known algorithm required double-exponential time. given that the problem is known to be pspace-hard, the bound we present is essentially the best (in the worst-case sense) that can reasonably be expected.  john h. reif james a. storer
deciding first-order properties of locally tree-decomposable structures we introduce the concept of a class of graphs, or more generally, relational structures, being _locally tree-decomposable_. there are numerous examples of locally tree-decomposable classes, among them the class of planar graphs and all classes of bounded valence or of bounded tree-width. we also consider a slightly more general concept of a class of structures having _bounded local tree-width_.we show that for each property φ of structures that is definable in first-order logic and for each locally tree-decomposable class c of structures, there is a linear time algorithm deciding whether a given structure _a_ ∈ c has property φ. for classes c of bounded local tree- width, we show that for every _k_ ≥ 1 there is an algorithm solving the same problem in time _o_(_n< /i>1+(1/_k_)) (where _n_ is the cardinality of the input structure). markus frick martin grohe
on solving equations and disequations  we are interested in the problem of solving a systemi&amp;l; t;/inf>=ti:1≤i≤n,pj&amp;l; t;/inf> qj:1≤j≤m> of equations and disequations, also known as disunification. solutions to disunification problems are substitutions for the variables of the problem that make the two terms of each equation equal, but leave those of the disequations different. we investigate this in both algebraic and logical contexts where equality is defined by an equational theory and more generally by a definitive clause equality theory e. we show how e-disunification can be reduced to e-unification, that is, solving equations only, and give a disunification algorithm for theories given a unification algorithm. in fact, this result shows that for theories in which the solutions of all unification problems can also be represented finitely. we sketch how disunification can be applied to handle negation in logic programming with equality in a similar style to colmerauer's logic programming with rational trees, and to represent many solutions to ac-unification problems by a few solutions to aci- disunification problems.  wray l. buntine hans-jurgen burckert
incremental reduction in the lambda calculus  an incremental algorithm is one that takes advantage of the fact that the function it computes is to be evaluated repeatedly on inputs that differ only slightly from one another, avoiding unnecessary duplication of common computations.  we define here a new notion of incrementality for reduction in the untyped λ-calculus and describe an incremental reduction algorithm, Λinc. we show that Λinc has the desirable property of performing non-overlapping reductions on related terms, yet is simple enough to allow a practical implementation. the algorithm is based on a novel λ-reduction strategy that may prove useful in a non-incremental setting as well.  incremental λ-reduction can be used to advantage in any setting where an algorithm is specified in a functional or applicative manner.  john field tim teitelbaum
another advantage of free choice (extended abstract): completely asynchronous agreement protocols  recently, fischer, lynch and paterson [3] proved that no completely asynchronous consensus protocol can tolerate even a single unannounced process death. we exhibit here a probabilistic solution for this problem, which guarantees that as long as a majority of the processes continues to operate, a decision will be made (theorem 1). our solution is completely asynchronous and is rather strong: as in [4], it is guaranteed to work with probability 1 even against an adversary scheduler who knows all about the system.  michael ben-or
the alternating fixpoint of logic programs with negation  we introduce and describe the alternating fixpoint of a logic program with negation. the underlying idea is to monotonically build up a set of negative conclusions until the least fixpoint is reached, using a transformation related to the one that defines stable models, developed by gelfand and lifschitz. from a fixed set of negative conclusions, we can derive the positive conclusions that follow (without deriving any further negative ones), by traditional horn clause semantics. the union of positive and negative conclusions is called the alternating fixpoint partial model. the name "alternating" was chosen because the transformation runs in two passes; the first pass transforms an underestimate of the set of negative conclusions into an (intermediate) overestimate; the second pass transforms the overestimates into a new underestimate; the composition of the two passes is monotonic.  our main theorem is that the alternating fixpoint partial model is exactly the well-founded partial model.  we also show that a system is fixpoint logic, which permits rule bodies to be first order formulas but requires inductive relations to be positive within them, can be transformed straightforwardly into a normal logic program whose alternating fixpoint partial model corresponds to the least fixpoint of the fixpoint logic system. thus alternating fixpoint logic is at least as expressive as fixpoint logic. the converse is shown to hold for finite structures.  a. van gelder
partial order programming (extended abstract)  we introduce a programming paradigm in which statements are constraints over partial orders. a partial order programming problem has the form minimize u subject to u1 &amp;sqsupe; v1, u2 &amp;sqsupe; v2, *** where u is the goal, and u1 &amp;sqsupe; v1, u2 &amp;sqsupe; v2, *** is a collection of constraints called the program. a solution of the problem is a minimal value for u determined by values for u1, v1, etc. satisfying the constraints. the domain of values here is a partial order, a domain d with ordering relation &amp;sqsupe;.  the partial order programming paradigm has interesting properties:  it generalizes mathematical programming and also computer programming paradigms (logic, functional, and others) cleanly, and offers a foundation both for studying and combining paradigms.  it takes thorough advantage of known results for continuous functionals on complete partial orders, when the constraints involve expressions using only continuous and monotone operators. the semantics of these programs coincide with recent results on the relaxation solution method for constraint problems.  it presents a framework that may be effective in modeling, or knowledge representation, of complex systems.  d. s. parker
points and triangles in the plane and halving planes in space  we prove that for any set s of n points in the plane and n3-α triangles spanned by the points of s there exists a point (not necessarily of s) contained in at least n3-3α/(512 log5 n) of the triangles. this implies that any set of n points in three-dimensional space defines at most 6.4n8/3 log5/3 n halving planes.  boris aronov bernard chazelle herbert edelsbrunner leonidas j. guibas micha sharir rephael wenger
multiplicative complexity of polynomial multiplication over finite fields  let mq( n) denote the number of multiplications required to compute the coefficients of the product of two polynomials of degree n over a q-element field by means of bilinear algorithms. it is shown that mq(n) 3n \\- o(n). in particular, if q/2 < n q \\+ 1, we establish the tight bound q(n) = 3n \\+ 1 [q/2].the technique we use can be applied to analysis of algorithms for multiplication of polynomials modulo a polynomial as well.  michael kaminski nader h. bshouty
probabilistic simulations (preliminary version)  the results of this paper concern the question of how fast machines with one type of storage media can simulate machines with a different type of storage media. most work on this question has focused on the question of how fast one deterministic machine can simulate another. in this paper we shall look at the question of how fast a probabilistic machine can simulate another. this approach should be of interest in its own right, in view of the great attention that probabilistic algorithms have recently attracted.  nicholas pippenger
low level complexity for combinatorial games  there have been numerous attempts to discuss the time complexity of problems and classify them into hierarchical classes such as p, np, pspace, exp, etc. a great number of familiar problems have been reported which are complete in np (nondeterministic polynomial time). even and tarjan considered generalized hex and showed that the problem to determine who wins the game if each player plays perfectly is complete in polynomial space. shaefer derived some two- person game from np complete problems which are complete in polynomial space.  a rough discussion such as to determine whether or not a given problem belongs to np is independent of the machine model and the way of defining the size of problems, since any of the commonly used machine models can be simulated by any other with a polynomial loss in running time and by no matter what criteria the size is defined, they differ from each other by polynomial order. however, in precise discussion, for example, in the discussion whether the computation of a problem requires o(n k) time or o(nk+l) time, the complexity heavily depends on machine models and the definition of size of problems. from these points, we introduce somewhat stronger notion of the reducibility.  akeo adachi shigeki iwata takumi kasai
reducing computational complexity with array predicates this article describes how _array predicates_ were used to reduce the computational complexity of four apl primitive functions when one of their arguments is a permutation vector. the search primitives, _indexof_ and set membership, and the sorting _primitives,_ upgrade and downgrade, execute in linear time on such arguments. our contribution, a method for static determination of array properties, lets us generate code that is optimized for special cases of primitives. our approach eliminates runtime checks which would otherwise slow down the execution of all cases of the effected primitives. we use the same analysis technique to reduce the type complexity of certain array primitives. robert bernecky
competitive algorithms for on-line problems  an on-line problem is one in which an algorithm must handle a sequence of requests, satisfying each request without knowledge of the future requests. examples of on-line problems include scheduling the motion of elevators, finding routes in networks, allocating cache memory, and maintaining dynamic data structures. a competitive algorithm for an on-line problem has the property that its performance on any sequence of requests is within a constant factor of the performance of any other algorithm on the same sequence. this paper presents several general results concerning competitive algorithms, as well as results on specific on-line problems.  mark manasse lyle mcgeoch daniel sleator
probabilistic temporal logics for finite and bounded models  we present two (closely-related) propositional probabilistic temporal logics based on temporal logics of branching time as introduced by ben-ari, pnueli and manna and by clarke and emerson. the first logic, ptlf, is interpreted over finite models, while the second logic, ptlb, which is an extension of the first one, is interpreted over infinite models with transition probabilities bounded away from 0. the logic ptlf allows us to reason about finite-state sequential probabilistic programs, and the logic ptlb allows us to reason about (finite-state) concurrent probabilistic programs, without any explicit reference to the actual values of their state-transition probabilities. a generalization of the tableau method yields exponential-time decision procedures for our logics, and complete axiomatizations of them are given. several meta-results, including the absence of a finite-model property for ptlb, and the connection between satisfiable formulae of ptlb and finite state concurrent probabilistic programs, are also discussed.  sergiu hart micha sharir(
an optimal algorithm for the ( k)-levels, with applications to separation and transversal problems  this paper gives an optimal onlogn+nk time algorithm for constructing the levels1,…,k in an arrangement ofn lines in the plane. this algorithmis extended to compute these levels in an arrangement ofn unboundedx-monotone polygonal convex chains,of which each pair intersects at most a constant number of times.  these algorithms can be used to solve the following separation andtransversal problems. for a set nblue points and an set of n redpoints, find a line that separates the two sets in such a way that thesum, m, of the number of red pointsabove the line and the number of blue points below the line isminimized. such an optimal line can be found in onmlogm+nlogn time. for a set ofnline segments in the plane, find aline that intersects the maximum number of the line segments. such anoptimal line can be found in onmlogm+nlogn time for vertical segments and in onmlogm+nlog  2  nan expected time for arbitrary line segments, wherem denotes the number ofline segments not intersected by the optimal line.  hazel everett jean-marc robert marc van kreveld
on exact specification by examples  some recent work [7, 14, 15] in computational learning theory has discussed learning in situations where the teacher is helpful, and can choose to present carefully chosen sequences of labelled examples to the learner. we say a function t in a set h of functions (a hypothesis space) defined on a set x is specified by s***x if the only function in h which agrees with t on s is t itself. the specification number (t) of t is the least cardinality of such an s. for a general hypothesis space, we show that the specification number of any hypotheis is at least equal to a parameter from [14] known as the testing dimension of h. we investigate in some detail the specification numbers of hypotheses in the set hn of linearly separable boolean functions: we present general methods for finding upper bounds on  (t) and we characterise those t which have largest  (t). we obtain a general lower bound on the number of examples required and we show that for all nested hypotheses, this lower bound is attained. we prove that for any t ε hn, there is exactly one set of examples of minimal cardinality (i.e., of cardinality  (t)) which specifies t. we then discuss those t ε hn which have limited dependence, in the sense that some of the variables are redundant (i.e., there are irrelevant attributes), giving tight upper and lower bounds on  (t) for such hypotheses. in the final section of the paper, we address the complexity of computing specification numbers and related parameters.  martin anthony graham brightwell dave cohen john shawe-taylor