waashk/dblp huggingface dataset:
symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures. most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. examples of such sets of operators comprise xor, multiplication, abstract encryption/decryption. in this report we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. this is the case for most of the intruder theories for which a decision procedure has been given. in particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.
alternating states for dual nondeterminism in imperative programming. the refinement calculus of back, morgan, morris, and others is based on monotone predicate transformers (weakest preconditions) where conjunctions stand for demonic choices between commands and disjunctions for angelic choices. arbitrary monotone predicate transformers cannot be modelled by relational semantics but can be modelled by so-called multirelations. results of morris indicate, however, that the natural domain for the combination of demonic and angelic choice is the free distributive completion (fdc) of the state space. the present paper provides a new axiomatization and more explicit construction of the fdc of an arbitrary ordered set. the fdc concept is self-dual, but the construction is not. we therefore determine the duality function from the fdc to the dual of the fdc of the dual ordered set. the elements of the fdc are classified according to their conjunctivity and disjunctivity. the theory is applied to imperative programming with operators for sequential composition and demonic and angelic choice. the theory based on the fdc is shown to be equivalent to a weakest precondition theory for up-closed predicates. if the order is discrete (i.e., the equality relation), the fdc turns out to be the domain of the choice semantics of back and von wright, whereas up-closed multirelations are functions towards this domain.
parameterized algorithms for d-hitting set: the weighted case. we are going to analyze search tree algorithms for weightedd-hitting set. although the algorithms that we develop are fairly simple, their analysis is technically involved. we compare the weighted case with the previously analyzed unweighted one, exhibiting that the advantage of the unweighted case dwindles with growing d.
on decision problems for parameterized machines. in this paper, we investigate various decision problems concerning parameterized versions of some classes of machines. let c(s,m,t) be the class of nondeterministic multitape turing machine (tm) acceptors with a two-way read-only input, at most s states, at most m read-write worktapes, and at most t symbols in the worktape alphabet, where s,m,t are fixed positive integers. there is no restriction on the cardinality of the input alphabet. we are able to show the emptiness, disjointness, and universe (also called universality) problems to be decidable for c(s,m,t). for the class consisting of machines in c(s,m,t) that always halt or whose minimal-time accepting computations can be bounded by some recursive function f(n) (where n is the input length), the containment and equivalence problems are decidable. these results hold for other machines, e.g., when the worktapes are pushdown stacks (where on every step, each pushdown can only pop the top of the stack or replace the top of the stack by at most two symbols) or when stacks are counters (where on every step, a counter can be incremented by 1, decremented by 1, or remain unchanged, and can be tested for zero). our results are the best possible in the sense that not parameterizing one of s,m,t (or, in the case of counter machines, allowing the counters to increment by arbitrary integers that may change from machines to machines) makes the universe problem undecidable. we also give a simple characterization of the languages defined by c(s,m,t). finally, we investigate the applicability of our techniques to machines with multiple input heads or multiple input tapes.
non-cooperative facility location and covering games. we consider a general class of non-cooperative games related to combinatorial covering and facility location problems. a game is based on an integer programming formulation of the corresponding optimization problem, and each of the k players wants to satisfy a subset of the constraints. for that purpose, resources available in integer units must be bought, and their cost can be shared arbitrarily between players. we consider the existence and cost of exact and approximate pure-strategy nash equilibria. in general, the prices of anarchy and stability are in @q(k) and deciding the existence of a pure nash equilibrium is np-hard. under certain conditions, however, cheap nash equilibria exist, in particular if the integrality gap of the underlying integer program is 1, or in the case of single constraint players. we also present algorithms that compute simultaneously near-stable and near-optimal approximate nash equilibria in polynomial time.
playing monotone games to understand learning behaviors. we deal with a special class of games against nature which correspond to subsymbolic learning problems where we know a local descent direction in the error landscape but not the amount gained at each step of the learning procedure. namely, alice and bob play a game where the probability of victory grows monotonically by unknown amounts with the resources each employs. for a fixed effort on alice's part bob increases his resources on the basis of the results of the individual contests (victory, tie or defeat). quite unlike the usual ones in game theory, his aim is to stop as soon as the defeat probability goes under a given threshold with high confidence. we adopt such a game policy as an archetypal remedy to the general overtraining threat of learning algorithms. namely, we deal with the original game in a computational learning framework analogous to the probably approximately correct formulation. therein, a wise use of a special inferential mechanism (known as twisting argument) highlights relevant statistics for managing different trade-offs between observability and controllability of the defeat probability. with similar statistics we discuss an analogous trade-off at the basis of the stopping criterion of subsymbolic learning procedures. as a conclusion, we propose a principled stopping rule based solely on the behavior of the training session, hence without distracting examples into a test set.
minimizing the makespan on a single parallel batching machine. in this paper, we consider the problem of scheduling with release dates and rejection on a single parallel batching machine, where the jobs have non-identical sizes. our objective is to minimize the makespan of the accepted jobs plus the total penalty of the rejected jobs. first, we give a polynomial time approximation scheme (ptas) for the case where jobs can be split. then, we propose a 2-approximation algorithm for the special case with identical release dates. finally, we present an approximation algorithm for the general problem with worst-case ratio 2+@e, where @e>0 is an arbitrarily small constant.
rotations in the stable b-matching problem. this paper deals with the stable b-matching problem on general multigraphs. we generalize the notion of singular and dual rotations and establish a one-one correspondence between stable b-matchings and certain sets of rotations. this correspondence is used to find all stable edges and a minimum regret stable b-matching in polynomial time. we also recall the np-completeness of the egalitarian stable b-matching problem.
efficient enumeration of all ladder lotteries and its application. a ladder lottery, known as ''amidakuji'' in japan, is a common way to choose a permutation randomly. a ladder lottery l corresponding to a given permutation @p is optimal if l has the minimum number of horizontal lines among the ladder lotteries corresponding to @p. in this paper we show that for any two optimal ladder lotteries l"1 and l"2 of a permutation, there exists a sequence of local modifications which transforms l"1 into l"2. we also give an algorithm to enumerate all optimal ladder lotteries of a given permutation. by setting @p=(n,n-1,...,1), the algorithm enumerates all arrangements of n pseudolines efficiently. by implementing the algorithm we compute the number of arrangements of n pseudolines for each n@?11.
infinite labeled trees: from rational to sturmian trees. this paper studies infinite unordered d-ary trees with nodes labeled by {0,1}. we introduce the notions of rational and sturmian trees along with the definitions of (strongly) balanced trees and mechanical trees, and study the relations among them. in particular, we show that (strongly) balanced trees exist and coincide with mechanical trees in the irrational case, providing an effective construction. such trees also have a minimal factor complexity, hence are sturmian. we also give several examples illustrating the inclusion relations between these classes of trees.
arrows for secure information flow. this paper presents an embedded security sublanguage for enforcing information-flow policies in the standard haskell programming language. the sublanguage provides useful information-flow control mechanisms including dynamic security lattices, run-time code privileges and declassification all without modifying the base language. this design avoids the redundant work of producing new languages, lowers the threshold for adopting security-typed languages, and also provides great flexibility and modularity for using security-policy frameworks. the embedded security sublanguage is designed using a standard combinator interface called arrows. computations constructed in the sublanguage have static and explicit control-flow components, making it possible to implement information-flow control using static-analysis techniques at run time, while providing strong security guarantees. this paper presents a formal proof that our embedded sublanguage provides noninterference, a concrete haskell implementation and an example application demonstrating the proposed techniques.
on the expressiveness of interaction. subbisimilarity is proposed as a general tool to classify the relative expressive power of process calculi. the expressiveness of several variants of ccs is compared in terms of the subbisimilarity relationship. similar investigation is also carried out for the variants of the pi calculus. the relative expressiveness of the different forms of the choice operation and the different ways of introducing infinite behaviors are systematically studied in both the frameworks of ccs and pi. some issues concerning the expressiveness of both ccs and pi are clarified. several open problems are solved along the way. the subbisimilarity approach and the relative expressiveness results are applied to show the independence of the operators of the pi calculus. the definition of the subbisimilarity relationship can be further strengthened with computational requirement, leading to a uniform treatment of computation and interaction.
transducers for the bidirectional decoding of prefix codes. we construct a transducer for the bidirectional decoding of words encoded by the method introduced by girod (1999) in [5] and we prove that it is bideterministic and that it can be used both for the left-to-right and the right-to-left decoding. we also give a similar construction for a transducer that decodes in both directions words encoded by a generalization of girod's encoding method. we prove that it has the same properties as those of the previous transducer. in addition we show that it has a single initial/final state and that it is minimal.
bounded sequence testing from deterministic finite state machines. the w- andwp-methods are the basis for conformance testing from a deterministic finite state machine (dfsm) when the conformance relation considered is equivalence. however, many dfsm applications use only input sequences of limited length. in such cases, the test data only need to establish that the implementation under test produces the specified responses for sequences of length less than or equal to the upper bound l. this paper extends the w- and wp-methods to the case in which only bounded sequences are allowed. the methods for bounded sequences are stronger than the originals since test suites for the unbounded case can be obtained as a particular case (in which the upper bound l is sufficiently large) from the new formulae. furthermore, the generalization is not straightforward as it is not sufficient to extract the sequences of length at most l from the test suites produced in the unbounded case, or even all prefixes of length at most l of the original test sequences. the practicality of the methods is also improved in comparison to the unbounded case: the size of the test suites may be considerably reduced while the complexity of the test generation algorithms remains basically unchanged.
average long-lived binary consensus: quantifying the stabilizing role played by memory. consider a system composed of n sensors operating in synchronous rounds. in each round an input vector of sensor readings x is produced, where the i-th entry of x is a binary value produced by the i-th sensor. the sequence of input vectors is assumed to be smooth: exactly one entry of the vector changes from one round to the next one. the system implements a fault-tolerant averaging consensus functionf. this function returns, in each round, a representative output valuev of the sensor readings x. assuming that at most t entries of the vector can be erroneous, f is required to return a value that appears at least t+1 times in x. we introduce the definition of instability of the system, which consists in the number of output changes over a random sequence of input vectors. we first design optimal (with respect to the instability measure) consensus systems: d"0 without memory, and d"1 with memory. then we quantify the gain factor due to memory by computing c"n(t), the number of decision changes performed by d"0 per decision change performed by d"1.
accepting splicing systems. in this paper, we propose a novel approach to splicing systems, namely we consider them as accepting devices. two ways of iterating the splicing operation and two variants of accepting splicing system are investigated. altogether, we obtain four models, which are compared with each other as well as with the generating splicing systems from the computational power point of view. several decision problems concerning the accepting splicing systems are discussed.
an operational semantics for a calculus for wireless systems. in wireless systems, the communication mechanism combines features of broadcast, synchrony, and asynchrony. we develop an operational semantics for a calculus of wireless systems. we present different reduction semantics and a labelled transition semantics and prove correspondence results between them. finally, we apply cws to the modelling of the alternating bit protocol, and prove a simple correctness result as an example of the kind of properties that can be formalized in this framework. a major goal of the semantics is to describe the forms of interference among the activities of processes that are peculiar of wireless systems. such interference occurs when a location is simultaneously reached by two transmissions. the reduction semantics differ on how information about the active transmissions is managed. we use the calculus to describe and analyse a few properties of a version of the alternating bit protocol.
hyperbolicity of the fixed point set for the simple genetic algorithm. we study an infinite population model for the genetic algorithm, where the iteration of the algorithm corresponds to an iteration of a map g. the map g is a composition of a selection operator and a mixing operator, where the latter models effects of both mutation and crossover. we examine the hyperbolicity of fixed points of this model. we show that for a typical mixing operator all the fixed points are hyperbolic.
computing the graph-based parallel complexity of gene assembly. we consider a graph-theoretical formalization of the process of gene assembly in ciliates introduced in ehrenfeucht et al. (2003) [3], where a gene is modeled as a signed graph. the gene assembly, based on three types of operations only, is then modeled as a graph reduction process (to the empty graph). motivated by the robustness of the gene assembly process, the notions of parallel reduction and parallel complexity of signed graphs have been considered in harju et al. (2006) [7]. we describe in this paper an exact algorithm for computing the parallel complexity of a given signed graph and for finding an optimal parallel reduction for it. checking the parallel applicability of a given set of operations and scanning all possible selections amount to a high computational complexity. we also briefly discuss a faster approximate algorithm that however, cannot guarantee finding the optimal reduction.
euclidean tsp on two polygons. we give an o(n^2m+nm^2+m^2logm) time and o(n^2+m^2) space algorithm for finding the shortest traveling salesman tour through the vertices of two simple polygonal obstacles in the euclidean plane, where n and m are the number of vertices of the two polygons. by obstacle, we mean that the tour may not cross between the interior and exterior of either polygon. we also consider the problem's extension to higher dimensions, proving that, if p
hybrid automata, reachability, and systems biology. hybrid automata are a powerful formalism for the representation of systems evolving according to both discrete and continuous laws. unfortunately, undecidability soon emerges when one tries to automatically verify hybrid automata properties. an important verification problem is the reachability one that demands to decide whether a set of points is reachable from a starting region. if we focus on semi-algebraic hybrid automata the reachability problem is semi-decidable. however, high computational costs have to be afforded to solve it. we analyse this problem by exploiting some existing tools and we show that even simple examples cannot be efficiently solved. it is necessary to introduce approximations to reduce the number of variables, since this is the main source of runtime requirements. we propose some standard approximation methods based on taylor polynomials and ad hoc strategies. we implement our methods within the software saha-tool and we show their effectiveness on two biological examples: the repressilator and the delta-notch protein signaling.
on the complexity of finding chordless paths in bipartite graphs and some interval operators in graphs and hypergraphs. in this paper we show that the problem of finding a chordless path between a vertex s and a vertex t containing a vertex v remains np-complete in bipartite graphs, thereby strengthening the previous results on the same problem. we show a relation between this problem and two interval operators: the simple path interval operator in hypergraphs and the even-chorded path interval operator in graphs. we show that the problem of computing the two mentioned intervals is np-complete.
translating propositional extended conjunctions of horn clauses into boolean circuits. horn^@? is a logic programming language which extends usual horn clauses by adding intuitionistic implication in goals and clause bodies. this extension can be seen as a way of structuring programs in logic programming. we are interested in finding correct and efficient translations from horn^@? programs into some representation type that, preserving the signature, allows us suitable implementations of these kinds of programs. in this paper we restrict to the propositional setting of horn^@? and we study correct translations into boolean circuits, i.e. graphs; into boolean formulas, i.e. trees; and into conjunctions of propositional horn clauses. different results for the efficiencies of the transformations are obtained in the three cases.
quantum circuit oracles for abstract machine computations. this paper considers a very general model of computation via conditional iteration, the abstract machines of hines (2008) [23], and studies the conditions under which these describe reversible computations. using this, we demonstrate how to construct quantum circuits that act as oracles for these abstract machines. for a classical computation with worst-case performance t, the resulting quantum circuit requires an ancilla of 1+log(t) qubits, and takes o(t) steps. the ancilla starts and finishes in the constant state |0>, so garbage collection is performed automatically.
the complexity of the hajós calculus for planar graphs. the planar hajos calculus is the hajos calculus with the restriction that all the graphs that appear in the construction (including a final graph) must be planar. we prove that the planar hajos calculus is polynomially bounded iff the hajos calculus is polynomially bounded.
chromatic index of graphs with no cycle with a unique chord. the class c of graphs that do not contain a cycle with a unique chord was recently studied by trotignon and vuskovic (in press) [23], who proved for these graphs strong structure results which led to solving the recognition and vertex-colouring problems in polynomial time. in the present paper, we investigate how these structure results can be applied to solve the edge-colouring problem in the class. we give computational complexity results for the edge-colouring problem restricted to c and to the subclass c^' composed of the graphs of c that do not have a 4-hole. we show that it is np-complete to determine whether the chromatic index of a graph is equal to its maximum degree when the input is restricted to regular graphs of c with fixed degree @d>=3. for the subclass c^', we establish a dichotomy: if the maximum degree is @d=3, the edge-colouring problem is np-complete, whereas, if @d=3, for r>=3.
simple algorithms for minimal triangulation of a graph and backward selection of a decomposable markov network. in this paper we propose a simple algorithm called cliquemintriang for computing a minimal triangulation of a graph. if f is the set of edges that is added to g to make it a complete graph k"n then the asymptotic complexity of cliquemintriang is o(|f|(@d^2+|f|)) where @d is the degree of the subgraph of k"n induced by f. therefore our algorithm performs well when g is a dense graph. we also show how to exploit the existing minimal triangulation techniques in conjunction with cliquemintriang to efficiently find a minimal triangulation of nondense graphs. finally we show how the algorithm can be adapted to perform a backward stepwise selection of decomposable markov networks; the resulting procedure has the same time complexity as that of existing similar algorithms.