Circular Separability of Polygons

Two planar sets are circularly separable if there exists a circle enclosing one of the sets and whose open interior disk does not intersect the other set. This paper studies two problems related to circular separability. A linear-time algorithm is proposed to decide if two polygons are circularly separable. The algorithm outputs the smallest separating circle. The second problem asks for the largest circle included in a preprocessed, convex polygon, under some point and/ or line constraints. The resulting circle must contain the query points and it must lie in the halfplanes delimited by the query lines. Received October 25, 1998; revised April 21, 1999.     

Triangulating input-constrained planar point sets

We present a linear-time algorithm for computing a triangulation of n points in 2D whose positions are constrained to n disjoint disks of uniform size, after O(nlogn) preprocessing applied to these disks. Our algorithm can be extended to any collection of convex sets of bounded areas and aspect ratios, assuming no point lies in more than some constant number of sets (bounded depth of overlap), and each set contains only a constant number of query points.     

Some chain visibility problems in a simple polygon

In this paper, the notions of convex chain visibility and reflex chain visibility of a simple polygonP are introduced, and some optimal algorithms concerned with convex- and reflex-chain visibility problems are described. For a convex-chain visibility problem, two linear-time algorithms are exhibited for determining whether or notP is visible from a given convex chain; one is the turn-checking approach and the other is the decomposition approach based on checking edge visibilities. We also present a linear-time algorithm for finding, if any, all maximal convex chains of a given polygonP from whichP is visible, where a maximal convex chain is a convex chain which does not properly include any other convex chains. It can be made by showing that there can be at most four visible maximal convex chains inP with an empty kernel. By similar arguments, we show that the same problems for reflex chain visibility can be easily solved in linear time.     

For completeness, sublogarithmic space is no space

It is shown that for any class C closed under linear-time reductions, the complete sets for C under sublogarithmic reductions are also complete under 2DFA reductions, and thus are isomorphic under first-order reductions.     

Don’t care words with an application to the automata-based approach for real addition

Automata have proved to be a useful tool in infinite-state model checking, since they can represent infinite sets of integers and reals. However, analogous to the use of binary decision diagrams (bdds) to represent finite sets, the sizes of the automata are an obstacle in the automata-based set representation. In this article, we generalize the notion of “don’t cares” for bdds to word languages as a means to reduce the automata sizes. We show that the minimal weak deterministic Büchi automaton (wdba) with respect to a given don’t care set, under certain restrictions, is uniquely determined and can be efficiently constructed. We apply don’t cares to improve the efficiency of a decision procedure for the first-order logic over the mixed linear arithmetic over the integers and the reals based on wdbas.     

Searching for empty convex polygons

A key problem in computational geometry is the identification of subsets of a point set having particular properties. We study this problem for the properties of convexity and emptiness. We show that finding empty triangles is related to the problem of determining pairs of vertices that see each other in a star-shaped polygon. A linear-time algorithm for this problem which is of independent interest yields an optimal algorithm for finding all empty triangles. This result is then extended to an algorithm for finding empty convex r-gons (r> 3) and for determining a largest empty convex subset. Finally, extensions to higher dimensions are mentioned.The first author is pleased to acknowledge support by the National Science Foundation under Grant CCR-8700917. The research of the second author was supported by Amoco Foundation Faculty Development Grant CS 1-6-44862 and by the National Science Foundation under Grant CCR-8714565.     

Observations on complete sets between linear time and polynomial time

There is a single set that is complete for a variety of nondeterministic time complexity classes with respect to related versions of m-reducibility. This observation immediately leads to transfer results for determinism versus nondeterminism solutions. Also, an upward transfer of collapses of certain oracle hierarchies, built analogously to the polynomial-time or the linear-time hierarchies, can be shown by means of uniformly constructed sets that are complete for related levels of all these hierarchies. A similar result holds for difference hierarchies over nondeterministic complexity classes. Finally, we give an oracle set relative to which the nondeterministic classes coincide with the deterministic ones, for several sets of time bounds, and we prove that the strictness of the tape-number hierarchy for deterministic linear-time Turing machines does not relativize.     

一种基于优先级扩展的时间自动机模型中DBM减法算法的改进

