Search

Strategy Logic (SL) is a logical formalism for strategic reasoning in multi-agent systems. Its main feature is that it has variables for strategies that are associated to specific agents using a binding operator. In this paper we introduce Graded Strategy Logic ( Graded SL), an extension of SL by graded quantifiers over tuples of strategy variables, i.e., “there exist at least g different tuples ( x 1 , . . . , x n ) of strategies” where g is a cardinal from the set N ∪ { ℵ 0 , ℵ 1 , 2 ℵ 0 } . We prove that the model-checking problem of Graded SL is decidable. We then turn to the complexity of fragments of Graded SL. When the g 's are restricted to finite cardinals, written Graded N SL, the complexity of model-checking is no harder than for SL, i.e., it is non-elementary in the quantifier-block rank. We illustrate our formalism by showing how to count the number of different strategy profiles that are Nash equilibria (NE). By analysing the structure of the specific formulas involved, we conclude that the important problem of checking for the existence of a unique NE can be solved in 2 ExpTime , which is not harder than merely checking for the existence of such an equilibrium. [ABSTRACT FROM AUTHOR]

Computation today is interactive agency in social networks. In this discussion paper, we look at this trend through the lens of logic, identifying two main lines. One is ‘epistemization’, making computational tasks refer explicitly to knowledge or beliefs of the agents performing them. The other line is using games as a model for computation, leading to ‘gamification’ of classical tasks, and computing by agents that may have preferences. This provides ingredients for a fundamental theory of computation that shifts from what is computed to how it is computed and by whom, moving from output to social behavior. The true impact of this shift is not in learning how to replace humans, but in creating new societies where humans and machines interact. While we do not offer a Turing-style account of this richer world, we discuss what becomes of three classical themes: the Universal Machine, Church's Thesis and the Turing Test. 1 [ABSTRACT FROM AUTHOR]

Given a directed graph, two vertices v and w are 2- vertex-connected if there are two internally vertex-disjoint paths from v to w and two internally vertex-disjoint paths from w to v . In this paper, we show how to compute this relation in O ( m + n ) time, where n is the number of vertices and m is the number of edges of the graph. As a side result, we show how to build in linear time an O ( n ) -space data structure, which can answer in constant time queries on whether any two vertices are 2-vertex-connected. Additionally, when two query vertices v and w are not 2-vertex-connected, our data structure can produce in constant time a “witness” of this property, by exhibiting a vertex or an edge that is contained in all paths from v to w or in all paths from w to v . [ABSTRACT FROM AUTHOR]

Non-locality and contextuality are among the most counterintuitive aspects of quantum theory. They are difficult to study using classical logic and probability theory. In this paper we start with an effect algebraic approach to the study of non-locality and contextuality. We will see how different slices over the category of set valued functors on the natural numbers induce different settings in which non-locality and contextuality can be studied. This includes the Bell, Hardy and Kochen–Specker-type paradoxes. We link this to earlier sheaf theoretic approaches by defining a fully faithful embedding of the category of effect algebras in this presheaf category over the natural numbers. [ABSTRACT FROM AUTHOR]

In this paper an implicit characterization of the complexity classes k - EXP and k - FEXP , for k ≥ 0 , is given, by a type assignment system for a stratified λ -calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic ( ELL ), and the hierarchy of complexity classes k - EXP is characterized by a hierarchy of types. [ABSTRACT FROM AUTHOR]

In this paper we show how the runtime complexity of imperative programs can be analysed fully automatically by a transformation to term rewrite systems , the complexity of which can then be automatically verified by existing complexity tools. We restrict to well-formed Jinja bytecode programs that only make use of non-recursive methods. The analysis can handle programs with cyclic data only if the termination behaviour is independent thereof. We exploit a term-based abstraction of programs within the abstract interpretation framework. The proposed transformation encompasses two stages. For the first stage we perform a combined control and data flow analysis by evaluating program states symbolically, which is shown to yield a finite representation of all execution paths of the given program through a graph, dubbed computation graph . In the second stage we encode the (finite) computation graph as a term rewrite system. This is done while carefully analysing complexity preservation and reflection of the employed transformations such that the complexity of the obtained term rewrite system reflects on the complexity of the initial program. Finally, we show how the approach can be automated and provide ample experimental evidence of the advantages of the proposed analysis. [ABSTRACT FROM AUTHOR]

We give polynomial time algorithms for quantitative (and qualitative) reachability analysis for Branching Markov Decision Processes (BMDPs). Specifically, given a BMDP, and given an initial population, where the objective of the controller is to maximize (or minimize) the probability of eventually reaching a population that contains an object of a desired (or undesired) type, we give algorithms for approximating the supremum (infimum) reachability probability, within desired precision ϵ > 0 , in time polynomial in the encoding size of the BMDP and in log ⁡ ( 1 / ϵ ) . We furthermore give P-time algorithms for computing ϵ -optimal strategies for both maximization and minimization of reachability probabilities. We also give P-time algorithms for all associated qualitative analysis problems, namely: deciding whether the optimal (supremum or infimum) reachability probabilities are 0 or 1. Prior to this paper, approximation of optimal reachability probabilities for BMDPs was not even known to be decidable. Our algorithms exploit the following basic fact: we show that for any BMDP, its maximum (minimum) non -reachability probabilities are given by the greatest fixed point (GFP) solution g ⁎ ∈ [ 0 , 1 ] n of a corresponding monotone max (min) Probabilistic Polynomial System of equations (max/minPPS), x = P ( x ) , which are the Bellman optimality equations for a BMDP with non-reachability objectives. We show how to compute the GFP of max/minPPSs to desired precision in P-time. We also study more general branching simple stochastic games (BSSGs) with (non-)reachability objectives. We show that: (1) the value of these games is captured by the GFP, g ⁎ , of a corresponding max-minPPS, x = P ( x ) ; (2) the quantitative problem of approximating the value is in TFNP; and (3) the qualitative problems associated with the value are all solvable in P-time. [ABSTRACT FROM AUTHOR]

