waashk/dblp huggingface dataset:
deterministic m2m multicast in radio networks. we study the problem of exchanging messages within a fixed group of k nodes, called participants, in an n-node radio network, modeled as an undirected graph. this communication task was previously considered in the setting of atm video applications, in [j.m. tsai, h.-h. fang, c.-y. lee, a multicast solution for atm video applications, ieee trans. circuits systems video technol. 7 (1997) 675-686], and was called multipoint-to-multipoint (m2m) multicasting. while the radio network topology is known to all nodes, it is assumed that no node is aware of the location of the participants. we give a distributed deterministic algorithm for the m2m multicasting problem in radio networks, and analyze its time complexity. we show that if the maximum distance between any two out of k participants is d then this local information exchange problem can be solved in time o(d log2 n + k log4 n).
a truly concurrent semantics for a process algebra using resource pomsets. in this paper we study a process algebra whose semantics is based on true concurrency. in our model, actions are defined in terms of the resources they need to execute, which allows a simple definition of a weak sequential composition operator. this operator allows actions which do not share any resources to execute concurrently, while dependent actions have to occur sequentially. this weak sequential composition operator may be used to automatically parallelize a sequential process. we add the customary (strict) sequential composition and a parallel composition operator allowing synchronization on specified actions. our language also supports a hiding operator that allows the hiding of actions and even of individual resources used by actions. strict sequential composition and hiding require that we generalize from the realm of mazurkiewicz traces to that of pomsets, since these operations introduce "over-synchronized" tracesones for which a pair of independent actions may occur sequentially. our language also supports recursion and our semantics makes the unwinding of recursion visible by the use of special resources used to label unwindings. this is done on purpose in order to make divergence observable, but the usual semantics that does not observe unwindings can be obtained by using the hiding operator to abstract away from these special resources. we give both an sos-style operational semantics for our language, as well as a denotational semantics based on resource pomsets. generalizing results from our earlier work in this area, we derive a congruence theorem for our language which shows that the sos-style operational rules induce the same equivalence relation on the language as the denotational semantic map does. a corollary is that our denotational model is both adequate and fully abstract relative to the behavior function defined from our operational semantics. this behavior consists naturally of the strings of actions the process can perform. this work continues our study into modelling concurrency in the absence of nondeterminism. in particular, our language is deterministic.
resource traces: a domain for processes sharing exclusive resources. the domain of partially terminated finite and infinite words is commonly used to give denotational semantics for process algebras such as csp. in this well-known framework the denotational semantics of concurrency is derived via power-domains from that of non-deterministic choice and interleaving to the effect that the denotational semantics of a concurrent process is equal to the set of all its possible finite and infinite sequential behaviours. in this paper, we define a more versatile domain of the so-called finite and infinite resource traces which allows to capture the concurrent behaviour of a process and encode the static concurrency of a system directly into the domains definition. the approach we present refines the previous work of diekert and gastin (lecture notes in computer science, vol. 944, springer, berlin, pp. 15-26) on - and -traces. we start with an alphabet of atomic actions, a set of resources, and a resource map assigning to each action the non-empty subset of resources it uses. actions that do not share common resources are called independent and considered to be able to execute concurrently. a partially terminated concurrent process is specified by a resource trace which consists of two components: an already observed part represented as an action-labeled partial order (mazurkiewicz trace), and a guard set containing the resources granted to the process for its further development. a process concatenation is then defined, which allows independent actions to execute concurrently. specification refinement leads to a natural approximation ordering between processes. it confers to the set of all processes the structure of a coherently complete prime algebraic scott domain, whereby, process concatenation is scott-continuous in both arguments. furthermore, we define a natural ultrametric on processes based on prefix information. the induced topology is shown to be equivalent to the compact lawson topology induced by the approximation ordering. process concatenation is moreover shown to be uniformly continuous with respect to the defined ultrametric. the mathematical theory we develop thus extends the central order and metric properties of the domain of partially terminated finite and infinite words which are needed in order to devise truly concurrent semantics for process algebras much in the style of classical csp semantics.
fast arithmetic with general gauß periods. we show how to apply fast arithmetic in conjunction with general gauß periods in finite fields. this is an essential ingredient for some efficient exponentiation algorithms.
interval routing in reliability networks. in this paper, we consider routing with compact tables in reliability networks. more precisely, we study interval routing on random graphs g(b, p) obtained from a base graph b by independently removing each edge with a failure probability 1 - p. we focus on additive stretched routing for n-node random graphs for which the base b is a square mesh and p = 0.5, that is the percolation model at the critical phase. we show a lower bound of ω(√log n/(δ+2)) on the number of intervals required per edge for every additive stretch δ≥0. on the other side, our experimental results show that the size of the largest biconnected components is θ(n0.827), and thus that there exists a trivial shortest-path routing scheme using at most o(n0.827) intervals per edge.the results are extended to random meshes of higher dimension. we show that, asymptotically almost surely, the number of intervals per edge for a random r-dimensional mesh with n nodes is ω(16-r (δ + 2)1-r r-4(log n)1-1/r), for every additive stretch δ≥0 and for every integral dimension r ∈ [1, log2n].
on the decidability of termination of query evaluation in transitive-closure logics for polynomial constraint databases. the formalism of constraint databases, in which possibly infinite data sets are described by boolean combinations of polynomial inequality and equality constraints, has its main application area in spatial databases. the standard query language for polynomial constraint databases is first-order logic over the reals. because of the limited expressive power of this logic with respect to queries that are important in spatial data base applications, various extensions have been introduced. we study extensions of first-order logic with different types of transitive-closure operators and we are in particular interested in deciding the termination of the evaluation of queries expressible in these transitive-closure logics. it turns out that termination is undecidable in general. however, we show that the termination of the transitive closure of a continuous function graph in the two-dimensional plane, viewed as a binary relation over the reals, is decidable, and even expressible in first-order logic over the reals. based on this result, we identify a particular transitive-closure logic for which termination of query evaluation is decidable and which is more expressive than first-order logic over the reals. furthermore, we can define a guarded fragment in which exactly the terminating queries of this language are expressible.
converting two-way nondeterministic unary automata into simpler automata. we show that, on inputs of length exceeding 5n2, any n-state unary two-way nondeterministic finite automaton (2nfa) can be simulated by a (2n + 2)-state quasi-sweeping 2nfa. such a result, besides providing a "normal form" for 2nfa's, enables us to get a subexponential simulation of unary 2nfa's by two-way deterministic finite automata (2dfa's). in fact, we prove that any n-state unary 2nfa can be simulated by a sweeping 2dfa with o(n ⌈log2(n+1)+3⌉) states.
more efficient on-the-fly ltl verification with tarjan's algorithm. state-of-the-art algorithms for on-the-fly automata-theoretic ltl model checking make use of nested depth-first search to look for accepting cycles in the product of the system and the büchi automaton. here, we present two new single depth-first search algorithms that accomplish the same task. the first is based on tarjan's algorithm for detecting strongly connected components, while the second is a combination of the first and couvreur's algorithm for finding acceptance cycles in the product of a system and a generalized büchi automaton. both new algorithms report an accepting cycle immediately after all transitions in the cycle have been investigated. we show their correctness, describe efficient implementations and discuss how they interact with some other model checking techniques, such as bitstate hashing. the algorithms are compared to the nested search algorithms in experiments on both random and actual state spaces, using random and real formulas. our measurements indicate that our algorithms investigate at most as many states as the old ones. in the case of a violation of the correctness property, the algorithms often explore significantly fewer states.
scheduling hard sporadic tasks with regular languages and generating functions. in this paper, we consider offline validation of hard real-time systems composed of both periodic and sporadic tasks, embedded on centralized multi-processor architectures. to model hard real-time systems, we use untimed finite automata: each accepted word is a valid operational behavior of the periodic component of the system. then, by associating generating functions with edges of the automaton, we give a modular decisional technique to decide the feasibility of sporadic tasks.
arborescence optimization problems solvable by edmonds' algorithm. we consider a general class of optimization problems regarding spanning trees in directed graphs (arborescences). we present an algorithm for solving such problems, which can be considered as a generalization of edmonds' algorithm for the solution of the minimum sum arborescence problem. the considered class of optimization problems includes as special cases the standard minimum sum arborescence problem, the bottleneck and lexicographically optimal arborescence problem, as well as the widest-minimum sum arborescence problem.
efficient gossip and robust distributed computation. this paper presents an efficient deterministic gossip algorithm for p synchronous, crash-prone, message-passing processors. the algorithm has time complexity t = o(log2p) and message complexity m = o(p1+ε), for any ε > 0. this substantially improves the message complexity of the previous best algorithm that has m = o(p1.77), while maintaining the same time complexity.the strength and utility of the new result is demonstrated by constructing a deterministic algorithm for performing n tasks in this distributed setting. previous solutions used coordinator or checkpointing approaches, immediately incurring a work penalty ω(n + f ċ p) for f crashes, or relied on strong communication primitives, such as reliable broadcast, or had work too close to the trivial θ(p ċ n) bound of oblivious algorithms. the new algorithm uses p crash-prone processors to perform n similar and idempotent tasks so long as one processor remains active. the work of the algorithm is w = o(n + p ċ min{f + 1, log3p}) and its message complexity is m = o(fpepsiv; + p min{f + 1, log p}), for any ε > 0. this substantially improves the work complexity of previous solutions using simple point-to-point messaging, while "meeting or beating" the corresponding message complexity bounds.the new algorithms use communication graphs and permutations with certain combinatorial properties that are shown to exist. the algorithms are correct for any permutations, and in particular, the same expected bounds can be achieved using random permutations.
periodic graphs and connectivity of the rational digital hyperplanes. given a digital hyperplane of zn defined by a double-inequality hi=1naixi<h+, we want to determine whether it is connected. the problem consists of computing the connectivity of a graph whose set of vertices is not finite. the classical algorithms of labelling are not deterministic in this framework but we can think of using the properties of the digital hyperplanes and in particular their periodicity to provide a deterministic method. it leads to introduce a special kind of graphs that we call periodic and whose properties allow to compute connective components of infinite size. it provides a deterministic algorithm determining whether a given rational digital hyperplane is connecte
reduction from three-dimensional discrete tomography to multicommodity flow problem. the reduction from two-dimensional-discrete tomography to max-flow problem is well-known [gale, a theorem on flows in networks, pacific j. math. 7 (1957) 1073-1082]. this approach is based on the natural correspondence between two-dimensional lattices and bipartite graphs. we extend this result in dimension 3 by reducing three-dimensional discrete tomography to multicommodity flow problems. two reductions are presented, one considering discrete tomography with multisets while the other one works with sets.
algorithms for vertex-partitioning problems on graphs with fixed clique-width. many vertex-partitioning problems can be expressed within a general framework introduced by telle and proskurowski. they showed that optimization problems in this framework can be solved in polynomial time on classes of graphs with bounded tree-width. in this paper, we consider a very similar framework, in relationship with more general classes of graphs: we propose a polynomial time algorithm on classes of graphs with bounded clique-width for all the optimization problems in our framework. these classes of graphs are more general than the classes of graphs with bounded tree-width in the sense that classes of graphs with bounded tree-width have also bounded clique-width (but not necessarily the inverse).our framework includes problems such as independent (dominating) set, p-dominating set, induced bounded degree subgraph, induced p-regular subgraph, perfect matching cut, graph k-coloring and graph list-k-coloring with cardinality constraints (fixed k). this paper thus provides a second (distinct) framework within which the optimization problems can be solved in polynomial time on classes of graphs with bounded clique-width, after a first framework (called ms1) due to the work of courcelle, makowsky and rotics (for which they obtained a linear time algorithm).
architecture independent parallel selection with applications to parallel priority queues. we present a randomized selection algorithm whose performance is analyzed in an architecture independent way on the bulk-synchronous parallel (bsp) model of computation along with an application of this algorithm to dynamic data structures, namely parallel priority queues. we show that our algorithms improve previous results upon both the communication requirements and the amount of parallel slack required to achieve optimal performance. we also establish that optimality to within small multiplicative constant factors can be achieved for a wide range of parallel machines. while these algorithms are fairly simple themselves, descriptions of their performance in terms of the bsp parameters is somewhat involved; the main reward of quantifying these complications is that it allows transportable software to be written for parallel machines that fit the model.
an upper bound for the largest lyapunov exponent of a markovian product of nonnegative matrices. we derive an upper bound for the largest lyapunov exponent of a markovian product of nonnegative matrices using markovian type counting arguments. the bound is expressed as the maximum of a nonlinear concave function over a finite-dimensional convex polytope of probability distributions.
the regular-language semantics of second-order idealized a. we explain how recent developments in game semantics can be applied to reasoning about equivalence of terms in a non-trivial fragment of idealized algol (ia) by expressing sets of complete plays as regular languages. being derived directly from the fully abstract game semantics for ia, our model inherits its good theoretical properties; in fact, for second-order ia taken as a stand-alone language the regular language model is fully abstract. the method is algorithmic and formal, which makes it suitable for automation. we show how reasoning is carried out using a meta-language of extended regular expressions, a language for which equivalence is decidable.
syntactic control of concurrency. we consider a finitary procedural programming language (finite data-types, no recursion) extended with parallel composition and binary semaphores. having first shown that may-equivalence of second-order open terms is undecidable we set out to find a framework in which decidability can be regained with minimum loss of expressivity. to that end we define an annotated type system that controls the number of concurrent threads created by terms and give a fully abstract game semantics for the notion of equivalence induced by typable terms and contexts. finally, we show that the semantics of all typable terms, at any order and in the presence of iteration, has a regular-language representation and thus the restricted observational equivalence is decidable.
transforming semantics by abstract interpretation. in 1997, cousot introduced a hierarchy where semantics are related with each other by abstract interpretation. in this field we consider the standard abstract domain transformers, devoted to refine abstract domains in order to include attribute independent and relational information, respectively the reduced product and power of abstract domains, as domain operations to systematically design and compare semantics of programming languages by abstract interpretation. we first prove that natural semantics can be decomposed in terms of complementary attribute independent observables, leading to an algebraic characterization of the symmetric structure of the hierarchy. moreover, we characterize some structural property of semantics, such as their compositionality, in terms of simple abstract domain equations. this provides an equational presentation of most well known semantics, which is parametric on the observable and structural property of the semantics, making it possible to systematically derive abstract semantics, e.g. for program analysis, as solutions of abstract domain equations.
rotation sequences and edge-colouring of binary tree pairs. the famous four-colour problem of planar maps is equivalent, by an optimally fast reduction, to the problem of colouring pairs of binary trees (cpbt). extant proofs of the four colour theorem lack conciseness, are not lucid in their detail and require hours of electronic computation. the search for a more satisfactory proof continues and, in this spirit, we explore one approach to cpbt based upon the rotation operation in binary trees. we prove that a more satisfactory proof exists if a rotational path between the two trees of every problem instance satisfies our non-colour-clashing sequence conjecture.
logical foundations for programming semantics. this paper was presented to the sixth workshop on mathematical foundations of programming semantics held at queen''s university, may 15-19,1990. \n\nthe paper provides an introduction to a natural deduction based set theory, nadset, and illustrates its use in programming semantics. the need for such a set theory for the development of programming semantics is motivated by contrasting the presentation of recursive definitions within first order logic with their presentation within nadset. within first order logic such definitions are always incomplete in a very simple sense: induction axioms must be added to the given definitions and extended with every new recursive definition. within a set theory such as nadset, recursive definitions of sets are represented as terms in the theory and are complete in the sense that all properties of the set can be derived from its definition. such definitions not only have this advantage of completeness, but they also permit recursively defined sets to be members of the universe of discourse of the logic and thereby be shown to be members of other defined sets. \nthe resolution of the paradoxes provided by nadset is dependant upon replacing the naive comprehension axiom scheme of an inconsistent first order logic with natural deduction rules for the introduction of abstraction terms into arguments. the abstraction terms admitted are a generalization of the abstraction terms usually admitted into set theory. in order to avoid a confusion of use and mention, the nominalist interpretation of the atomic formulas of the logic forces nadset to be second order, although only a single kind of quantifier and variable is required. \nthe use of nadset for programming semantics is illustrated for a simple flow diagram language that has been used to illustrate the principles of denotational semantics. the presentation of the semantics within nadset is not only fully formal, in contrast to the simply mathematical presentation of denotational semantics, but because nadset is formalized as a natural deduction logic, its derivations can be simply checked by machine.
an asymptotic study for path reversal. a path reversal is performed in a rooted tree when a node becomes the root of all the nodes along the path from it to the former root. this algorithm on trees is presented as a transition system specified by induction over a convenient view of the tree structure. when each tree node is assigned a fixed weight representing its relative probability to move to the root, the transition system defines a finite markov chain. this paper presents some of its asymptotic properties. a closed formula for the stationary distribution and a tight upper bound for the average computational complexity of path reversal are also given as new results.
on the expressiveness of higher dimensional automata. in this paper i compare the expressive power of several models of concurrency based on their ability to represent causal dependence. to this end, i translate these models, in behaviour preserving ways, into the model of higher dimensional automata (hda), which is the most expressive model under investigation. in particular, i propose four different translations of petri nets, corresponding to the four different computational interpretations of nets found in the literature.i also extend various equivalence relations for concurrent systems to hda. these include the history preserving bisimulation, which is the coarsest equivalence that fully respects branching time, causality and their interplay, as well as the st-bisimulation, a branching time respecting equivalence that takes causality into account to the extent that it is expressible by actions overlapping in time. through their embeddings in hda, it is now well-defined whether members of different models of concurrency are equivalent.