Technical reports

It is fairly accepted that the realization of complex systems must be accomplished step by step from the initial specification, through a sequence of intermediate phases, to the final program. These development steps, linking a preliminary version, or description, of the program to a more detailed one, are usually called refinement steps, while the intermediate stages of a refinement process are called levels of abstraction. A refinement calculus is a means to support this modus operandi in program development, allowing to link different levels of abstraction: it introduces a precise relation between intermediate descriptions, and the rules to check whether the relation is satisfied. Tuple space languages are concurrent languages, that foster the definition of autonomous entities of computation (the processes), and offer mechanisms for their synchronization and communication. In particular, they represent one of the most acknowledged models of coordination. Tuple space languages are based on the idea that a dynamic collection of tuples can act as shared state of concurrent processes, and play the role of coordination media among them. To build a refinement calculus for tuple spaces, we address three points, in this paper: 1) We single out a specification language, a variation of first order temporal logic. Temporal relations between propositional formulae are not expressive enough to describe relations between tuple spaces, which are multisets of atoms. The specification language, called Oikos-tl, includes three new temporal operators that enhance the expressive power of the logic, permitting to directly link state transitions and state configurations. The semantics of the specification language is formally defined, and a set of useful properties for refinement are shown. 2) We introduce a reference language for tuple spaces, dubbed TuSpRel, and define its axiomatic and operational semantics. We need the former to derive properties, the latter to describe the allowed computations of a system. We relate these descriptions, and guarantee that using the axiomatic semantics we can derive properties, which are correct and complete with respect to the operational behaviour. The non-deterministic features of tuple space languages make this result new, and more complex than in other programming paradigms. One of the contributions of our work is the idea to derive weakest preconditions exploiting the demonic strict choice in non-deterministic selection. The transition system defining the operational semantics is based on the new notion of enabling precondition, which exploits the angelic strict choice. 3) To build the refinement calculus, we take a compositional approach. We first consider the basic statements of the language, and say under which conditions they satisfy a property, then compose these proofs to derive that a system refines a specification. Finally, in the refinement calculus definition, we extend to tuple space languages the ability to exploit logic formulae to specify the behaviour of unrefined modules: in the intermediate steps, a system is only partially written in the programming language, and the still unrefined features are described by logical formulae.

In this paper we focus on the notion of metabolism and the way it can be expressed in symbolic terms. We show as an adequate logical formalization of this concept could help to unify several approaches based in string rewriting mechanism. This viewpoint suggests new perspectives in the search for more powerful and general methods in the description of symbolic dynamical systems where evolution obeys some internal laws of structural recombination (L-systems, Grammar systems, H-systems, Ecogrammars, DNA computing models).

In un recente lavoro [13] e` stato proposto un modello di tipo logit gerarchico per l'assegnazione dei flussi ad una rete di trasporto collettivo urbano. Nel modello viene ipotizzato, su alcune ipotesi comportamentali dei passeggeri, che ad ogni fermata e per ogni destinazione venga considerato come attivo al piu` un iperarco di salita. In questo lavoro, dopo un'introduzione al modello logit di Dial [6] volta a mostrare come per il trasporto privato un modello logit di tipo globale coincide con un modello gerarchico, viene analizzato il modello proposto in [13] e vengono formulate ipotesi alternative di comportamento dei passeggeri che implicano la possibile presenza di piu` iperarchi attivi alla medesima fermata per la medesima destinazione. Viene quindi proposta una tecnica di risoluzione del modello, piu` generale di quella descritta in [13], e vengono mostrati gli effetti delle diverse ipotesi su alcuni casi test.

Completeness in abstract interpretation is an ideal situation where the abstract semantics is able to take full advantage of the power of representation of the underlying abstract domain. Thus, complete abstract interpretations can be rightfully considered as optimal. In this article, we develop a general theory of completeness in abstract interpretation, also dealing with the most frequent case of least fixpoint semantics. We show that both completeness and least fixpoint completeness are properties that only depend on the underlying abstract domain. In this context, we demonstrate that there always exist both the greatest complete and least fixpoint complete restrictions of any abstract domain, and for continuous semantic functions, the least complete extension exists as well. Also, under certain hypotheses, a constructive characterization of the least complete extensions and restrictions of abstract domains is given as solutions of simple abstract domain equations. These methodologies provide advanced algebraic tools for manipulating and comparing abstract interpretations, which can be fruitfully used both in program analysis and in semantics design. A number of examples illustrating these techniques are given in the fields of integer variable and logic program analysis.