Strategy Logic (SL) is a logical formalism for strategic reasoning in multi-agent systems. Its main feature is that it has variables for strategies that are associated to specific agents using a binding operator. In this paper we introduce Graded Strategy Logic ( Graded SL), an extension of SL by graded quantifiers over tuples of strategy variables, i.e., “there exist at least g different tuples ( x 1 , . . . , x n ) of strategies” where g is a cardinal from the set N ∪ { ℵ 0 , ℵ 1 , 2 ℵ 0 } . We prove that the model-checking problem of Graded SL is decidable. We then turn to the complexity of fragments of Graded SL. When the g 's are restricted to finite cardinals, written Graded N SL, the complexity of model-checking is no harder than for SL, i.e., it is non-elementary in the quantifier-block rank. We illustrate our formalism by showing how to count the number of different strategy profiles that are Nash equilibria (NE). By analysing the structure of the specific formulas involved, we conclude that the important problem of checking for the existence of a unique NE can be solved in 2 ExpTime , which is not harder than merely checking for the existence of such an equilibrium. [ABSTRACT FROM AUTHOR]

Abbott et al.'s notion of containers characterises a subset of parametric data types which can be described by a set of shapes and set of positions for each shape. This captures common data types such as tuples, lists, trees, arrays, and graphs. Various useful categorical structures can be derived for containers given additional information. For example, directed containers give rise to container comonads (Ahman et al.). Containers provide a useful reasoning principle and asbtraction mechanism for programming. This paper studies the performance characteristics of traversal schemes over containers, modelled by functor and comonad structures. A cost model for container transformations is defined from which complexity bounds for the operations of container functors and comonads are derived. These bounds suggest optimisations for programs structured using these idioms. The abstract interface provided by the syntax of containers and category theory provides complexity bounds and subsequent optimisations that are implementation agnostic (machine free). [ABSTRACT FROM AUTHOR]

Abstract: We continue our study of the complexity of MSO-definable local temporal logics over concurrent systems that can be described by Mazurkiewicz traces. In previous papers, we showed that the satisfiability problem for any such logic is in PSPACE (provided the dependence alphabet is fixed, Gastin and Kuske (2003) ) and remains in PSPACE for all classical local temporal logics even if the dependence alphabet is part of the input, Gastin and Kuske (2007) . In this paper, we consider the uniform satisfiability problem for arbitrary MSO-definable local temporal logics. For this problem, we prove multi-exponential lower and upper bounds that depend on the number of alternations of set quantifiers present in the chosen MSO-modalities. [Copyright &y& Elsevier]

Abstract: This paper proposes a semiring formulation for reasoning about an agent’s changing beliefs: a dynamic epistemic semiring (DES). A DES is a modal semiring extended with epistemic-action operators. The paper concentrates on the revision operator by proposing an axiomatisation, developing a basic calculus and deriving the classical AGM revision axioms in the algebra. Iterated action is also considered. [Copyright &y& Elsevier]

Abstract: In this paper, we focus on the edit distance between two given strings where block-edit operations are allowed and better fitting to the human natural edit behaviors. Previous results showed that this problem is NP-hard when block moves are allowed. Various approximations to this problem have been proposed in recent years. However, this problem can be solved by the polynomial-time optimization algorithms if some reasonable restrictions are applied. The restricted variations which we consider involve character insertions, character deletions, block copies and block deletions. In this paper, three problems are defined with different measuring functions, which are , and . Then we show that with some preprocessing, the minimum block edit distances of these three problems can be obtained by dynamic programming in , and time, respectively, where n and m are the lengths of the two input strings. [Copyright &y& Elsevier]

Abstract: It has become a standard approach to reason about contextual equivalence using some notion of (bi)simulation. The main technical task of this approach is to show that (bi)simulation is a (pre)congruence, and hence is sound for reasoning about contextual equivalence. Howe devised a method to prove this, and his method has been widely adapted and applied. This paper deals with this challenge for call-by-need computation including non-determinism. In this setting, sharing of sub-computations must be taken into account due to its observable effects on the outcome of computations. The technical results of this paper are the definition of a class of non-deterministic reduction-based functional languages (SHOCS). The definition of this class is in terms of a schematic characterization of the reduction rules of the language. The main result is that for SHOCS languages mutual similarity is sound for reasoning about contextual equivalence based on may-convergence. The paper also contains a presentation of a particular non-deterministic call-by-need calculus with let, case, constructors, and seq. [Copyright &y& Elsevier]

