waashk/dblp huggingface dataset:
on boundaries of highly visible spaces and applications. the purpose of this paper is to investigate the properties of a certain class of highly visible spaces. for a given geometric space c containing obstacles specified by disjoint subsets of c, the free space f is defined to be the portion of c not occupied by these obstacles. the space is said to be highly visible if at each point in f a viewer can see at least an ε fraction of the entire f. this assumption has been used for robotic motion planning in the analysis of random sampling of points in the robot's configuration space, as well as the upper bound of the minimum number of guards needed for art gallery problems. however, there is no prior result on the implication of this assumption to the geometry of the space under study. for the two-dimensional case, with the additional assumptions that c is bounded within a rectangle of constant aspect ratio and that the volume ratio between f and c is a constant, we use the proof technique of "charging" each obstacle boundary segment by a certain portion of c to show that the total length of all obstacle boundaries in c is o(√nµ(f)/ε), if f contains polygonal obstacles with a total of n boundary edges; or o(√nµ(f)/ε), if c contains n convex obstacles that are piecewise smooth. in both cases, µ(f) is the volume of f. for the polygonal case, this bound is tight as we can construct a space whose boundary size is θ(√nµ(f)/ε). these results can be partially extended to three dimensions. we show that these results can be applied to the analysis of certain probabilistic roadmap planners, as well as a variant of the art gallery problem. we also propose a number of conjectures on the properties of these highly visible, spaces.
localic sup-lattices and tropological systems. the approach to process semantics using quantales and modules is topologized by considering tropological systems whose sets of states are replaced by locales and which satisfy a suitable stability axiom. a corresponding notion of localic sup-lattice (algebra for the lower powerlocale monad) is described, and it is shown that there are contravariant functors from sup-lattices to localic sup-lattices and, for each quantale q, from left q-modules to localic right q-modules. a proof technique for third completeness due to abramsky and vickers is reset constructively, and an example of application to failures semantics is given.
on the lattice of prefix codes. the natural correspondence between prefix codes and trees is explored, generalizing the results obtained in giammarresi et al. (theoret. comput. sci. 205 (1998) 1459) for the lattice of finite trees under division and the lattice of finite maximal prefix codes. joins and meets of prefix codes are studied in this light in connection with such concepts as finiteness, maximality and varieties of rational languages. decidability results are obtained for several problems involving rational prefix codes, including the solution to the primeness problem.
handsome proof-nets: perfect matchings and cographs. we first extract the combinatorial result behind various proofs of the sequentialisation theorem for multiplicative proof-nets. this result is an inductive characterisation of graphs with a unique perfect matching.extending these techniques, we give a definition of multiplicative proof-nets in which commutativity but also associativity of the multiplicative connectives is interpreted as equality. this is done by representing a sequent by a cograph and axioms by a perfect matching. the main advantage of this presentation is aesthetic: any such graph, without any further requirement is a proof-structure and the correctness criterion also is a natural graph-theoretical property.a direct and purely graph theoretical proof of these results is available as a research report in which more details can be found (c. retoré, handsome proof-nets: r&b-graphs, perfect matchings and series-parallel graphs, rapport de recherche rr-3652, inria, march 1999. http://www.inria.fr/rrrt/publications-eng.html).
semantics and logic of object calculi. the main contribution of this paper is a formal characterization of recursive object specifications and their existence based on a denotational untyped semantics of the object calculus. existence is not guaranteed but can be shown employing pitts' results on relational properties of domains. the semantics can be used to analyse and verify abadi and leino's object logic but it also suggests extensions. for example, specifications of methods may not only refer to fields but also to methods of objects in the store. this can be achieved without compromising the existence theorem. an informal logic of predomains is in use intentionally in order to avoid any commitment to a particular syntax of specification logic.
some results on tries with adaptive branching. we study a modification of digital trees (or tries) with adaptive multi-digit branching. such tries can dynamically adjust degrees of their nodes by choosing the number of digits to be processed per lookup. while we do not specify any particular method for selecting the degrees of nodes, we assume that such selection can be accomplished by examining the number of strings remaining in each sub-tree, and/or estimating parameters of the input distribution. we call this class of digital trees adaptive multi-digit tries (or amd-tries) and provide a preliminary analysis of their expected behavior in a memoryless model. we establish the following results: (1) there exist amd-tries attaining a constant expected time of a successful search; (2) there exist amd-tries consuming a linear (in the number of strings inserted) amount of space; (3) both constant search time and linear space usage can be attained if the (memoryless) source is symmetric. we accompany our analysis with a brief survey of several known types of adaptive trie structures, and show how our analysis extends (and/or complements) previous results.
conjugacy and episturmian morphisms. episturmian morphisms generalize sturmian morphisms. here, we study some intrinsic properties of these morphisms: invertibility, presentation, cancellativity, unitarity, characterization by conjugacy. most of them are generalizations of known properties of sturmian morphisms. but we present also some results on episturmian morphisms that have not already been stated in the particular case of sturmian morphisms: characterization of the episturmian morphisms that preserve palindromes, new algorithms to compute conjugates.we also study the conjugation of morphisms in the general case and show that the monoid of invertible morphisms on an alphabet containing at least three letters is not finitely generated.
some results on k-power-free morphisms. one way to generate infinite k-power-free words is to iterate a k-power-free morphism, that is a morphism that preserves finite k-power-free words. we first prove that the monoid of k-power-free endomorphisms on an alphabet containing at least three letters is not finitely generated. test-sets for k-power-free morphisms (that is, the sets t such that a morphism f is k-power-free if and only if f(t) is k-power-free) give characterizations of these morphisms. in the case of binary morphisms and k=3, we prove that a set t of cube-free words is a test-set for cube-freeness if and only if it contains 12 particular factors. consequently, a morphism f on {a,b} is cube-free if and only if f(aabbababbabbaabaababaabb) is cube-free (length 24 is optimal). another consequence is an unpublished result of leconte: a binary morphism is cube-free if and only if the images of all cube-free words of length 7 are cube-free. when k3, we show that no finite test-set exists for morphisms defined on an alphabet containing at least three letters. in the last part, we show that to generate an infinite cube-free word by iterating a morphism, we do not necessarily need a cube-free morphism. we give a new characterization of some morphisms that generate infinite cube-free words.
online request server matching. in the following paper an alternative online variant of the matching problem in bipartite graphs is presented. it is triggered by a scheduling problem. there, a task is unknown up to its disclosure. however, when a task is revealed, it is not necessary to take a decision on the service of that particular task. on the contrary, an online scheduler has to decide on how to use the current resources. therefore, the problem is called online request server matching (orsm). it differs substantially from the online bipartite matching problem of karp et al. (proc. 22nd annual acm symp. on theory of computing, baltimore, maryland, may 14-16, 1990, acm press, new york, 1990). hence, the analysis of an optimal, deterministic online algorithm for the orsm problem results in a smaller competitive ratio of 1.5. an extension to a weighted bipartite matching problem is also introduced, and results of its investigation are presented. additional concepts for the orsm model (e.g. lookahead, parallel resources, deadlines) are studied. all of these modifications are realized by restrictions on the input structure. decreased competitive ratios are presented for some of these modified models. copyright 2001 elsevier science b.v.
distributed processes and location failures. site failure is an essential aspect of distributed systems; nonetheless its effect on programming language semantics remains poorly understood. to model such systems, we define a process calculus in which processes are run at distributed locations. the language provides operators to kill locations, to test the status (dead or alive) of locations, and to spawn processes at remote locations. using a variation of bisimulation, we provide alternative characterizations of strong and weak barbed congruence for this language, based on an operational semantics that uses congurations to record the status of locations. we then derive a second, symbolic characterization in which configurations are replaced by logical formulae. in the strong case the formulae come from a standard propositional logic, while in the weak case a temporal logic with past time modalities is required. the symbolic characterization establishes that, in principle, barbed congruence for such languages can be checked using existing symbolic techniques. copyright 2001 elsevier science b.v.
semantics of plan revision in intelligent agents. in this paper, we give an operational and denotational semantics for a meta-language of the 3apl agent programming language. with this meta-language, various 3apl interpreters can be programmed. we prove equivalence of the operational and denotational semantics. furthermore, we give an operational semantics for object-level 3apl. using this semantics, we relate the 3apl meta-language to object-level 3apl by providing a specific interpreter, the semantics of which will prove to be equivalent to object-level 3apl.
constant bounds on the moments of the height of binary search trees. we show that binary search trees of a given size tend to have smaller height when the root division is into two subtrees of more balanced sizes. we deduce that the expectation of the absolute value of the difference in height of two binary search trees of the same number of nodes is less than 3.135 infinitely often. we also deduce strong upper bounds on the probability of large deviations from the median. putting together these two conclusions and a simple and plausible conjecture on critical nodes leads to o(1) bounds on all moments of binary search tree heights.
wmso theories as grammar formalisms. we explore the use of weak monadic second-order languages over structures of varying dimension as specification languages for grammars and automata, focusing, in particular, on the extension of the longstanding results characterizing the regular and context-free languages in terms of definability in ws1s (one-dimensional) and wsns (two-dimensional), respectively, to a characterization of the tree-adjoining languages in terms of definability in the weak monadic second-order theory of certain three-dimensional tree-like structures. we then explore the application of these results to aspects of an existing large-scale tree-adjoining grammar for english and close with some speculation on the feasibility of this approach as a means of building and maintaining such grammars.
phase transitions and symmetry breaking in genetic algorithms with crossover. in this paper, we consider the role of the crossover operator in genetic algorithms. specifically, we study optimisation problems that exhibit many local optima and consider how crossover affects the rate at which the population breaks the symmetry of the problem. as an example of such a problem, we consider the subset sum problem. in doing so, we demonstrate a previously unobserved phenomenon, whereby the genetic algorithm with crossover exhibits a critical mutation rate, at which its performance sharply diverges from that of the genetic algorithm without crossover. at this critical mutation rate, the genetic algorithm with crossover exhibits a rapid increase in population diversity. we calculate the details of this phenomenon on a simple instance of the subset sum problem and show that it is a classic phase transition between ordered and disordered populations. finally, we show that this critical mutation rate corresponds to the transition between the genetic algorithm accelerating or preventing symmetry breaking and that the critical mutation rate represents an optimum in terms of the balance of exploration and exploitation within the algorithm.
csp-casl - a new integration of process algebra and algebraic specification. csp-casl integrates the process algebra csp [t. hoare, communicating sequential processes, prentice-hall, englewood cliffs, nj, 1985; a.w. roscoe, the theory and practice of concurrency, prentice-hall, englewood cliffs, nj, 1998] with the algebraic specification language casl [p.d. mosses (ed.), casl reference manual, lecture notes in computer science, vol. 2960, springer, berlin, 2004; e. astesiano, m. bidoit, b. krieg-brückner, h. kirchner, p.d. mosses, d. sannella, a. tarlecki, casl--the common algebraic specification language, theoret. comput. sci. 286 (2002) 153-196]. its novel aspects include the combination of denotational semantics in the process part and, in particular, loose semantics for the data types covering both concepts of partiality and sub-sorting. technically, this integration involves the development of a new so-called data-logic formulated as an institution. this data-logic serves as a link between the institution underlying casl and the alphabet of communications necessary for the csp semantics. besides being generic in the various denotational csp semantics, this construction leads also to an appropriate notion of refinement with clear relations to both data refinement in casl and process refinement in csp.
using data-independence in the analysis of intrusion detection systems. in this paper we demonstrate the modelling and analysis of intrusion detection systems and their environment using the process algebra communicating sequential processes and its model checker fdr. we show that this analysis can be used to discover attack strategies that can be used to blind an intrusion detection system, even a hypothetically perfect one that knows all the weaknesses of its protected host. we give an exhaustive analysis of all such attack possibilities. we discuss how to strengthen the intrusion detection systems to prevent these attacks, and finally we show how we can use data independence techniques to verify the corrected versions.
a principled exploration of coordination models. coordination is a style of interaction in which information exchange among independent system components is accomplished by means of high-level constructs designed to enhance the degree of decoupling among participants. a decoupled mode of computation is particularly important in the design of mobile systems which emerge dynamically through the composition of independently developed components meeting under unpredictable circumstances and thrust into achieving purposeful cooperative behaviors. this paper examines a range of coordination models tailored for use in mobile computing and shows that the constructs they provide are reducible to simple schema definitions in mobile unity. intellectually, this exercise contributes to achieving a better operational-level understanding of the relation among several important classes of models of mobility. pragmatically, this work demonstrates the immediate applicability of mobile unity to the formal specification of coordination constructs supporting mobile computing. moreover, the resulting schemas are shown to be helpful in reducing the complexity of the formal verification effort.
hybrid action systems. in this paper we investigate the use of action systems with differential actions in the specification of hybrid systems. as the main contribution we generalize the definition of a differential action, allowing the use of arbitrary relations over model variables and their time derivatives in modelling continuous-time dynamics. the generalized differential action has an intuitively appealing predicate transformer semantics, which we show to be both conjunctive and monotonic. in addition, we show that differential actions blend smoothly with conventional actions in action systems even under parallel composition. moreover, as the strength of the action system formalism is the support for stepwise development by refinement, we investigate refinement involving a differential action. we show that, due to the predicate transformer semantics, standard action refinement techniques apply also to the differential action, thus, allowing stepwise development of hybrid systems.
the word problem for 1lc congruences is np-hard. in this paper, it is proved that the word problem for congruences generated by subsets of {(abc,acb)|a ∈ a ∪ {ε},b, c ∈ a) is np-hard. these congruences are a generalization of mazurkiewicz's traces.
an algebraic view of the relation between largest common subtrees and smallest common supertrees. the relationship between two important problems in tree pattern matching, the largest common subtree and the smallest common supertree problems, is established by means of simple constructions, which allow one to obtain a largest common subtree of two trees from a smallest common supertree of them, and vice versa. these constructions are the same for isomorphic, homeomorphic, topological, and minor embeddings, they take only time linear in the size of the trees, and they turn out to have a clear algebraic meaning.
behavioral abstraction is hiding information. we show that for any behavioral σ-specification b there is an ordinary algebraic specification b˜ over a larger signature, such that a model behaviorally satisfies b iff it satisfies, in the ordinary sense, the σ-theorems of b˜. the idea is to add machinery for contexts and experiments (sorts, operations and equations), use it, and then hide it. we develop a procedure, called unhiding, which takes a finite b and produces a finite b˜. the practical aspect of this procedure is that one can use any standard equational inductive theorem prover to derive behavioral theorems, even if neither equational reasoning nor induction is sound for behavioral satisfaction.
revision by comparison as a unifying framework: severe withdrawal, irrevocable revision and irrefutable revision. fermé and rott [revision by comparison, art. intell. 157 (2004) 5-47] introduced a binary operation of 'revision by comparison' and pointed out that this method of changing epistemic states has both characteristics of belief contraction (with respect to the 'reference sentence') and characteristics of belief revision (with respect to the 'input sentence'). using revision by comparison as a unifying framework, the present paper studies the unary limiting cases of severe withdrawal, irrevocable revision and irrefutable revision. while variants of the first two operations are well-known from the literature, the last one is new.
differentiable coarse graining. coarse graining is defined in terms of a commutative diagram. necessary and sufficient conditions are given in the continuously differentiable case. the theory is applied to linear coarse grainings arising from partitioning the population space of a simple genetic algorithm (ga). cases considered include proportional selection, binary tournament selection, ranking selection, and mutation. a nonlinear coarse graining for ranking selection is also presented. a number of results concerning "form invariance" are given. within the context of gas, the primary contribution made is the illustration of a technique by which coarse grainings may be analyzed. it is applied to obtain a number of new coarse graining results.
on the computational complexity of longley's h functional. longley discovered a functional h that, when added to pcf, yields a language that computes exactly sr, the sequentially realizable functionals of van oosten. we show that if p ≠ np, then the computational complexity of h (and of similar sr-functionals) is inherently infeasible.
icalp, eatcs and maurice nivat. the purpose of this writing is to tell something about the quite unique and fundamental role of maurice nivat, both in launching icalp and eatcs, as well as in guiding them through the difficult early stages. our account is based on personal recollections, as well as some original documents and letters. to preserve the personal character of our recollections, we have not tried to fill the gaps in our information through other channels such as interviewing some of the people involved. in other words, our personal account is not intended to be a comprehensive history. it only tells how things seemed to us.
dna computing by blocking. we present a method for molecular computing which relies on blocking (inactivating) this part of the total library of molecules that does not contribute to (finding) a solution--this happens essentially in one biostep (after the input has been read). the method is explained by presenting a dna based algorithm for solving (albeit in the theoretical sense only!) the satisfiability problem.
a greedy approximation for minimum connected dominating sets. given a graph, a connected dominating set is a subset of vertices such that every vertex is either in the subset or adjacent to a vertex in the subset and the subgraph induced by the subset is connected. a minimum connected dominating set is such a vertex subset with minimum cardinality. in this paper, we present a new one-step greedy approximation with performance ratio ln δ + 2 where δ is the maximum degree in the input graph. the interesting aspect is that the greedy potential function of this algorithm is not supmodular while all previously known one-step greedy algorithms with similar performance have supmodular potential functions.
exists-universal termination of logic programs. we introduce the notion of $\exists$-universal termination of logic programs. a program p and a goal g $\exists$-universally terminate iff there exists a selection rule s such that every sld-derivation of p u { g }$via s is finite. we claim that it is an essential concept for declarative programming, where a crucial point is to associate a terminating control strategy to programs and goals. we show that $\exists$-universal termination and universal termination via fair selection rules coincide. then we offer a characterization of $\exists$-universal termination by defining fair-bounded programs and goals. they provide us with a correct and complete method of proving $\exists$-universal termination. we show other valuable properties of fair-bounded programs and goals, including persistency, modularity, ease of use in paper & pencil proofs, automatization of proofs. the acm portal is published by the association for computing machinery. copyright © 2010 acm, inc. terms of usage privacy policy code of ethics contact us useful downloads: adobe acrobat quicktime windows media player real player