We introduce the new Masked Interval Routing Scheme, MIRS for short, where a maskis added to each interval to indicate particular subsets of "consecutive" labels. Interval routing becomes more flexible, with the classical IRS scheme being a special case of MIRS. We then take two directions. First we show that the interval information stored in the network may be drastically reduced in the hard cases, proving that in globe graphs of O(n^2) vertices the number of intervals per edge goes down from Omega(n) to O(log n). The technique is then extended to globe graphs of arbitrary dimensions. Second we show that MIRS may be advantageously used in fault-tolerant networks, proving that optimal routing with one interval per edge is still possible in hypercubes with a "harmless" subset of faulty vertices. This work is aimed to introducing a new technique. Further research is needed in both the directions taken here. Still, the examples provided show that MIRS may be useful in practical applications.

For a simple CCS-like language a trace semantics and a failure semantics are presented. The failure semantics is shown to be fully abstract with respect to the trace semantics if and only if the set of internal actions is infinite.

Well-known metric spaces for modelling finitely branching and image finite systems are shown to be (the carrier of) terminal coalgebras.

According to Italian law, monitoring is a kind of quality control that must be performed during the carrying out of contracts regarding the information systems of Italian Public Bodies. This technical report describes and analyses monitoring as a tool to guarantee the quality of software production and consequently to assure the customer's satisfaction. It presents the institutional context in which monitoring is used, its activities, its purposes, its areas of application, and its relation to other kinds of quality control.

This paper investigates the advantages of reasoning on logic programs and queries that have only successful derivations. We consider an extension of the logic programming paradigm that combines guarded clauses, in the style of concurrent logic languages, and dynamic selection rules. Some general conditions for a class of programs and queries are stated, which characterize when successful derivations only are present. A few practical instances of the general conditions are studied, and their applicability to real programs demonstrated. The main contributions of the proposed method are: (i) don't care non determinism can be safely adopted for programs that do not fail, (ii) termination of process networks expressed as logic programs can be proved, by means of a simple proof method developed for a fixed selection rule, and (iii) a strategy for parallelizing terminating Prolog programs is identified.

"Acyclic" Term Graphs are able to represent terms with sharing, and the relationship between Term Graph Rewriting (TGR) and Term Rewrtiting (TR) is now well understood. During the last years, some researchers considered the extension of TGR to possibly "cyclic" term graphs, which can represent possibly infinite, rational terms. In [Kennaway et.al.,1994] the authors formalize the classical relationship between TGR and TR as an "adequate mapping" between rewriting systems, and extend it by proving that unraveling is an adequate mapping from cyclic TGR to rational, infinitary term rewriting: In fact, a single graph reduction may correspond to an infinite sequence of term reductions. Using the same notions, we propose a different adequacy result, showing that unraveling is an adequate mapping from cyclic TGR to "rational parallel term rewriting" , where at each reduction infinitely many rules can be applied in parallel. We also argue that our adequacy result is more natural than that proposed in [Kennaway et.al.,1994], because the length of the reduction sequences is preserved by unraveling, and collapsing rules are treated in a completely uniform way.

An algorithm for the computation of the LU factorization over the integers of an $n\times n$ Bezoutian $B$ is presented. The algorithm requires $O(n^2)$ arithmetic operations and involves integers having at most $O(n\log nc)$ bits, where $c$ is an upper bound of the moduli of the integer entries of $B$. As an application, by using the correlations between Bezoutians and the Euclidean scheme, we devise a new division-free algorithm for the computation of the polynomial pseudo-remainder sequence of two polynomials of degree at most $n$ in $O(n^2)$ arithmetic operations. The growth of the length of the integers involved in the computation is kept at the minimum value, i.e., $O(n\log nc)$ bits, no matter if the sequence is normal or not, where $c$ is an upper bound of the moduli of the input coefficients. The algorithms, that rely on the Bareiss technique and on the properties of the Schur complements of Bezoutians , improve the previous ones.