本文介绍一种具有优先级扩展的时间自动机模型,并对一种计算DBM减法算法进行改进。这种减法是DBM上操作中的一种,它会产生需要用DBM集来表示的非凸集合。DBM的数量影响符号模型检测的性能,我们的减法算法是有效的,因为它产生的DBM的数量相对于最初算法具有较大程度的约减。DBM减法操作扩展了具有优先级的时间自动机理论,它对对于具有紧急行为的变换描述、死锁检测、时间博弈等问题具有非常重要的作用。     

A linear-time algorithm for linearL1 approximation of points

In this paper we present a linear-time algorithm for approximating a set ofn points by a linear function, or a line, that minimizes theL ₁ norm. The algorithmic complexity of this problem appears not to have been investigated, although anO(n ³) naive algorithm can be easily obtained based on some simple characteristics of an optimumL ₁ solution. Our linear-time algorithm is optimal within a constant factor and enables us to use linearL ₁ approximation of many points in practice. The complexity ofL ₁ linear approximation of a piecewise linear function is also touched upon.     

参数化系统安全性的启发式符号验证

参数化系统(paramterized system)是指包含特定有限状态进程多个实例的并发系统,其中的参数是指系统内进程实例的数目,即系统的规模.反向可达性分析(backward reachability analysis)已被广泛用于验证参数化系统是否满足以向上封闭(upward-closed)集合表示的安全性(safety property).与有限状态系统验证相类似,参数化系统的验证同样也面临着状态爆炸(state explosion)问题,并且模型检测算法的有效性依赖于如何采用有效的数据结构表示状     

Towards a computation system based on set theory

An axiomatic theory of sets and rules is formulated, which permits the use of sets as data structures and allows rules to operate on rules, numbers, or sets. We might call it a “polymorphic set theory”. Our theory combines the λ-calculus with traditional set theories. A natural set-theoretic model of the theory is constructed, establishing the consistency of the theory and bounding its proof-theoretic strength, and giving in a sense its denotational semantics. Another model, a natural recursion-theoretic model, is constructed, in which only recursive operations from integers to integers are represented, even though the logic can be classical. Some related philosophical considerations on the notions of set, type, and data structure are given in an appendix.     

Clique-perfectness and balancedness of some graph classes

A graph is clique-perfect if the maximum size of a clique-independent set (a set of pairwise disjoint maximal cliques) and the minimum size of a clique-transversal set (a set of vertices meeting every maximal clique) coincide for each induced subgraph. A graph is balanced if its clique-matrix contains no square submatrix of odd size with exactly two ones per row and column. In this work, we give linear-time recognition algorithms and minimal forbidden induced subgraph characterizations of clique-perfectness and balancedness of P₄-tidy graphs and a linear-time algorithm for computing a maximum clique-independent set and a minimum clique-transversal set for any P₄-tidy graph. We also give a minimal forbidden induced subgraph characterization and a linear-time recognition algorithm for balancedness of paw-free graphs. Finally, we show that clique-perfectness of diamond-free graphs can be decided in polynomial time by showing that a diamond-free graph is clique-perfect if and only if it is balanced.     

Maximum gap labelings of graphs

Given a graph, we define a base set to be a set of integers of size equal to the number of vertices in the graph. Given a graph and a base set, a labeling of the graph from the base set is an assignment of distinct integers from the base set to the vertices of the graph. The gap of an edge in a labeled graph is the absolute value of the difference between the labels of its endpoints. The gap of a labeled graph is the sum of the gaps of its edges.The maximum gap graph labeling problem takes as input a graph and a base set and maximizes the gap of the graph over all possible labelings from the base set. We show that this problem is NP-complete even when the base set is restricted to consecutive integers. We also show that this restricted case has polynomial time approximations that achieve a factor of 2/3 for trees, of 1/2 for bipartite graphs, and of 1/4 for general graphs, with a deterministic algorithm, while an expected factor of 1/3 for general graphs is achieved with a randomized algorithm. The case of general base sets is approximated within an expected factor of 1/16 for general graphs with a randomized polynomial time algorithm. We finally give a polynomial time algorithm that solves the maximum gap graph labeling problem for a graph that has bounded degree and bounded treewidth. The maximum graph labeling problem shows connections with the graceful tree conjecture.     

A predictor-corrector type algorithm for the pseudospectral abscissa computation of time-delay systems

