Rapporti tecnici

We introduce Oikos_adtl, a specification language for distributed systems based on asynchronous communication via remote writings. The language is designed to support the composition of specifications. It allows expressing the global properties of a system in terms of the local properties of the components and of coordination patterns. Oikos_adtl is based on an asynchronous, distributed, temporal logic, which extends Unity to deal with components and events. We present the specification language and its semantics, introduce a number of compositionality theorems, and discuss some coordination patterns. A fragment of a standard case study is used to validate pragmatically the approach, with respect to expressiveness and work-ability.

This paper presents a new graph theoretic framework for the passenger assignment problem that encompasses simultaneously the departure time and the route choice. The implicit FIFO access to transit lines is taken into account by the concept of available capacity. This notion of flow priority has not been considered explicitly in previous models. A traffic equilibrium model is described and a computational procedure based on asymmetric boarding penalty functions is suggested.

In this paper we present history-dependent automata (HD-automata in brief). They are an extension of ordinary automata that overcomes their limitations in dealing with history-dependent formalisms. In a history-dependent formalism the actions that a system can perform carry information generated in the past history of the system. The most interesting example is pi-calculus: channel names can be created by some actions and they can then be referenced by successive actions. Other examples are CCS with localities and the history-preserving semantics of Petri nets. Ordinary automata are an unsatisfactory operational model for these formalisms: infinite automata are obtained for all the systems with infinite computations, even for very simple ones; moreover, the ordinary definition of bisimulation does not apply in these cases, thus preventing the reusage of standard theories and algorithms. In this paper we show that HD-automata are an adequate model for the history-dependent formalisms. We present translations of pi-calculus, CCS with localities and Petri nets into HD-automata; and we show that finite HD-automata are obtained for significant classes of systems with infinite computations. We also define HD-bisimulation, both in a set-theoretical way (that is suitable for automatic verification in the case of finite HD-automata) and in a categorical way (by exploiting open maps). HD-bisimulation captures the classical definitions of bisimulation on the considered history dependent formalisms.

The authors of Logo wanted to create a tool to help children build and explore the world of programming as means of building and exploring their own logical thought. The strength of this idea is particular and the turtle has carried his work out well. Today, however, new programming paradigms call for new metaphors and the technological gap between the turtle and modern graphic and multimedia programs seems to make less powerful the original Logo metaphor. In this paper we propose to enhance standard Logo by introducing modern program paradigms. In particular we extend Logo with object-oriented programming and multi-agent programming features. This new language is called YALL and try to change the way of programming Logo without abandon the original philosophy of the language. We introduce a new approach to express the inheritance relation that is more suitable for children. We discuss about these new extensions to Logo describing the new commands introduced. We also discuss a possible implementation of YALL using the Java language by Sun Microsystems.

By providing a matrix version of Koenig's theorem we reduce the problem of evaluating the coefficients of a monic factor $r(z)$ of degree $h$ of a power series $f(z)$ to that of approximating the first $h$ entries in the first row of the inverse of an infinite Toeplitz matrix in block Hessenberg form. This matrix is reduced to a band matrix if $f(z)$ is a polynomial. We devise a suitable algorithm, based on cyclic reduction and on the concept of displacement rank, for generating a sequence of vectors $\B v^{(2^j)}$ that quadratically converges to the vector $\B v$ having as components the coefficients of the factor $r(z)$. In the case of a polynomial $f(z)$ of degree $N$, the cost of computing the entries of $\B v^{(2^j)}$ given $\B v^{(2^{j-1})}$ is $O(N\log N+\theta(N))$, where $\theta(N)$ is the cost of solving an $ N\times N$ Toeplitz-like system. In the case of analytic functions the cost depends on the numerical degree of the power series involved in the computation. The algorithm is strictly related to the Graeffe method for lifting the roots of a polynomial. From the numerical experiments performed with several test polynomials and power series, the algorithm has shown good numerical properties and promises to be a good candidate for implementing polynomial rootfinders based on recursive splitting

In a similar way as 2-categories can be regarded as a special case of double categories, rewriting logic (in the unconditional case) can be embedded into the more general tile logic, where also side-effects and rewriting synchronization are considered. Since rewriting logic is the semantic basis of several language implementation efforts, it is useful to map tile logic back into rewriting logic in a conservative way, to obtain executable specifications of tile systems. We extend the results of earlier work by two of the authors, focusing on some interesting cases where the mathematical structures representing configurations (\ie, states) and effects (\ie, observable actions) are very similar, in the sense that they have in common some auxiliary structure (\eg, for tupling, projecting, etc.). In particular, we give in full detail the descriptions of two such cases where (net) process-like and usual term structures are employed. Corresponding to these two cases, we introduce two categorical notions, namely, symmetric strict monoidal double category and cartesian double category with consistently chosen products, which seem to offer an adequate semantic setting for process and term tile systems. The new model theory of 2EVH-categories required to relate the categorical models of tile logic and rewriting logic is presented making use of a recently developed framework, called partial membership equational logic, particularly suitable to deal with categorical structures. Consequently, symmetric strict monoidal and cartesian classes of double categories and 2-categories are compared through their embedding in the corresponding versions of 2EVH-categories. As a result of this comparison, we obtain a correct rewriting implementation of tile logic. This implementation uses a meta-layer to control the rewritings, so that only tile proofs are accepted. Making use of the reflective capabilities of the Maude language, some (general) internal strategies are then defined to implement the mapping from tile systems into rewriting systems, and some interesting applications related to the implementation of concurrent process calculi are presented.