Abstract: This paper has the purpose of reviewing some of the established relationships between logic and concurrency, and of exploring new ones. Concurrent and distributed systems are notoriously hard to get right. Therefore, following an approach that has proved highly beneficial for sequential programs, much effort has been invested in tracing the foundations of concurrency in logic. The starting points of such investigations have been various idealized languages of concurrent and distributed programming, in particular the well established state-transformation model inspired by Petri nets and multiset rewriting, and the prolific process-based models such as the -calculus and other process algebras. In nearly all cases, the target of these investigations has been linear logic, a formal language that supports a view of formulas as consumable resources. In the first part of this paper, we review some of these interpretations of concurrent languages into linear logic and observe that, possibly modulo duality, they invariably target a small semantic fragment of linear logic that we call LVobs. In the second part of the paper, we propose a new approach to understanding concurrent and distributed programming as a manifestation of logic, which yields a language that merges those two main paradigms of concurrency. Specifically, we present a new semantics for multiset rewriting founded on an alternative view of linear logic and specifically LVobs. The resulting interpretation is extended with a majority of linear connectives into the language of -multisets. This interpretation drops the distinction between multiset elements and rewrite rules, and considerably enriches the expressive power of standard multiset rewriting with embedded rules, choice, replication, and more. Derivations are now primarily viewed as open objects, and are closed only to examine intermediate rewriting states. The resulting language can also be interpreted as a process algebra. For example, a simple translation maps process constructors of the asynchronous -calculus to rewrite operators. The language of -multisets forms the basis for the security protocol specification language MSR 3. With relations to both multiset rewriting and process algebra, it supports specifications that are process-based, state-based, or of a mixed nature, with the potential of combining verification techniques from both worlds. Additionally, its logical underpinning makes it an ideal common ground for systematically comparing protocol specification languages. [Copyright &y& Elsevier]

Abstract: Boolean grammars [A. Okhotin, Boolean grammars, Information and Computation 194 (1) (2004) 19–48] are a promising extension of context-free grammars that supports conjunction and negation in rule bodies. In this paper, we give a novel semantics for Boolean grammars which applies to all such grammars, independently of their syntax. The key idea of our proposal comes from the area of negation in logic programming, and in particular from the so-called well-founded semantics which is widely accepted in this area to be the “correct” approach to negation. We show that for every Boolean grammar there exists a distinguished (three-valued) interpretation of the non-terminal symbols, which satisfies all the rules of the grammar and at the same time is the least fixed-point of an operator associated with the grammar. Then, we demonstrate that every Boolean grammar can be transformed into an equivalent (under the new semantics) grammar in normal form. Based on this normal form, we propose an algorithm for parsing that applies to any such normalized Boolean grammar. In summary, the main contribution of this paper is to provide a semantics which applies to all Boolean grammars while at the same time retaining the complexity of parsing associated with this type of grammars. [Copyright &y& Elsevier]

Abstract: Wavelet Trees have been introduced by Grossi et al. in SODA 2003 and have been rapidly recognized as a very flexible tool for the design of compressed full-text indexes and data compression algorithms. Although several papers have investigated the properties and usefulness of this data structure in the full-text indexing scenario, its impact on data compression has not been fully explored. In this paper we provide a throughout theoretical analysis of a wide class of compression algorithms based on Wavelet Trees. Also, we propose a novel framework, called Pruned Wavelet Trees, that aims for the best combination of Wavelet Trees of properly-designed shapes and compressors either binary (like, Run-Length encoders) or non-binary (like, Huffman and Arithmetic encoders). [Copyright &y& Elsevier]

Abstract: This paper is about the verification of dynamic properties by model-checking for finite state reactive systems. Properties are expressed as PLTL formulae. Systems are specified through a top-down refinement process. In order to cope with the state explosion problem, we propose partitioning the state space to be verified and to verify the properties independently on each part. Properties that are such that if they hold on every part then they hold for the whole system are called verifiable by parts. In a previous paper, we presented a class of interesting PLTL properties that are always verifiable by parts. That is, they are verifiable by parts with any partitioning of the state space. In addition to these properties, some properties are verifiable by parts on a system provided with a particular partitioning. In this paper, we propose a partitioning of the state space of a system that is guided by the refinement process. We introduce an extended class of PLTL properties that are verifiable by parts with regard to this partitioning. This class includes the first one. In particular, the new class includes liveness properties under fairness assumptions. This class is defined from Büchi automata that accept the language of the negations of the properties. Our work is illustrated by its application to a chip card protocol called . This protocol is specified through successive refinements. [Copyright &y& Elsevier]

Abstract: Deterministic behavior for parallel and distributed computation is rather difficult to ensure. To reach that goal, many formal calculi, languages, and techniques with well-defined semantics have been proposed in the past. But none of them focused on an imperative object calculus with asynchronous communications and futures. In this article, an object calculus, Asynchronous Sequential Processes (ASP), is defined, with its semantics. We prove also confluence properties for the ASP calculus. ASPs main characteristics are asynchronous communications with futures, and sequential execution within each process. This paper provides a very general and dynamic property ensuring confluence. Further, more specific and static properties are derived. Additionally, we present a formalization of distributed components based on ASP, and show how such components are used to statically ensure determinacy. This paper can also be seen as a formalization of the concept of futures in a distributed object setting. [Copyright &y& Elsevier]

Abstract: This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles. [Copyright &y& Elsevier]