The pseudospectrum of a linear time-invariant system is the set in the complex plane consisting of all the roots of the characteristic equation when the system matrices are subjected to all possible perturbations with a given upper bound. The pseudospectral abscissa is defined as the maximum real part of the characteristic roots in the pseudospectrum and, therefore, it is for instance important from a robust stability point of view. In this paper we present an accurate method for the computation of the pseudospectral abscissa of retarded delay differential equations with discrete pointwise delays. Our approach is based on the connections between the pseudospectrum and the level sets of an appropriately defined complex function. The computation is done in two steps. In the prediction step, an approximation of the pseudospectral is obtained based on a rational approximation of the characteristic matrix and the application of a bisection algorithm. Each step in this bisection algorithm relies on checking the presence of the imaginary axis eigenvalues of a complex matrix, similar to the delay free case. In the corrector step, the approximate pseudospectral abscissa is corrected to any given accuracy, by solving a set of nonlinear equations that characterizes the extreme points in the pseudospectrum contours.     

联锁逻辑形式化模型检验的研究

利用自动机理论模型检验算法，检验车站联锁逻辑的有色Petri网模型是否满足预期的性能。通过采用带标签的广义Büchi自动机(LGBA)构建线性时态逻辑，有效地解决了模型检验中的状态空间爆炸问题。该方法的研究增强了有色Petri网的分析和验证能力，利用该方法对车站联锁逻辑的实际问题进行了性能验证。     

Distributed Symbolic Model Checking for μ-Calculus

In this paper we propose a distributed symbolic algorithm for model checking of propositional μ-calculus formulas. μ-calculus is a powerful formalism and μ-calculus model checking can solve many problems, including, for example, verification of (fair) CTL and LTL properties. Previous works on distributed symbolic model checking were restricted to reachability analysis and safety properties. This work thus significantly extends the scope of properties that can be verified distributively, enabling us to use them for very large designs.The algorithm distributively evaluates subformulas. It results in sets of states which are evenly distributed among the processes. We show that this algorithm is scalable and therefore can be implemented on huge distributed clusters of computing nodes. The memory modules of the computing nodes collaborate to create a very large memory space, thus enabling the checking of much larger designs. We formally prove the correctness of the parallel algorithm. We complement the distribution of the state sets by showing how to distribute the transition relation.This research was supported by The Israel Science Foundation (grant number 111/01-2) and by a grant from Intel Academic Relations.     

Computational complexity of queries based on itemsets

We investigate determining the exact bounds of the frequencies of conjunctions based on frequent sets. Our scenario is an important special case of some general probabilistic logic problems that are known to be intractable. We show that despite the limitations our problems are also intractable, namely, we show that checking whether the maximal consistent frequency of a query is larger than a given threshold is NP-complete and that evaluating the Maximum Entropy estimate of a query is PP-hard. We also prove that checking consistency is NP-complete.     

Sorting by Short Block-Moves

Sorting permutations by operations such as reversals and block-moves has received much interest because of its applications in the study of genome rearrangements and in the design of interconnection networks. A short block-move is an operation on a permutation that moves an element at most two positions away from its original position. This paper investigates the problem of finding a minimum-length sorting sequence of short block-moves for a given permutation. A 4/3 -approximation algorithm for this problem is presented. Woven double-strip permutations are defined and a polynomial-time algorithm for this class of permutations is devised that employs graph matching techniques. A linear-time maximum matching algorithm for a special class of grid graphs improves the time complexity of the algorithm for woven double-strip permutations. Received June 1, 1997; revised July 25, 1998.     

Linear-time wrappers to identify atypical points: two subset generation methods

The wrapper approach to identify atypical examples can be preferable to the filter approach (which may not be consistent with the classifier in use), but its running time is prohibitive. The fastest available wrappers are quadratic in the number of examples, which is far too expensive for atypical detection. The algorithm presented in this paper is a linear-time wrapper that is roughly 75 times faster than the quadratic wrappers on average over 7 classifiers and 20 data sets tested in this research. Also, two subset generation, methods for the wrapper are introduced and compared. Atypical points are defined in this paper as the misclassified points that the proposed algorithm (Atypical Sequential Removing: ASR) finds not useful to the classification task. They may include outliers as well as overlapping samples. ASR can identify and rank atypical points in the whole data set without damaging the prediction accuracy. It is general enough that classifiers without reject option can use it. Experiments on benchmark data sets and different classifiers show promising results and confirm that this wrapper method has some advantages and can be used for atypical detection.