waashk/dblp huggingface dataset:
well-behaved flow event structures for parallel composition and action refinement. flow event structures were introduced as a model for giving semantics to process algebras. however, it turned out that certain restrictions have to be made to make them suitable for this purpose. in this paper, we investigate subclasses of flow event structures which are both suited for the process algebraic composition operators, and for action refinement as a means of regarding processes on different levels of abstraction.first, suitable subclasses are characterised. then two specific subclasses are proposed. the larger class generalises the one from castellani and zhang (theoret. comput. sci. 179 (1997) 203-215), which is not suitable for action refinement. the smaller one is still sufficiently expressive for dealing with all standard process algebras and action refinement.
formal description and analysis of a distributed location service for mobile ad hoc networks. in this paper, we define a distributed abstract state machine (dasm) model of the network or routing layer protocol for mobile ad hoc networks. in conjunction with the chosen routing strategy, we propose a distributed logical topology based location service (ltls) protocol and give a formal description and analysis of this protocol on the dasm model. the high dynamics of mobile ad hoc networks require routing strategies substantially different from those used in static communication networks. a strategy for such networks is geographic routing in which each network node can find its physical location via gps or other navigation technologies. to send a packet, the sender needs to know the most recent physical location of the destination node. this location information is provided by a location service protocol. the ltls protocol has short message delivery delay, requires small routing tables, uses relatively few administrative packets, and has very good fault tolerance properties. our goal in defining the network layer protocol in terms of a dasm model is twofold. first, we feel that the mathematical modeling paradigm of distributed abstract state machines provides an ideal formal basis for constructing, analyzing, and validating abstract requirements specifications of mobile ad hoc network protocols. second, we intend to utilize the resulting behavior model as a formal basis for developing executable specifications serving as a platform for experimental validation of key system attributes and exploration of alternative design choices.
occurrences of palindromes in characteristic sturmian words. this paper is concerned with palindromes occurring in characteristic sturmian words cα of slope α, where α ∈ (0, 1) is an irrational. as cα is a uniformly recurrent infinite word, any (palindromic) factor of cαoccurs infinitely many times in cα with bounded gaps. our aim is to completely describe where palindromes occur in cα. in particular, given any palindromic factor u of cα, we shall establish a decomposition of cα with respect to the occurrences of u. such a decomposition shows precisely where u occurs in cα, and this is directly related to the continued fraction expansion of α.
what is the coalgebraic analogue of birkhoff's variety theorem? logical definability is investigated for certain classes of coalgebras related to state-transition systems, hidden algebras and kripke models. the filter enlargement of a coalgebra a is introduced as a new coalgebra a+ whose states are special "observationally rich" filters on the state set of a. the ultra filter enlargement is the subcoalgebra a* of a+ whose states are ultrafilters. boolean combinations of equations between terms of observable (or output) type are identified as a natural class of formulas for specifying properties of coalgebras. these observable formulas are permitted to have a single-state variable, and form a language in which modalities describing the effects of state transitions are implicitly present. a* and a+ validate the same observable formulas. it is shown that a class of coalgebras is definable by observable formulas iff the class is closed under disjoint unions, images of bisimulations, and (ultra)filter enlargements. (closure under images of bisimulations is equivalent to closure under images and domains of coalgebraic morphisms.) moreover, every set of observable formulas has the same models as some set of conditional equations. examples are constructed to show that the use of enlargements is essential in these characterisations, and that there are classes of coalgebras definable by conditional observable equations, but not by equations alone. the main conclusion of the paper is that to structurally characterise classes of coalgebras that are logically definable by modal languages requires a new construction, of "stone space" type, in addition to the coalgebraic duals of the three constructions (homomorphisms, subalgebras, direct products) that occur in birkhoff's original variety theorem for algebras. copyright 2001 elsevier science b.v.
on learning unions of pattern languages and tree patterns in the mistake bound model. we present efficient on-line algorithms for learning unions of a constant number of tree patterns, unions of a constant number of one-variable pattern languages, and unions of a constant number of pattern languages with fixed length substitutions. by fixed length substitutions we mean that each occurrence of variable xi must be substituted by terminal strings of fixed length l(xi). we prove that if arbitrary unions of pattern languages with fixed length substitutions can be learned efficiently then dnfs are efficiently learnable in the mistake bound model. since we use a reduction to winnow, our algorithms are robust against attribute noise. furthermore, they can be modified to handle concept drift. also, our approach is quite general and we give results to learn a class that generalizes pattern languages.
1-optimality of static bsp computations: scheduling independent chains as a case study. the aim of this work is to study a specific scheduling problem under the machine-independent model bsp. the problem of scheduling a set of independent chains in this context is shown to be a difficult optimization problem, but it can be easily approximated in practice. efficient heuristics taking into account communications are proposed and analyzed in this paper. we particularly focus on the influence of synchronization between consecutive supersteps. a family of algorithms is proposed with the best possible load-balancing. then, a strategy for determining a good compromise between the two opposite criteria of minimizing the number of supersteps and a good balance of the load is derived. finally, a heuristic which considers the influence of the latency is presented. simulations of a large number of instances have been carried out to complement the theoretical worst case analysis. they confirm the very good behavior of the algorithms on the average cases.
pattern statistics and vandermonde matrices. in this paper, we determine some limit distributions of pattern statistics in rational stochastic models. we present a general approach to analyze these statistics in rational models having an arbitrary number of strongly connected components. we explicitly establish the limit distributions in most significant cases; they are characterized by a family of unimodal density functions defined by means of confluent vandermonde matrices.
a combinatorial approach to golomb forests. optimal binary prefix-free codes for infinite sources with geometrically distributed frequencies, e.g., p = {pi(1 - p)}i=0; 0p1, were first (implicitly) suggested by golomb over 30 years ago in the context of run-length encodings. ten years later gallager and van voorhis exhibited such optimal codes for all values of p. these codes were derived by using the hu2man encoding algorithm to build optimal codes for finite sources and then showing that the finite codes converge in a very specific sense to the infinite one. in this note, we present a new combinatorial approach to solve the same problem, one that does not use the hu2man algorithm, but instead treats a coding tree as an infinite sequence of integers and derives properties of the sequence. one consequence of this new approach is a complete characterization of all of the optimal codes; in particular, it shows that for all p; 0p1; except for an easily describable countable set, there is a unique optimal code, but for each p in this countable set there are an uncountable number of optimal codes. another consequence is a derivation of infinite codes for geometric sources when the encoding alphabet is no longer restricted to be the binary one. a final consequence is the extension of the results to optimal forests instead of being restricted to optimal trees.
tuning evaluation functions by maximizing concordance. heuristic search effectiveness depends directly upon the quality of heuristic evaluations of states in a search space. given the large amount of research effort devoted to computer chess throughout the past half-century, insufficient attention has been paid to the issue of determining if a proposed change to an evaluation function is beneficial.we argue that the mapping of an evaluation function from chess positions to heuristic values is of ordinal, but not interval scale. we identify a robust metric suitable for assessing the quality of an evaluation function, and present a novel method for computing this metric efficiently. finally, we apply an empirical gradient-ascent procedure, also of our design, over this metric to optimize feature weights for the evaluation function of a computer-chess program. our experiments demonstrate that evaluation function weights tuned in this manner give equivalent performance to hand-tuned weights.
shuffle on positive varieties of languages. we show there is a unique maximal positive variety of languages which does not contain the language (ab)*. this variety is the unique maximal positive variety satisfying the two following conditions: it is strictly included in the class of rational languages and is closed under the shuffle operation. it is also the largest proper positive variety closed under length preserving morphisms. the ordered monoids of the corresponding variety of ordered monoids are characterized as follows: for every pair (a,b) of mutually inverse elements, and for every element z of the minimal ideal of the submonoid generated by a and b, (abzab)ω ≤ ab. in particular this variety is decidable.
complexity of pairwise shortest path routing in the grid. in parallel and distributed systems many communications take place concurrently. the efficient delivery of all the messages depends on the routing algorithms as well as the underlying interconnection network topology. the grid is a planar network topology that lends itself for efficient vlsi implementation and therefore is of interest for theoretical analysis. frequently, networks and switches achieve high performance by delivering the messages through shortest paths. in addition, network fault tolerance improves through insuring that the traversed paths are both edge and/or node disjoint. the edge disjoint criterion is useful when network links are the predominant constraint, and the node disjoint criterion becomes important when switches are the fault tolerant bottleneck. because the latter necessarily implies the former, it is apparent that node disjointness contributes to fault tolerance and enhanced performance. in this paper, we examine the k-pairwise node and edge disjoint shortest paths problem in the undirected graph topology of the grid. herein it is shown that the k-pairwise node as well as the k-pairwise edge disjoint shortest paths decision problems are np-hard, and remain np-hard even for many different restrictions on the problem. we also discuss polynomial time algorithms for restricted versions of our problems.
complete axiomatization and decidability of alternating-time temporal logic. alternating-time temporal logic (atl), introduced by alur, henzinger and kupferman, is a logical formalism for the specification and verification of open systems involving multiple autonomous players (agents, components). in particular, this logic allows for the explicit expression of coalition abilities in such systems, modelled as infinite transition games between the coalition and its complement.formally, atl is a non-normal multi-modal extension of ctl (regarded as a one-player fragment of atl) with temporal operators indexed by coalitions of players, and thus expressing selective quantification over those paths which can be effected as outcomes of infinite transition games between the coalition and its complement.we present a sound and complete axiomatization of the logic atl, based on pauly's axiomatization of his coalition logic, augmented with axioms and rules for fixed point formulae characterizing the temporal operators. the completeness proof is by construction of a bounded branching tree model for each atl-consistent formula. these models can be folded into finite models, thus rendering the finite model property for atl.we also describe an automata-based decision procedure for atl by translating the satisfiability problem to the nonemptiness problem for alternating automata on infinite trees. when considering formulae over a fixed finite set of players the decidability problem is shown to be exptime-complete.
typing correspondence assertions for communication protocols. woo and lam propose correspondence assertions for specifying authenticity properties of security protocols. prior work on checking correspondence assertions depends on model-checking and is limited to finite-state systems. we propose a dependent type and effect system for checking correspondence assertions. since it is based on type-checking, our method is not limited to finite-state systems. this paper presents our system in the simple and general setting of the π-calculus. we show how to type-check correctness properties of example communication protocols based on secure channels. in a related paper, we extend our system to the more complex and specific setting of checking cryptographic protocols based on encrypted messages sent over insecure channels.
dls-trees: a model of evolutionary scenarios. we present a model of evolution of gene trees in the context of species evolution. its concept is similar to reconciliation models. we assume that the gene evolution is modelled by duplications and losses. evolution of species is modelled by speciation events. we define an evolutionary scenario (called a dls-tree) which can represent an evolution of genes in species. we are interested in all scenarios for a given species tree and a given gene tree--not only parsimonious ones. we propose a rewrite system for transforming the scenarios. we prove that the system is confluent, sound and strongly normalizing. we show that a scenario in normal form (i.e., non-reducible) is unique and minimal in the sense of the cost computed as the total number of gene duplications and losses (mutation cost). we present a classification of the scenarios and analyze their hierarchy. finally, we prove that the reconciled tree can be easily transformed into dls-tree in normal form. this solves some open problems for reconciled trees.
an abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations. we extend the framework of comini et al. (inform. comput. (1999), to appear) in order to be able to reason on properties (of abstractions) of possibly infinite sld-derivations. this issue is relevant since some important operational properties such as finite failure, infinite behavior can only be addressed as abstraction of finite and infinite sld-derivations. the framework allows us to define new fixpoint semantics correctly modelling such properties and address problems such as compositionality w.r.t. various syntactic operators, correctness and minimality of the chosen denotations. in this paper we also apply the framework in order to obtain a new fixpoint semantics, based on a co-continuous operator, which correctly models finite failure and is compositional w.r.t. the syntactic operators.
a theory of processes with durational actions. a new bisimulation-based semantics, called performance equivalence, is proposed for a process algebra equipped with tcsp parallel operator. this semantics relies on the basic assumption that actions are time-consuming, where their duration is statically fixed. performance equivalence equates systems whenever they perform the same actions in the same amount of time, thus introducing a simple form of performance evaluation in process algebras. a comparison with other equivalences is provided; in particular, we show that performance equivalence is strictly finer than step bisimulation equivalence and strictly coarser than partial ordering bisimulation equivalence.
asymmetry in -center variants. this paper explores three concepts: the k-center problem, some of its variants, and asymmetry. the k-center problem is fundamental in location theory. variants of k-center may more accurately model real-life problems than the original formulation. asymmetry is a significant impediment to approximation in many graph problems, such as k-center, facility location, k-median, and the tsp.we give an o(log*n)-approximation algorithm for the asymmetric weighted k-center problem. here, the vertices have weights and we are given a total budget for opening centers. in the p-neighbor variant each vertex must have p (unweighted) centers nearby: we give an o(log*k)-bicriteria algorithm using 2k centers, for small p.finally, we show the following three versions of the asymmetric k-center problem to be inapproximable: priority k-center, k-supplier, and outliers with forbidden centers.
computing logcfl certificates. the complexity class logcfl consists of all languages (or decision problems) which are logspace reducible to a context-free language. since logcfl is included in ac1, the problems in logcfl are highly parallelizable. by results of ruzzo (jcss 21 (1980) 218), the complexity class logcfl can be characterized as the class of languages accepted by alternating turing machines (atms) which use logarithmic space and have polynomially sized accepting computation trees. we show that for each such atm m recognizing a language a in logcfl, it is possible to construct an llogcfl transducer tm such that tm on input w &&egr; a outputs an accepting tree for m on w. it follows that computing single logcfl certificates is feasible in functional ac1 and is thus highly parallelizable.wanke (j. algorithms 16 (1994) 470) has recently shown that for any fixed k, deciding whether the treewidth of a graph is at most k is in the complexity-class logcfl. as an application of our general result, we show that the task of computing a tree-decomposition for a graph of constant treewidth is in functional logcfl, and thus in ac1. we also show that the following tasks are all highly parallelizable: computing a solution to an acyclic constraint satisfaction problem; computing an m-coloring for a graph of bounded treewidth; computing the chromatic number and minimal colorings for graphs of bounded tree- width.
enumeration of symmetry classes of convex polyominoes on the honeycomb lattice. we enumerate the symmetry classes of convex polyominoes on the hexagonal (honeycomb) lattice. here convexity is to be understood as convexity along the three main column directions. we deduce the generating series of free (i.e. up to reflection and rotation) and of asymmetric convex hexagonal polyominoes, according to area and half-perimeter. we give explicit formulas or implicit functional equations for the generating series, which are convenient for computer algebra. thus, computations can be carried out up to area 70.
on the completeness and decidability of duration calculus with iteration. the extension of the duration calculus (dc) by iteration, which is also known as kleene star, enables the straightforward specification of repetitive behaviour in dc and facilitates the translation of design descriptions between dc, timed regular expressions and timed automata. in this paper we present axioms and a proof rule about iteration in dc. we consider abstract-time dc and its extension by a state-variable binding existential quantifier known as higher-order dc (hdc). we show that the ω-complete proof systems for dc and hdc known from our earlier work can be extended by our axioms and rule in various ways in order to axiomatise iteration completely. the additions we propose include either the proof rule or an induction axiom. we also present results on the decidability of a subset of the extension dc* of dc by iteration.
distribution results for low-weight binary representations for pairs of integers. we discuss an optimal method for the computation of linear combinations of elements of abelian groups, which uses signed digit expansions. this has applications in elliptic curve cryptography. we compute the expected number of operations asymptotically (including a periodically oscillating second order term) and prove a central limit theorem. apart from the usual right-to-left (i.e., least significant digit first) approach we also discuss a left-to-right computation of the expansions. this exhibits fractal structures that are studied in some detail.
combinatorics of geometrically distributed random variables: run statistics. for words of length n, generated by independent geometric random variables, we consider the mean and variance, and thereafter the distribution of the number of runs of equal letters in the words. in addition, we consider the mean length of a run as well as the length of the longest run over all words of length n.
parsing mell proof nets. we propose a new formulation for full (weakening and constants included) multiplicative and exponential (mell) proof nets, allowing a complete set of rewriting rules to parse them. the recognizing grammar defined by such a rewriting system (confluent and strong normalizing on the new proof nets) gives a correctness criterion that we show equivalent to the danos-regnier one.
sorting algorithms for broadcast communications: mathematical analysis. we study three algorithms for sorting under the broadcast communication model. two algorithms are based on the maximum finding and the loser selection strategy, the third one is the naïve strategy based on loser selection only. while a precise description of the algorithms can be found in the paper [15], we concentrate here on the mathematical aspects of the analysis. from these elementary considerations it follows that the average time complexities of the non-naïve algorithms are θ(n). we give precise expressions for the constants involved by writing them as contour integrals involving zeta functions. the numerical evaluation via residues leads to slowly converging series, and the acceleration of them is a non-trivial task that is done in a slightly more general fashion in order to fit all the applications.
coherence for sharing proof-nets. sharing graphs are an implementation of linear logic proof-nets in which a redex is never duplicated. in their usual formulation, sharing graphs present a problem of coherence: if the proof-net n reduces by standard cut-elimination to n', then, by reducing the sharing graph of n we do not obtain the sharing graph of n'. we solve this problem by changing the way the information is coded into sharing graphs and introducing a new reduction rule (absorption). the rewriting system is confluent and terminating. the proof exploits an algebraic semantics for sharing graphs.