Abstract: Structured Operational Semantics (SOS) is a popular method for defining semantics by means of transition rules. An important feature of SOS rules is negative premises, which are crucial in the definitions of such phenomena as priority mechanisms and time-outs. However, the inclusion of negative premises in SOS rules also introduces doubts as to the preferred meaning of SOS specifications. Orderings on SOS rules were proposed by Phillips and Ulidowski as an alternative to negative premises. Apart from the definition of the semantics of positive GSOS rules with orderings, the meaning of more general types of SOS rules with orderings has not been studied hitherto. This paper presents several candidates for the meaning of general SOS rules with orderings and discusses their conformance to our intuition for such rules. We take two general frameworks (rule formats) for SOS with negative premises and SOS with orderings, and present semantics-preserving translations between them with respect to our preferred notion of semantics. Thanks to our semantics-preserving translation, we take existing congruence meta-results for strong bisimilarity from the setting of SOS with negative premises into the setting of SOS with orderings. We further compare the expressiveness of rule formats for SOS with orderings and SOS with negative premises. The paper contains also many examples that illustrate the benefits of SOS with orderings and the properties of the presented definitions of meaning. [Copyright &y& Elsevier]

Abstract: The paper presents a case study on the synthesis of labelled transition systems (ltss) for process calculi, choosing as testbed Milner’s Calculus of Communicating System (ccs). The proposal is based on a graphical encoding: each ccs process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence. Graphs with interfaces are amenable to the synthesis mechanism proposed by Ehrig and König and based on borrowed contexts (bcs), an instance of relative pushouts originally introduced by Milner and Leifer. The bc mechanism allows the effective construction of an lts that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. Our paper focuses on the analysis of the lts distilled by exploiting the encoding of ccs processes: besides offering major technical contributions towards the simplification of the bc mechanism, a key result of our work is the proof that the bisimilarity on processes obtained via bcs coincides with the standard strong bisimilarity for ccs. [Copyright &y& Elsevier]

Abstract: Computability logic (CL) is a semantical platform and research program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth which it has more traditionally been. Formulas in CL stand for (interactive) computational problems, understood as games between a machine and its environment; logical operators represent operations on such entities; and “truth” is understood as existence of an effective solution, i.e., of an algorithmic winning strategy. The formalism of CL is open-ended, and may undergo series of extensions as the study of the subject advances. The main groups of operators on which CL has been focused so far are the parallel, choice, branching, and blind operators, with the logical behaviors of the first three groups resembling those of the multiplicatives, additives and exponentials of linear logic, respectively. The present paper introduces a new important group of operators, called sequential. The latter come in the form of sequential conjunction and disjunction, sequential quantifiers, and sequential recurrences (“exponentials”). As the name may suggest, the algorithmic intuitions associated with this group are those of sequential computations, as opposed to the intuitions of parallel computations associated with the parallel group of operations. Specifically, while playing a parallel combination of games means playing all components of the combination simultaneously, playing a sequential combination means playing the components in a sequential fashion, one after one. The main technical result of the present paper is a sound and complete axiomatization of the propositional fragment of computability logic whose vocabulary, together with negation, includes all three — parallel, choice and sequential — sorts of conjunction and disjunction. An extension of this result to the first-order level is also outlined. [Copyright &y& Elsevier]

Abstract: In this paper, we consider the problem of covering a set of strings S with a set C of substrings in S, where C is said to cover S if every string in S can be written as a concatenation of the substrings in C. We discuss applications for the problem that arise in the context of computational biology and formal language theory. We then proceed to show several hardness of approximation results for the problem, and in the main part of the paper, we focus on devising approximation algorithms using two generic paradigms—the local-ratio technique and linear programming rounding. [Copyright &y& Elsevier]

Abstract: We define reactive simulatability for general asynchronous systems. Roughly, simulatability means that a real system implements an ideal system (specification) in a way that preserves security in a general cryptographic sense. Reactive means that the system can interact with its users multiple times, e.g., in many concurrent protocol runs or a multi-round game. In terms of distributed systems, reactive simulatability is a type of refinement that preserves particularly strong properties, in particular confidentiality. A core feature of reactive simulatability is composability, i.e., the real system can be plugged in instead of the ideal system within arbitrary larger systems; this is shown in follow-up papers, and so is the preservation of many classes of individual security properties from the ideal to the real systems. A large part of this paper defines a suitable system model. It is based on probabilistic IO automata (PIOA) with two main new features: One is generic distributed scheduling. Important special cases are realistic adversarial scheduling, procedure-call-type scheduling among colocated system parts, and special schedulers such as for fairness, also in combinations. The other is the definition of the reactive runtime via a realization by Turing machines such that notions like polynomial-time are composable. The simple complexity of the transition functions of the automata is not composable. As specializations of this model we define security-specific concepts, in particular a separation between honest users and adversaries and several trust models. The benefit of IO automata as the main model, instead of only interactive Turing machines as usual in cryptographic multi-party computation, is that many cryptographic systems can be specified with an ideal system consisting of only one simple, deterministic IO automaton without any cryptographic objects, as many follow-up papers show. This enables the use of classic formal methods and automatic proof tools for proving larger distributed protocols and systems that use these cryptographic systems. [Copyright &y& Elsevier]