A labelled transition system is presented for Milner's pi_epsilon-calculus. This system is related to the reduction system for the calculus presented by Bellin and Scott. Also a reduction system and a labelled transition system for pi_epsilonI-calculus are given and their correspondence is studied. This calculus is a subcalculus of pi_epsilon-calculus in the way Sangiorgi's piI-calculus is a subcalculus of ordinary pi-calculus.

The marriage between logic programming and databases has given rise to the definition of deductive databases. These systems allow the users to express data manipulations and queries in a declarative way, and permit efficient storage and retrieval of intensional knowledge. Another improvement in the database field has come from the use of active rules, linking the occurrence of certain events to a reaction (e.g., updates of some data). This kind of rules has proven to be very useful to ensure integrity constraints and to automatize common procedures. This paper presents an integration of active rules in U-Datalog, which is an extension to Datalog supporting declarative specification of updates based on a nonimmediate update semantics. The resulting language, called Active-U-Datalog, extends the semantics of U-Datalog in a conservative way, introducing a PARK-like semantics for active rules activation and firing, and for handling conflicting update requests.

We introduce a practical method for abductive analysis of modular logic programs. This is obtained by reversing the deduction process, which is usually applied in static-dataflow analysis of logic programs, on generic, possibly abstract, domains for analysis. The approach is validated in the framework of abstract interpretation. The abduced information provides an abstract specification for program modules which can be of assistance both in top-down development of programs and in compile-time optimization. To the best of our knowledge this is the first application of abductive reasoning in dataflow analysis of logic programs.

We define the notion of meet-uniformity for closure operators on a complete lattice, which corresponds to co-additivity restricted to subsets mapped into the same element, and we study its properties. A class of closures given by principal filters and the downward closures are relevant examples of meet-uniform closures. Next, we introduce a lifting of a complete order by means of a meet-uniform closure. Our main results show that this lifting preserves the complete lattice structure, and allows the meet-uniform closure to become fully co-additive.

In the context of standard abstract interpretation theory, we define and study a systematic operator of reduced relative power for composing functionally abstract domains. The reduced relative power of two abstract domains D1 (the exponent) and D2 (the base) consists in a suitably defined lattice of monotone functions from D1 to D2, called dependencies, and it is a generalization of the Cousot and Cousot operator of reduced (cardinal) power. The relationship between the reduced relative power and Nielson's tensor product is also investigated. The case of autodependencies (when base and exponent are the same domain) turns out to be particularly interesting: Under certain hypotheses, the domain of autodependencies corresponds to a suitable powerset-like completion of the base abstract domain, providing a compact lattice-theoretic representation for autodependencies. The usefulness of the reduced relative power is shown by a number of applications to abstract domains used both for program analysis and for semantics design. Notably, we prove that the domain Def for logic program ground-dependency analysis can be characterized as autodependencies of a standard more abstract domain representing plain groundness only, and we show how to exploit reduced relative power to systematically derive compositional logic program semantics.

Shortest Path Problems are among the most studied network flow optimization problems, with interesting applications in various fields. One of such field is transportation, where shortest path problems of different kinds need to be solved. Due to the nature of the application, transportation scientists need very flexible and efficient shortest path procedures, both from the running time point of view, and also for the memory requirements. Since no "best" algorithm currently exists for every kind of transportation problem, research in this field has recently moved to the design and implementation of "ad hoc" shortest path procedures, which are able to capture the peculiarities of the problems under consideration. The aim of this work is to present in a unifying framework both the main algorithmic approaches that have been proposed in the past years for solving the shortest path problems arising most frequently in the transportation field, and also some important implementaion techniques which allow one to derive efficient procedures from the general algorithmic schema, in line with trends in current research. In the first part of the paper, afetr presenting the problem, we review those classical primal and dual algorithms which seem to be the most interesting in transportation. Promising reoptimization approaches are then discussed. The second part is devoted to dynamic shortest path problems, which arise very frequently in the transportation field. We analyse the main features and propose a general "chronological" algorithmic paradigm, called Chrono-SPT. We study several special cases, and investigate promising research avenues related to various extensions (time-windows. turn penalties, multicriteria and shortest hyperpaths).

