Catálogo de publicaciones - libros

We introduce a uniform framework for reasoning about infinite-state systems with unbounded control structures and unbounded data domains. Our framework is based on constrained rewriting systems on words over an infinite alphabet. We consider several rewriting semantics: factor, prefix, and multiset rewriting. Constraints are expressed in a logic on such words which is parametrized by a first-order theory on the considered data domain. We show that our framework is suitable for reasoning about various classes of systems such as recursive sequential programs, multithreaded programs, parametrized and dynamic networks of processes, etc. Then, we provide generic results (1) for the decidability of the satisfiability problem of the fragment ∃  ∀  of this logic provided that the underlying logic on data is decidable, and (2) for proving inductive invariance and for carrying out Hoare style reasoning within this fragment. We also show that the reachability problem is decidable for a class of prefix rewriting systems with integer data.

We look at the recently introduced neural-like systems, called SN P systems. These systems incorporate the ideas of spiking neurons into membrane computing. We study various classes and characterize their computing power and complexity. In particular, we analyze asynchronous and sequential SN P systems and present some conditions under which they become (non-)universal. The non-universal variants are characterized by monotonic counter machines and partially blind counter machines and, hence, have many decidable properties. We also investigate the language-generating capability of SN P systems.

In many areas of science huge networks (graphs) are central objects of study: the internet, the brain, various social networks, VLSI, statistical physics. To study these graphs, new paradigms are needed: What are meaningful questions to ask? When are two huge graphs “similar”? How to “scale down” these graphs without changing their fundamental structure and algorithmic properties? How to generate random examples with the desired properties? A reasonably complete answer can be given in the case when the huge graphs are dense (in the more difficult case of sparse graphs there are only partial results).

The notion of feedback and information flow is a fundamental concept arising in many classical areas of computing. In the late 1980s and early 1990s, an algebraic structure dealing with cyclic operations emerged from various fields, including flowchart schemes, dataflow with feedback, iteration theories, action calculi in concurrency theory, proof theory (Linear Logic and Geometry of Interaction), and network algebra, as well as in pure mathematics. This structure, now known as a “traced monoidal category”, was formally introduced in an influential paper of Joyal, Street and Verity (1996) from current work in topology and knot theory. However these authors were also keenly aware of its potential applicability. Since then, such structures – with variations – have been pursued in several areas of mathematics, logic and theoretical computer science, including game semantics, quantum programming languages and quantum protocols, and computational biology. We shall survey applications in logic and theoretical computer science and discuss progress towards an abstract geometry of algorithms.

We introduce a definition for a for  ≥ 1. Our purpose is to generalize the well-known definition of a longest common subsequence of linear strings for dimensions higher than one. We prove that computing a largest common two-dimensional subsequence of two given two-dimensional strings is -complete. We present an algorithm for the case of the problem when the definition is weakened.

We present new combinatorial approximation algorithms for -set cover. Previous approaches are based on extending the greedy algorithm by efficiently handling small sets. The new algorithms further extend them by utilizing the natural idea of computing large packings of elements into sets of large size. Our results improve the previously best approximation bounds for the -set cover problem for all values of  ≥ 6. The analysis technique could be of independent interest; the upper bound on the approximation factor is obtained by bounding the objective value of a linear program.

We propose and study a new information transmission problem motivated by today’s internet. Suppose a real number needs to be transmitted in a network. This real number may represent data or control and pricing information of the network. We propose a new transmission model in which the real number is encoded using Bernoulli trials. This differs from the traditional framework of Shannon’s information theory. We propose a natural criterion for the quality of an encoding scheme. Choosing the best encoding reduces to a problem in the calculus of variations, which we solve rigorously. In particular, we show there is a unique optimal encoding, and give an explicit formula for it.

We also solve the problem in a more general setting in which there is prior information about the real number, or a desire to weight errors for different values non-uniformly.

Our tools come mainly from real analysis and measure-theoretic probability, but there is also a connection to classical mechanics. Generalizations to higher dimensional cases are open.

Message sequence charts are an attractive formalism for specifying communicating systems. One way to test such a system is to substitute a component by a test process and observe its interaction with the rest of the system. Unfortunately, local observations can combine in unexpected ways to define implied scenarios not present in the original specification. Checking whether a scenario specification is closed with respect to implied scenarios is known to be undecidable when observations are made one process at a time. We show that even if we strengthen the observer to be able to observe multiple processes simultaneously, the problem remains undecidable. In fact, undecidability continues to hold even without message labels, provided we observe two or more processes simultaneously. On the other hand, without message labels, if we observe one process at a time, checking for implied scenarios is decidable.

Motivated by considerations in XML theory and model checking, data strings have been introduced as an extension of finite alphabet strings which carry, at each position, a symbol a data value from an infinite domain. Previous work has shown that it is not easy to come up with an expressive yet decidable automata model for data languages. Recently, such an automata model, , was introduced. This paper introduces a simpler but equivalent model and investigates its expressive power, algorithmic and closure properties and some extensions.

In most mainstream object-oriented languages, the object initialization protocol is based on constructors, where different constructors of the same class are, in fact, overloaded variants of the same method. This approach has some disadvantages: it forces an exponential growth of the code with respect to the number of properties, it may cause duplication of code, and it may create unnecessary code dependencies.

To the best of our knowledge, the literature lacks formal proposals that model non-trivial object initialization protocols.

In this paper we present a calculus (called FJMIP), which is an extension of the Igarashi-Pierce-Wadler Featherweight Java and models a novel object initialization protocol. Our calculus is reasonably simple, but it offers two benefits: () it formalizes a modular way of initializing objects that does not suffer from the previous mentioned flaws, while still being an expressive object initialization protocol; () as a by-product, it allowed us to introduce a novel technique to prove that our object initialization process actually initializes all the fields of an object.