Abstract: A Distance labeling scheme is a type of localized network representation in which short labels are assigned to the vertices, allowing one to infer the distance between any two vertices directly from their labels, without using any additional information sources. As most applications for network representations in general, and distance labeling schemes in particular, concern large and dynamically changing networks, it is of interest to focus on distributed dynamic labeling schemes. The paper considers dynamic weighted trees where the vertices of the trees are fixed but the (positive integral) weights of the edges may change. The two models considered are the edge-dynamic model, where from time to time some edge changes its weight by a fixed quanta, and the increasing-dynamic model in which edge weights can only grow. The paper presents distributed approximate distance labeling schemes for the two dynamic models, which are efficient in terms of the required label size and communication complexity involved in updating the labels following the weight changes. [Copyright &y& Elsevier]

Abstract: Though complexity theory already extensively studies path-cardinality-based restrictions on the power of nondeterminism, this paper is motivated by a more recent goal: To gain insight into how much of a restriction, it is of nondeterminism to limit machines to have just one contiguous (with respect to some simple order) interval of accepting paths. In particular, we study the robustness—the invariance under definition changes—of the cluster class CL#P. This class contains each #P function that is computed by a balanced Turing machine whose accepting paths always form a cluster with respect to some length-respecting total order with efficient adjacency checks. The definition of CL#P is heavily influenced by the defining paper’s focus on (global) orders. In contrast, we define a cluster class, CLU#P, to capture what seems to us a more natural model of cluster computing. We prove that the naturalness is costless: CL#P=CLU#P. Then we exploit the more natural, flexible features of CLU#P to prove new robustness results for CL#P and to expand what is known about the closure properties of CL#P. The complexity of recognizing edges—of an ordered collection of computation paths or of a cluster of accepting computation paths—is central to this study. Most particularly, our proofs exploit the power of unique discovery of edges—the ability of nondeterministic functions to, in certain settings, discover on exactly one (in some cases, on at most one) computation path a critical piece of information regarding edges of orderings or clusters. [Copyright &y& Elsevier]

Abstract: This paper studies the complexity of learning classes of expressions in propositional logic from equivalence queries and membership queries. In particular, we focus on bounding the number of queries that are required to learn the class ignoring computational complexity. This quantity is known to be captured by a combinatorial measure of concept classes known as the certificate complexity. The paper gives new constructions of polynomial size certificates for monotone expressions in conjunctive normal form (CNF), for unate CNF functions where each variable affects the function either positively or negatively but not both ways, and for Horn CNF functions. Lower bounds on certificate size for these classes are derived showing that for some parameter settings the new certificate constructions are optimal. Finally, the paper gives an exponential lower bound on the certificate size for a natural generalization of these classes known as renamable Horn CNF functions, thus implying that the class is not learnable from a polynomial number of queries. [Copyright &y& Elsevier]

Abstract: Bigraphs are graphs whose nodes may be nested, representing locality, independently of the edges connecting them. They may be equipped with reaction rules, forming a bigraphical reactive system (Brs) in which bigraphs can reconfigure themselves. Following an earlier paper describing link graphs, a constituent of bigraphs, this paper is a devoted to pure bigraphs, which in turn underlie various more refined forms. Elsewhere it is shown that behavioural analysis for Petri nets, π-calculus and mobile ambients can all be recovered in the uniform framework of bigraphs. The paper first develops the dynamic theory of an abstract structure, a wide reactive system (Wrs), of which a Brs is an instance. In this context, labelled transitions are defined in such a way that the induced bisimilarity is a congruence. This work is then specialised to Brss, whose graphical structure allows many refinements of the theory. The latter part of the paper emphasizes bigraphical theory that is relevant to the treatment of dynamics via labelled transitions. As a running example, the theory is applied to finite pure CCS, whose resulting transition system and bisimilarity are analysed in detail. The paper also mentions briefly the use of bigraphs to model pervasive computing and biological systems. [Copyright &y& Elsevier]

Abstract: This paper considers the problem of performing tasks in asynchronous distributed settings. This problem, called Do-All, has been substantially studied in synchronous models, but there is a dearth of efficient algorithms for asynchronous message-passing processors. Do-All can be trivially solved without any communication by an algorithm where each processor performs all tasks. Assuming p processors and t tasks, this requires work Θ(p · t). Thus, it is important to develop subquadratic solutions (when p and t are comparable) by trading computation for communication. Following the observation that it is not possible to obtain subquadratic work when the message delay d is substantial, e.g., d =Θ(t), this work pursues a message-delay-sensitive approach. Here, the upper bounds on work and communication are given as functions of p, t, and d, the upper bound on message delays, however, algorithms have no knowledge of d and they cannot rely on the existence of an upper bound on d. This paper presents two families of asynchronous algorithms achieving, for the first time, subquadratic work as long as d = o (t). The first family uses as its basis a shared-memory algorithm without having to emulate atomic registers assumed by that algorithm. These deterministic algorithms have work O(tp ε + pd⌈t/d⌉ ε ) for any ε >0. The second family uses specific permutations of tasks, with certain combinatorial properties, to sequence the work of the processors. These randomized (deterministic) algorithms have expected (worst-case) work O(t log p + pd log(2+ t/d)). Another important contribution in this work is the first delay-sensitive lower bound for this problem that helps explain the behavior of our algorithms: any randomized (deterministic) algorithm has expected (worst-case) work of Ω(t + pd log d+1 t). [Copyright &y& Elsevier]