The aim of this report is to make a review on DNA computing: molecular biology is used to suggest a new way of solving a NP-complete problem. The idea (due to Leonard Adleman in [Adl94]) is to use strands of DNA to encode the (instance of the) problem, and to manipulate them using techniques commonly available in any molecular biology laboratory, in order to simulate operations that select the solution of the problem, if it exists. After Adleman's paper (appeared on "Science" in November 1994), many authors have been interested in DNA computing. We will try to give a description of the discussions and the results which appeared in literature.

Frequently, in control system design, we are asked to locate the roots of a bivariate polynomial of the following form \begin{eqnarray*} H(s,k)=\sum_{i=0}^n Q_i(s) k^i\in {\bf Z}[k,s]={\bf Z}[k][s]={\bf D}[s], \end{eqnarray*} where $Q_i(s)\in {\bf Z}[s]$ for each $i$ and, moreover, $k$ is a free parameter ranging in some real interval. For a fixed value $\bar k$ of $k$, the zero distribution of the univariate polynomial $p(s)=H(s,\bar k)$ with respect to the imaginary axis can be found by determining the inertia of a Bezout matrix $B=B(\bar k)$ whose entries are expressed in terms of the coefficients of $p(s)$. This evaluation is usually accomplished by computing a block factorization of $B$, namely, $U^TBU=D$ where $D$ is a block diagonal matrix with lower triangular blocks with respect to the antidiagonal. It is intended in this paper to propose an efficient hybrid approach for determining the zero-distribution of $H(s,k)$ with respect to the imaginary axis for any value of $k$. We develop a fast fraction-free method for factoring the Bezout matrix $B(k)$ with entries over ${\bf D}$ determined by $H(s,k)\in {\bf D}[s]$. In this way, we easily compute the sequence $\{\phi_i(k)\}$ of the trailing principal minors of $B(k)$. For almost any value $\bar k$ of $k$ the associated sign sequence $\{sign(\phi_i(\bar k))\}$ specifies the inertia of $B(\bar k)$ and, therefore, the zero-distribution of $H(s,\bar k)$. The function $sign(\phi_i( k))$ is finally obtained by numerically computing rational approximations of the real zeros of $\phi_i(k)\in {\bf Z}[k]$.

In this paper first order logic is used for expressing syntax of formal languages. A model Syn is introduced and it is shown that whitin it syntactic relations and classes of languages are representable by means of first order formulae. The class of Sigma*(1) formulae is defined as an extension of arithmetical Sigma(1) formulae; then, a theory is considered where many syntactical notions can be developed in terms of axiomatic representability. This logical approach seems adequate to analyze and to integrate in a unique framework several grammatical models that emerge in the search for new computational paradigms.

This document concerns with the implementation of the P3L parallel programming language on the MPI abstract Machine. First we focus our attention on the characteristics of the MPI Abstract Machine, then we present a preliminary implementaton for each P3L construct based on that architecture.

We propose a proof method in the style of Hoare's logic, aimed at providing a unifying framework for the verification of logic and Prolog programs with respect to their specifications. The method, which relies on purely declarative reasoning, has been designed as a trade-off between expressive power and ease of use. On the basis of a few simple principles, we reason uniformly on several properties of logic and Prolog programs, including partial correctness, total correctness, absence of run-time errors, safe omission of the occur-check, computed answers, modular program development. We finally generalize the method to general programs.

The program composition approach can be fruitfully applied to combine general logic programs, i.e. logic programs possibly containing negative premises. We show how the introduction of a basic set of (meta-level) composition operations over general programs increases the knowledge representation capabilities of logic programming for non-monotonic reasoning. Examples of modular programming, hierarchical reasoning, constraints and rules with exceptions will be illustrated. The semantics of programs and program compositions is defined in terms of three-valued logic. The computational interpretation of program compositions is formalised by an equivalence preserving syntactic transformation of arbitrary program compositions into standard general programs.

A new algorithm is presented for computing an integer polynomial similar to the GCD of two polynomials $u(x)$ and $v(x)$ $\in {\bf Z}[x]$, $\deg(u(x))=n\geq \deg(v(x)) $. Our approach uses structured matrix computations involving Bezout matrices rather than Hankel matrices. In this way we reduce the computational costs showing that the new algorithm requires $O(n^2)$ arithmetical operations or $O(n^4(\log^2 n +l^2))$ Boolean operations, where $l=\max \{ \log(\parallel u(x) \parallel_{\infty}), \log(\parallel v(x) \parallel_{\infty})\}$.