An important class of problems in manufacturing system are those in which there is an item to be produced, a set of components which can be assembled together in order to obtain the wanted item, and a set of machines which are capable to perform the assembly operations. Here we consider the case in which one wants to find an optimal list of assembly operations. After discussing several optimality criteria, we address the problem in which the assembly operations are to be chosen in such a way that they can be scheduled on the available machines at minimum makespan. We show that these problems can be quite naturally modelled making use of Directed Hypergraphs, and describe a general heuristics, showing that in a particular but still relevant case, it yields solutions whose relative error is bounded. We present also a special class of assembly problems which can be solved in polynomial time by means of hyperpath computations.

This work involves two areas of research in computer science, namely Knowledge Representation and Logic Programming. Starting from the formalism proposed in Features Fluents by Erik Sandewall for describing and reasoning about Inhabited Dynamical Systems, we try to reconstruct it within a Logic Programming framework. The result is an extended logic programming language called Fluent Logic Programming (FLP) capable to deal with the main issues of the frame problem, in the context of Reasoning about Action and Change. From one point of view, FLP is the reconstruction of the proof-theory for the Sandewall's Discrete Fluent Logic by means of Meta-Logic Programming, on the other it is an attempt to integrate Temporal Reasoning and Logic Programming. In order to show soundness and completeness results between the Underlying Semantics and the Meta-Logical Semantics on which FLP is based, we provide a new abstract semantics for FLP as a bridge between them.

We propose a class of generalized Bundle methods where the stabilizi= term can be any closed convex function satisfying certain properties. = We prove finite termination, asymptotic convergence and finite convergenc= e to an optimal point of different variants of the algorithm: for some of= these proofs, f-regularity of the function (a new generalization of inf-= compactness) is required. Our analysis gives a unified convergence proof = for several classes of Bundle methods that have been so far regarded as d= istinct, enhancing on the results known for some of them: furthermore, it= covers methods proposed in the literature that had not previously been r= ecognised as Bundle methods. A novelty in our approach is the proposal of= a dual for the minimization problem: we show that Bundle methods can be = seen as a dual ascent approach to one single nonlinear problem in the dua= l space, where nonlinear subproblems are approximately solved at each ste= p with an inner linearization approach. This interpretation is particular= ly

We present a categorical formulation of the rewriting of possibly cyclic term graphs, and the proof that this presentation is equivalent to the well-accepted operational definition proposed by Barendregt et al., but for the case of circular redexes, for which we propose (and justify formally) a different treatment. The categorical framework, based on suitable 2-categories, allows to model also automatic garbage collection and rules for sharing/unsharing and folding/unfolding of structures. Furthermore, it can be used for defining various extensions of term graph rewriting, and for relating it to other rewriting formalisms.

This report formally defines the class of all problems on {\em Reasoning about Actions and Change}, where accurate and complete information about actions, together with strict inertia in continuous time, continuous change and alternative results of possibly concurrent and independent actions are the assumed properties. The intended model set for each member in the class is defined in terms of a model-theoretic trajectory semantics. The case is designated, in the {\em Features and Fluents} framework, with the~\KRACi family of reasoning problems. A fix-point characterization of the subclass \KspRAdCi is then given in terms of a simulative algebraic semantics, and show which are the difficulties when approaching the full class with that method. A non-simulative algebraic semantics is then presented as an alternative algebraic characterization of the model-theoretic trajectory semantics. Still the characterization is made in terms of complete lattices and continuous operators on those complete lattices. The algebraic semantics is shown to be correct and complete with respect to the trajectory-semantics, when applied to reasoning problems in \KRACi. Finally, adopting the non-simulative algebraic semantics as proof procedure, a logic-based {\em Calculus~of~Fluents} is defined, via a meta-theoretic extension of the Horn Clause Logic using the non-ground representation of object level variables. The meta-interpreter consists in the Horn clause representation of the proof procedure. The calculus is shown to be decidable, domain independent and class dependent; its semantics consists in the non-simulative algebraic semantics, and is executable as a logic program by the SLD-resolution rule.

One of the greatest difficulties involved in communication networks project is the need to interconnect different networks to form a unique internetwork. A major headache is the differing maximum packet sizes allowed by each network, which causes oversize packets to be broken up into appropriately sized fragments. Unfortunately, the fragmentation process implies additional costs, tightly bounded up with routing and fragmentation strategies in use. The approach commonly used in IP protocols provides two separated functions which operate in a completely indipendent way. This adversely affects network performance measures, both quantitatively (throughput) and qualitatively (average packet delay), whereas some form of cooperation between the two functions could result in a reduction of this efficiency loss. This paper presents a pseudo-polynomial algorithm for solving the combined fragmentation and routing problem. The method of solution is based on the concept of bicriterion shortest path problem, where two distinct objective functions must be minimized: the path length (in accordance with many classic routing algorithm) and the number of fragments received by the destination host. Besides, the paper deals with the problem of the effective fragments-hops minimization. An algorithm aimed at this purpose is provided together with the analysis of the possibility to reduce its running time under appropriate considerations on the generated fragment sizes.

We introduce the notion of $\exists$-universal termination of logic programs. A program P and a goal G $\exists$-universally terminate iff there exists a selection rule S such that every SLD-derivation of P U { G }$via S is finite. We claim that it is an essential concept for declarative programming, where a crucial point is to associate a terminating control strategy to programs and goals. We show that $\exists$-universal termination and universal termination via fair selection rules coincide. Then we offer a characterization of $\exists$-universal termination by defining fair-bounded programs and goals. They provide us with a correct and complete method of proving $\exists$-universal termination. We show other valuable properties of fair-bounded programs and goals, including persistency, modularity, ease of use in paper & pencil proofs, automatization of proofs.