Abstract: This paper introduces (pronounce spades), a stochastic process algebra for discrete event systems, that extends traditional process algebra with timed actions whose delay is governed by general (a.o. continuous) probability distributions. The operational semantics is defined in terms of stochastic automata, a model that uses clocks—like in timed automata—to symbolically represent randomly timed systems, cf. the accompanying paper [P.R. D’Argenio, J.-P. Kateon, A theory of stochastic systems. Part I: Stochastic automata. Inf. Comput. (2005), to appear]. We show that stochastic automata and are equally expressive, and prove that the operational semantics of a term up to α-conversion of clocks, is unique (modulo symbolic bisimulation). (Open) probabilistic and structural bisimulation are proven to be congruences for, and are equipped with an equational theory. The equational theory is shown to be complete for structural bisimulation and allows to derive an expansion law. [Copyright &y& Elsevier]

Abstract: This paper presents the theoretical underpinning of a model for symbolically representing probabilistic transition systems, an extension of labelled transition systems for the modelling of general (discrete as well as continuous or singular) probability spaces. These transition systems are particularly suited for modelling softly timed systems, real-time systems in which the time constraints are of random nature. For continuous probability spaces these transition systems are infinite by nature. Stochastic automata represent their behaviour in a finite way. This paper presents the model of stochastic automata, their semantics in terms of probabilistic transition systems, and studies several notions of bisimulation. Furthermore, the relationship of stochastic automata to generalised semi-Markov processes is established. [Copyright &y& Elsevier]

Abstract: This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship. [Copyright &y& Elsevier]

Abstract: This paper describes a superposition calculus where quantifiers are eliminated lazily. Superposition and simplification inferences may employ equivalences that have arbitrary formulas at their smaller side. A closely related calculus is implemented in the Saturate system and has shown useful on many examples, in particular in set theory. The paper presents a completeness proof and reports on practical experience obtained with the Saturate system. [Copyright &y& Elsevier]

Abstract: We study integrated prefetching and caching in single and parallel disk systems. In the first part of the paper we investigate approximation algorithms for the single disk problem. There exist two very popular approximation algorithms called Aggressive and Conservative for minimizing the total elapsed time. We give a refined analysis of the Aggressive algorithm, improving the original analysis by Cao et al. We prove that our new bound is tight. Additionally we present a new family of prefetching and caching strategies and give algorithms that perform better than Aggressive and Conservative. In the second part of the paper we investigate the problem of minimizing stall time in parallel disk systems. We present a polynomial time algorithm for computing a prefetching/caching schedule whose stall time is bounded by that of an optimal solution. The schedule uses at most extra memory locations in cache. This is the first polynomial time algorithm that, using a small amount of extra resources, computes schedules whose stall times are bounded by that of optimal schedules not using extra resources. Our algorithm is based on the linear programming approach of [Journal of the ACM, 47 (2000) 969]. However, in order to achieve minimum stall times, we introduce the new concept of synchronized schedules in which fetches on the disks are performed completely in parallel. [Copyright &y& Elsevier]

Abstract: Gossiping is an extensively investigated information dissemination process in which each processor has a distinct item of information and has to collect all the items possessed by the other processors. In this paper we provide an innovative and general lower bound technique relying on the novel notion of delay digraph of a gossiping protocol and on the use of matrix norm methods. Such a technique is very powerful and allows the determination of new and significantly improved lower bounds in many cases. In fact, we derive the first general lower bound on the gossiping time of systolic protocols, i.e., constituted by a periodic repetition of simple communication steps. In particular, given any network of n processors and any systolic period s, in the directed and the undirected half-duplex cases every s-systolic gossip protocol takes at least log(n)/log(1/λ)−O(loglog(n)) time steps, where λ is the unique solution between 0 and 1 of , with p i (λ)=1+ λ 2 +⋯+ λ 2i −2 for any integer i >0. We then provide improved lower bounds in the directed and half-duplex cases for many well-known network topologies, such as Butterfly, de Bruijn, and Kautz graphs. All the results are extended also to the full-duplex case. Our technique is very general, as for s →∞ it allows the determination of improved results even for non-systolic protocols. In fact, for general networks, as a simple corollary it yields a lower bound only an O(loglog(n)) additive factor far from the general one independently proved in [Proc. 1st ACM Symposium on Parallel Algorithms and Architectures (SPAA), 1989, p. 318; Topics in Combinatorics and Graph Theory (1990) 451; SIAM Journal on Computing 21(1) (1992) 111; Discrete Applied Mathematics 42 (1993) 75] for all graphs and any (non-systolic) gossip protocol. Moreover, for specific networks, it significantly improves with respect to the previously known results, even in the full-duplex case. Correspondingly, better lower bounds on the gossiping time of non-systolic protocols are determined in the directed, half-duplex and full-duplex cases for Butterfly, de Bruijn, and Kautz graphs. Even if in this paper we give only a limited number of examples, our technique has wide applicability and gives a general framework that often allows to get improved lower bounds on the gossiping time of systolic and non-systolic protocols in the directed, half-duplex and full-duplex cases. [Copyright &y& Elsevier]

