waashk/acm huggingface dataset:
an automata-theoretic approach to branching-time model checking  translating linear temporal logic formulas to automata has proven to be an effective approach for implementing linear-time model-checking, and for obtaining many extensions and improvements to this verification method. on the other hand, for branching temporal logic, automata-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. recently, bernholtz and grumberg [1993] have shown that this exponential penalty can be avoided, though they did not match the linear complexity of non-automata-theoretic algorithms. in this paper, we show that alternating tree automata are the key to a comprehensive automata- theoretic framework for branching temporal logics. not only can they be used to obtain optimal decision procedures, as was shown by muller et al., but, as we show here, they also make it possible to derive optimal model-checking algorithms. moreover, the simple combinatorial structure that emerges from the automata-theoretic approach opens up new possibilities for the implementation of branching-time model checking and has enabled us to derive improved space complexity bounds for this long-standing problem.  orna kupferman moshe y. vardi pierre wolper
functional reactive programming from first principles  functional reactive programming, or frp, is a general framework for programming hybrid systems in a high-level, declarative manner. the key ideas in frp are its notions of behaviors and events. behaviors are time-varying, reactive values, while events are time-ordered sequences of discrete-time event occurrences. frp is the essence of fran, a domain-specific language embedded in haskell for programming reactive animations, but frp is now also being used in vision, robotics and other control systems applications.  in this paper we explore the formal semantics of frp and how itrelates to an implementation based on streams that represent (and therefore only approximate) continuous behaviors. we show that, in the limit as the sampling interval goes to zero, the implementation is faithful to the formal, continuous semantics, but only when certain constraints on behaviors are observed. we explore the nature of these constraints, which vary amongst the frp primitives. our results show both the power and limitations of this approach to language design and implementation. as an example of a limitation, we show that streams are incapable of representing instantaneous predicate events over behaviors.  zhanyong wan paul hudak
on some deterministic space complexity problems  in this paper we give a complete problem in dspace(n). the problem is whether there exists a cycle in the connected component containing (o,o,...,o) in the graph gp of the zeroes of a polynomial p over gf(2) under a suitable natural coding. hence the deterministic space complexity of this problem is o(n) but not o(n). we give as well several problems for which we can obtain very close upper and lower deterministic space bounds. for example, the deterministic space complexity to determine whether there exists a cycle in the graph of the set of assignments satisfying a boolean formula is o(n/log n) but not o(n/log2n).  hong jia-wei
simplifying a polygonal subdivision while keeping it simple  we study the problem of simplifying a polygonal subdivision, subjectof a given error bound, $\epsilon$, and subject to maintaining the topology of the input, while not introducing new (steiner) vertices. in particular, we require that the simplified chains may not cross themselves or cross other chains. in gis applications, for example, we are interested in simplifying the banks of a river without the left and right banks getting "tangled" and without "islands" becoming part of the land mass. maintaining topology during subdivision simplification is an important constraint in many real gis applications.  \noindent we give both theoretical and experimental results.  (a). we prove that the general problem we are trying to solve is in fact difficult to solve, even approximately: we show that it is min pb-complete and that, in particular, assuming p $\neq$ np, in the general case we cannot obtain in polynomial time an approximation within a factor $n^{1/5-\delta}$ of an optimal solution.  (b). we propose some heuristic methods for solving the problem, which we have implemented. our experimental results show that, in practice, we get quite good simplifications in a reasonable amount of time.  regina estkowski joseph s. b. mitchell
comparison-sorting and selecting in totally monotone matrices  an  m x n matrix a is called totally monotone if for all i1 < i2 and j1 < j2, a[i1, j1] > a[i1, j2 implies a[i2, j1] > a[i2, j2]. we consider the complexity of comparison-based selection and sorting algorithms in such matrices. although our selection algorithm counts only comparisons its advantage on all previous work is that it can also handle selection of elements of different (and arbitrary) ranks in different rows (or even selection of elements of several ranks in each row), in time which is slightly better than that of the best known algorithm for selecting elements of the same rank in each row. we also determine the decision tree complexity of sorting each row of a totally monotone matrix up to a factor of at most log n by proving a quadratic lower bound and by slightly improving the upper bound. no nontrivial lower bound was previously known for this problem. in particular for the case m = n we prove a tight (n2) lower bound. this bound holds for any decision-tree algorithm, and not only for a comparison-based algorithm. the lower bound is proved by an exact characterization of the bitonic totally monotone matrices, whereas our new algorithms depend on techniques from parallel comparison algorithms.  noga alon yossi azar
objects that cannot be taken apart with two hands  it has been conjectured that every configuration c of convex objects in 3-space with disjoint interiorscan be taken apart by translation with two hands: that is, some propersubset of c can be translated to infinity withoutdisturbing its complement. we show that the conjecture holds for five orfewer objects and give a counterexample with six objects. we extend thecounterexample to a configuration that cannot be taken apart with twohands using arbitrary isometries (rigid motions).  jack snoeyink jorge stolfi
an indexed model of recursive types for foundational proof-carrying code the proofs of "traditional" proof carrying code (pcc) are type-specialized in the sense that they require axioms about a specific type system. in contrast, the proofs of foundational pcc explicitly define all required types and explicitly prove all the required properties of those types assuming only a fixed foundation of mathematics such as higher-order logic. foundational pcc is both more flexible and more secure than type-specialized pcc.for foundational pcc we need semantic models of type systems on von neumann machines. previous models have been either too weak (lacking general recursive types and first- class function-pointers), too complex (requiring machine-checkable proofs of large bodies of computability theory), or not obviously applicable to von neumann machines. our new model is strong, simple, and works either in λ-calculus or on pentiums. andrew w. appel david mcallester
on the relationship between permission and obligation  in two interesting papers ((1983), (1986)) thorne mccarty has presented a semantics for the central deontic concepts, permission and obligation, based upon a semantics for an action language. the latter, in turn, was constructed along lines deriving from pratt-harel dynamic logic.  i shall here offer some critical comments on mccarty's analysis of the relationship between obligation and permission, and of his account of so- called "free- choice" permissions; these come in section ii, below. in section i an outline sketch is given of the main features of mccarty's semantics with which the criticism will be concerned.  a. j. i. jones
shortest paths in the plane with polygonal obstacles  we present a practical algorithm for finding minimum-length paths between points in the euclidean plane with (not necessarily convex) polygonal obstacles. prior to this work, the best known algorithm for finding the shortest path between two points in the plane required  (n2 log n) time and o(n2) space, where n denotes the number of obstacle edges. assuming that a triangulation or a voronoi diagram for the obstacle space is provided with the input (if is not, either one can be precomputed in o(n log n) time), we present an o(kn) time algorithm, where k denotes the number of "islands" (connected components) in the obstacle space. the algorithm uses only o(n) space and, given a source point s, produces an o(n) size data structure such that the distance between s and any other point x in the plane (x) is not necessarily an obstacle vertex or a point on an obstacle edge) can be computed in o(1) time. the algorithm can also be used to compute shortest paths for the movement of a disk (so that optimal movement for arbitrary objects can be computed to the accuracy of enclosing them with the smallest possible disk).  james a. storer john h. reif
automata theoretic techniques for modal logics of programs: (extended abstract)  we present a new technique for obtaining decision procedures for modal logics of programs. the technique centers around a new class of finite automata on infinite trees for which the emptiness problem can be solved in polynomial time. the decision procedures then consist of constructing an automaton af for a given formula f, such that af accepts some tree if and only if f is satisfiable. we illustrate our technique by giving an exponential decision procedure for deterministic propositional dynamic logic and a variant of the &amp;mgr-calculus; of kozen.  moshe y. vardi pierre wolper
unified method for determining canonical forms of a matrix let _k_ be a field and _a_ a matrix with entries in _k._ it is well known that if det(_xi - a_) splits in _k,_ there exists a regular matrix _p_ with entries in _k,_ such that _p_-1 _ap_ is a diagonal matrix of jordan blocks. two problems arise that have been well treated in the literature. what should be done if the roots of _xi - a_ do not belong to _k?_ how can one compute _p?_ in this note, i answer these questions in a unified way. j. m. de olazábal
an improved context-free recognizer  a new algorithm for recognizing and parsing arbitrary context-free languages is presented, and several new results are given on the computational complexity of these problems. the new algorithm is of both practical and theoretical interest. it is conceptually simple and allows a variety of efficient implementations, which are worked out in detail. two versions are given which run in faster than cubic time. surprisingly close connections between the cocke-kasami-younger and earley algorithms are established which reveal that the two algorithms are "almost" identical.  susan l. graham michael harrison and walter l. ruzzo
equations between regular terms and an application to process logic  regular terms with the kleene operations ,;, and * can be thought of as operators on languages, generating other languages. an equation r1 r2 between two such terms is said to be satisfiable just in case languages exist which make this equation true. we show that the satisfiability problem even for *-free regular terms is undecidable. similar techniques are used to show that a very natural extension of the process logic of harel, kozen and parikh is undecidable.  ashok chandra joe halpern albert meyer rohit parikh
inadequacy of computable loop invariants  hoare logic is a widely recommended verification tool. there is, however, a problem of finding easily checkable loop invariants; it is known that decidable assertions do not suffice to verify while programs, even when the pre- and postconditions are decidable. we show here a stronger result: decidable invariants do not suffice to verify single-loop programs. we also show that this problem arises even in extremely simple contexts. let n be the structure consisting of the set of natural numbers together with the functions s(x)=x+1,d(x)&amp;l; t;/italic>=2(x)=***xx,y,z such that the asserted program =y=zn but any loop invariant i(x,y,z) for this asserted program is undecidable.  andreas blass yuri gurevich
a computational geometry workbench  we are constructing a workbench for computational geometry. this is intended to provide a framework for the implementation, testing, demonstration and application of algorithms in computational geometry. the workbench is being written in smalltalk/v using an apple macintosh ii.  the object-oriented model used in smalltalk is well- suited to algorithms manipulating geometric objects. in addition, the programming environment can be easily extended, and provides excellent graphics facilities, data abstraction, encapsulation, and incremental modification.  we have completed the design and implementation of the workbench platform, insofar as such a system can ever be considered complete. among the features of the system are:  an interactive graphical environment, including operations for creation and editing of geometric figures, and for the operation of algorithm on these figures  the system supports:  high-level representation- independent geometric objects (points, lines, polygons,…)  geometric data structures (segment trees, range trees,…)  non-geometric data structures (finger trees, splay trees, heaps, …)  "standard" algorithmic tools in as general a form as possible. algorithms currently available in the system include tarjan and van wyk's triangulation of a simple polygon, fortune's voronoi diagram,  preparata's chain decomposition, and melkman's convex hull algorithm.  tools for the animation of geometric algorithms  high-level graphical and symbolic debugging facilities  portability, due to the separation of the machine-independent code and the machine-dependent user- interface.  automatic handling of basic operations (device-independent graphics, storage management) allowing the implementor to focus on algorithmic issues  our group is currently working on extensions in two directions:  implementing additional algorithms from two-dimensional computational geometry  providing the framework for implementations of three-dimensional algorithms  we are also conducting comparison studies of different algorithms and data structures, including a comparison of different triangulation and convex hull algorithms for large input sizes and an empirical test of the dynamic optimality conjecture of sleator and tarjan using both splay and finger trees in the tarjan and van wyk triangulation.  the workbench is being demonstrated during this symposium.  a. knight j. may j. mcaffer t. nguyen j.-r. sack
a threshold of ln n for approximating set cover  given a collection f of subsets of s ={1,…,n}, setcover is the problem of selecting as few as possiblesubsets from  f such that their union coverss,, and maxk-cover is the problem of selectingk subsets from f such that their union has maximum cardinality. both these problems arenp-hard. we prove that (1 - o(1)) lnn is a threshold below which setcover cannot be approximated efficiently, unless np has slightlysuperpolynomial time algorithms. this closes the gap (up to low-orderterms) between the ratio of approximation achievable by the greedyalogorithm (which is (1 - o(1)) lnn), and provious results of lund and yanakakis, that showed hardness ofapproximation within a ratio of log2n/2 0.72 ln n. for maxk-cover, we show an approximationthreshold of (1 - 1/e)(up tolow-order terms), under assumption that p np.  uriel feige
on the formalization of architectural types with process algebras  architectural styles play an important role in software engineering as they convey codified principles and experience which help the construction of software systems with high levels of efficiency and confidence. we address the problem of formalizing and analyzing architectural styles in an operational setting by introducing the intermediate abstraction of architectural type. we develop the concept of architectural type in a process algebraic framework because of its modeling adequacy and the availability of means, such as milner's weak bisimulation equivalence, which allow us to reason compositionally and efficiently about the well formedness of architectural types.  marco bernardo paolo ciancarini lorenzo donatiello
min-max sort: a simple sorting method (abstract only)  a simple sorting algorithm which can be considered as a double-ended selection sort is presented. the algorithm, called min-max sort is based on the optimal method for simultaneously finding the smallest and the largest elements in an array [2]. the smallest and the largest elements found are pushed respectively to the left and right of the array, and the process is repeated on the middle portion. the correctness and termination of min-max sort are easily demonstrated through the use of standard loop invariant ideas. the algorithm fits the "hard split/easy join" paradigm of merritt [1].  let n be even. given an array a[1..n], it is said to be in a "rainbow pattern" if for each i := 1 to n/2 we have a [i] ≤ a[n+1-i]. the following step 1 establishes the rainbow pattern in a.  step 1 : for i := 1 to n div 2 do if a[i] > a[n+1-i] then swap(a[i],a[n+1-i]).  the step 1 requires n/2 number of comparisons. observe that when an array is in a rainbow pattern it is guaranteed that the smallest element of the array is in the left half of the array and the largest in the second half.  step 2 is to find p and q such that a[p] ≤ a[i] for i = 1 to n/2, and a[q] ≥ a[j] for j = n/2+1 to n, and swap(a[1],a[p]) and swap(a[q],a[n]).  the step 2 requires (n/2-1)+(n/2-1) number of comparisons. thus we have brought the largest and the smallest of elements of a into first and the last positions respectively at a cost of 3n/2 - 2 comparisons (in contrast to 2n - 2 comparisons required in the straight forward method).  observe that the rainbow pattern in a is still preserved, except perhaps the two pairs (a[p],a[n+1-p]) and (a[q],a[n+1-q]). the rainbow pattern is reinstated, in just two comparisons, by  step 3 : if a[p] > a[n+1-p] then swap(a[p],a[n+1-p]), and if a(n+1-q] > a[q] then swap(a[q],a[n+1-q]).  the general form of step 2 is step 2′ : find p and q such that a[p] ≤ a[i] for all i = k to n/2, and a[q] ≥ a[j] for all j = n/2+1 to n+1-k. the algorithm step 1; for k := 1 to n div 2-1 do begin step 2′; step 3; end; sorts the array a.  step 1 requires n/2 comparisons; step 2′ requires 2(n/2-k) and step 3 requires two comparisons. thus the total number of comparisons required to sort the array a is = n/2 + @@@@ [2(n/2 - k) + 2] = (n2 \\+ 4n - 8)/4  the size of the central portion decreases steadily by 2 and the invariant assures that the smallest and largest of the central portion can be found with a number of comparisons approximately equal to the size of the portion. the algorithm is included in discussion by zahn [3].  narayan murthy
relationships between and among models  mylopoulos: when we talk about a model, it can be either a program snapshot or execution, or a program, a data base, a conceptual schema, or a knowledge base. we can think of a program as consisting of units of some sort, e.g., procedures, assertions, data types; and they are related by relationships of various kinds. some relationships are user-defined and dependent on the domain the model is dealing with. on the other hand, some of the relationships used to describe the model are primitive, in the sense that their semantics are well-defined and embedded in the modelling framework in terms of which the model has been defined. some examples from the three areas being represented here are isa, part-of, instance-of. certain other relationships include procedural attachment, used in ai to associate procedures to data classes to specify operations on instances of the classes.  in programming languages, considering statements as the units, statement sequencing is a primitive relationship between these units. considering algol- like begin blocks as the units, scoping rules are relationships between units (blocks). procedure activation rules between blocks are another example of a relationship that can be considered as primitive and embedded in the modelling framework. simula concatenation, which allows the definition of classes to be given in terms of other classes gives a relationship between classes. the association of operations to a data type can also be treated as a relationship that has been used in pls.
efficient algorithms for generalized intersection searching on non-iso- oriented objects  generalized intersection searching problems are a class of geometric query- retrieval problems where the questions of interest concern the intersection of a query object with aggregates of geometric objects (rather than with individual objects.) this class contains, as a special case, the well-studied class of standard intersection searching problems and is rich in applications. unfortunately, the solutions known for the standard problems do not yield efficient solutions to the generalized problems. recently, efficient solutions have been given for generalized problems where the input and query objects are iso-oriented (i.e., axes- parallel) or where the aggregates satisfy additional properties (e.g., connectedness). in this paper, efficient algorithms are given for several generalized problems involving non-iso-oriented objects. these problems include: generalized halfspace range searching, segment intersection searching, triangle stabbing, and triangle range searching. the techniques used include: computing suitable sparse representations of the input, persistent data structures, and filtering search.  prosenjit gupta ravi janardan michiel smid
algorithms for subset testing and finding maximal sets  in this paper we consider two related problems: subset testing and finding maximal sets. first, consider a sequence of n operations, where each operation either creates a set, inserts (deletes) an element into (from) a set, queries whether a particular element is in a set, queries whether or not one set is a subset of another, or queries whether or not the intersection of two sets is empty. we show that for any integer k, one can implement subset and intersection testing in time o(n1-(1/k) log n) and all of the other operations in time o(n1/k log n)). it requires o(nk+1)/k) space. when k = 2, this yields a worst case time complexity of o(n1/2 log n) per operation, and uses o(n3/2) space. second, consider a set of sets, where the total size of the input is o(n). we show that one can find those sets that are maximal (a set is maximal if it is not contained in any other set) in time o(mn), where m is the number of maximal sets.  daniel m. yellin
solving projective complete intersection faster  in this paper, we present a new method for solving square polynomial systems with no zero at infinity. we analyze its complexity, which indicates substantial improvements, compared with the previously known methods for solving such systems. we describe a framework for symbolic and numeric computations, developed in c++, in which we have implemented this algorithm. we mention the techniques that are involved in order to build efficient codes and compare with existing softwares. we end by some applications of this method, considering in particular an autocalibration problem in computer vision and an identification problem in signal processing, and report on the results of our first implementation.  bernard mourrain philippe trebuchet