This paper presents a deterministic and efficient algorithm for online facility location. The algorithm is based on a simple hierarchical partitioning and is extremely simple to implement. It also applies to a variety of models, i.e., models where the facilities can be placed anywhere in the region, or only at customer sites, or only at fixed locations. The paper shows that the algorithm is O(logn)-competitive under these various models, where n is the total number of customers. It also shows that the algorithm is O(1)-competitive with high probability and for any arrival order when customers are uniformly distributed or when they follow a distribution satisfying a smoothness property. Experimental results for a variety of scenarios indicate that the algorithm behaves extremely well in practice. [Copyright &y& Elsevier]

Information integration systems provide uniform interfaces to varieties of heterogeneous information sources. For query answering in such systems, the current generation of query answering algorithms in local-as-view (source-centric) information integration systems all produce what has been thought of as “the best obtainable” answer, given the circumstances that the source-centric approach introduces incomplete information into the virtual global relations. However, this “best obtainable” answer does not include all information that can be extracted from the sources because it does not allow partial information. Neither does the “best obtainable” answer allow for composition of queries, meaning that querying a result of a previous query will not be equivalentto the composition of the two queries. In this paper, we provide a foundation for information integration, based on the algebraic theory of incomplete information. Our framework allows us to define the semantics of partial facts and introduce the notion of the exact answer—that is the answer that includes partial facts. We show that querying under the exact answer semantics is compositional. We also present two methods for actually computing the exact answer. The first method is tableau-based, and it is a generalization of the “inverse-rules” approach. The second, much more efficient method, is a generalization of the rewriting approach, and it is based on partial containment mappings introduced in the paper. [Copyright &y& Elsevier]

In this paper we study fixpoints of operators on lattices and bilattices in a systematic and principled way. The key concept is that of an approximating operator, a monotone operator on the product bilattice, which gives approximate information on the original operator in an intuitive and well-defined way. With any given approximating operator our theory associates several different types of fixpoints, including the Kripke–Kleene fixpoint, stable fixpoints, and the well-founded fixpoint, and relates them to fixpoints of operators being approximated. Compared to our earlier work on approximation theory, the contribution of this paper is that we provide an alternative, more intuitive, and better motivated construction of the well-founded and stable fixpoints. In addition, we study the space of approximating operators by means of a precision ordering and show that each lattice operator O has a unique most precise—we call it ultimate—approximation. We demonstrate that fixpoints of this ultimate approximation provide useful insights into fixpoints of the operator O. We then discuss applications of these results in logic programming. [Copyright &y& Elsevier]

This paper studies nested simulation and nested trace semantics over the language BCCSP, a basic formalism to express finite process behaviour. It is shown that none of these semantics affords finite (in)equational axiomatizations over BCCSP. In particular, for each of the nested semantics studied in this paper, the collection of sound, closed (in)equations over a singleton action set is not finitely based. [Copyright &y& Elsevier]

This paper introduces a novel (bi)simulation-based faster-than preorder which relates asynchronous processes, where the relative speeds of system components are indeterminate, with respect to their worst-case timing behavior. The study is conducted for a conservative extension of the process algebra CCS, called TACS, which permits the specification of upper time bounds on action occurrences. TACS complements work in plain process algebras which compares asynchronous processes with respect to their functional reactive behavior only, and in timed process algebras which focus on analyzing synchronous processes. The most unusual contribution is in showing that the proposed faster-than preorder coincides with several other preorders, two of which consider the absolute times at which actions occur in system runs. The paper also develops the semantic theory of TACS by studying congruence properties, equational laws, and abstractions from internal actions. Two examples, one dealing with mail delivery and one relating two implementations of a simple storage system, testify to the practical utility of the new theory. [Copyright &y& Elsevier]

In this paper we study the question of whether identifiable classes have subclasses which are identifiable under a more restrictive criterion. The chosen framework is inductive inference, in particular the criterion of explanatory learning (Ex) of recursive functions as introduced by Gold [Inform. Comput. 10 (1967) 447]. Among the more restrictive criteria is finite learning where the learner outputs, on every function to be learned, exactly one hypothesis (which has to be correct). The topic of the present paper are the natural variants (a) and (b) below of the classical question whether a given learning criterion like finite learning is more restrictive than Ex-learning. (a) Does every infinite Ex-identifiable class have an infinite finitely identifiable subclass? (b) If an infinite Ex-identifiable class S has an infinite finitely identifiable subclass, does it necessarily follow that some appropriate learner Ex-identifies S as well as finitely identifies an infinite subclass of S? These questions are also treated in the context of ordinal mind change bounds. [Copyright &y& Elsevier]

This paper deals with the file allocation problem concerning the dynamic optimization of communication costs to access data in a distributed environment. We develop a dynamic file re-allocation strategy that adapts on-line to a sequence of read and write requests whose location and relative frequencies are completely unpredictable. This is achieved by replicating the file in response to read requests and migrating the file in response to write requests while paying the associated communications costs, so as to be closer to processors that access it frequently. We develop first explicit deterministic on-line strategy assuming existence of global information about the state of the network; previous (deterministic) solutions were complicated and more expensive. Our solution has (optimal) logarithmic competitive ratio. The paper also contains the first explicit deterministic data migration algorithm achieving the best known competitive ratio for this problem. Using somewhat different technique, we also develop the first deterministic distributed file allocation algorithm (using only local information) with poly-logarithmic competitive ratio against a globally optimized optimal prescient strategy. [Copyright &y& Elsevier]

This paper presents a collection of string algorithms that are at the core of several biological problems such as discovering potential drug targets, creating diagnostic probes, universal primers or unbiased consensus sequences. All these problems reduce to the task of finding a pattern that, with some error, occurs in one set of strings (Closest Substring Problem) and does not occur in another set (Farthest String Problem). In this paper, we break down the problem into several subproblems and prove the following results.

Bounded operator abstraction is a language construct relevant to object oriented programming languages and to ML2000, the successor to Standard ML. In this paper, we introduce Fω&les;, a variant of F<:ω with this feature and with Cardelli and Wegner’s kernel Fun rule for quantifiers. We define a typed-operational semantics with subtyping and prove that it is equivalent with Fω&les;, using logical relations to prove soundness. The typed-operational semantics provides a powerful and uniform technique to study metatheoretic properties of Fω&les;, such as Church–Rosser, subject reduction, the admissibility of structural rules, and the equivalence with the algorithmic presentation of the system that performs weak-head reductions.Furthermore, we can show decidability of subtyping using the typed-operational semantics and its equivalence with the usual presentation. Hence, this paper demonstrates for the first time that logical relations can be used to show decidability of subtyping. [Copyright &y& Elsevier]

Grover's algorithm provides a quadratic speedup over classical algorithms to search for marked elements in an unstructured database. The original algorithm is probabilistic, and there are several schemes to achieve the deterministic version, by using the generalized Grover's iteration G (α , β) : = S r (β) S o (α). However, in all the existing schemes the value range of α and β is limited; for instance, in the three early schemes they are determined by the proportion of marked states M / N. In this paper, we break through this limitation by presenting a search framework with adjustable parameters, which allows α or β to be arbitrarily given. The significance of the framework lies not only in the expansion of mathematical form, but also in its application value, as we present two disparate problems which we are able to solve deterministically using the proposed framework, whereas previous schemes are ineffective. [ABSTRACT FROM AUTHOR]

Among different spatial data models, the topological model for spatial regions explicitly represents common boundaries. This model pursues the efficiency of topology-related queries and the elimination of data redundancy. This paper proposes several space-efficient data structures to support access to the topological representation of two-dimensional regions that are organized in a multi-granular or hierarchical structure, such as the political and administrative partition of a country. In the context of these hierarchies, we focus on queries that search for inclusion, disjointness, and adjacency between regions. The proposed structures build upon compact planar graph embeddings, which show to have a good trade-off between space and time. [ABSTRACT FROM AUTHOR]

The paper demonstrates the non-closure of the family of unambiguous linear languages (that is, those defined by unambiguous linear context-free grammars) under complementation. To be precise, a particular unambiguous linear grammar is presented, and it is proved that the complement of this language is not defined by any context-free grammar. This also constitutes an alternative proof for the result of Hibbard and Ullian ("The independence of inherent ambiguity from complementedness among context-free languages", JACM , 1966) on the non-closure of the unambiguous languages under complementation. [ABSTRACT FROM AUTHOR]

In previously published work (Jordon and Moser, 2020), notions of finite-state-depth and pushdown-depth were presented. These were based on finite-state transducers and information lossless pushdown compressors. Unfortunately, a complete separation between the two notions was not established. This paper introduces a new formulation of pushdown-depth based on restricting how fast a pushdown compressor's stack can grow. This allows us to do a full comparison by demonstrating the existence of sequences with high finite-state-depth and low pushdown-depth, and vice-versa. A new notion based on the Lempel-Ziv 78 algorithm is also presented. Its difference from finite-state-depth is shown by a Lempel-Ziv deep sequence that is not finite-state deep, and vice versa. Lempel-Ziv-depth's difference from pushdown-depth is shown by building sequences that have a pushdown-depth of roughly 1/2 but low Lempel-Ziv depth, and by a sequence with high Lempel-Ziv depth but low pushdown-depth. Properties of all three notions are also studied. [ABSTRACT FROM AUTHOR]

In this paper we introduce a new class of labelled transition systems—labelled Markov processes— and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete. We assume that the state space is a certain type of common metric space called an analytic space. We show that our definition of probabilistic bisimulation generalizes the Larsen–Skou definition given for discrete systems. The formalism and mathematics is substantially different from the usual treatment of probabilistic process algebra. The main technical contribution of the paper is a logical characterization of probabilistic bisimulation. This study revealed some unexpected results, even for discrete probabilistic systems.

Branching programs are considered as a nonuniform model of computation in complexity theory as well as a data structure for boolean functions in several applications. In many applications (e.g., verification), exact representations are required. For learning boolean functions f on the basis of classified examples, it is sufficient to produce the representation of a function g approximating f. This motivates the investigation of the size of the smallest branching program approximating f. Although several nonapproximability results are contained in the papers on randomized branching programs, these results often do not work for the uniform distribution (which is the most important one in applications). Here, the following nonapproximability results are presented.(1) It is proven that two simple and well-known functions from the branching program literature require exponential size to be approximated with respect to the uniform distribution by OBDDs, which are the most important type of branching programs in applications.(2) The first truly exponential lower bound on the size of approximating syntactic read-k-times branching programs with respect to the uniform distribution and error probability 1/2−2−Ω(n), n the input size, is shown. In order to improve upon the best previous results for error probabilities smaller than 1/3, a strong combinatorial lemma from a paper of Ajtai on linear-length branching programs is exploited. [Copyright &y& Elsevier]