DISI Technical Reports

2002

1. DISI-TR-02-04
   M. Ancona, W. Cazzola
   The Programming Language Io
2. DISI-TR-02-03
   F. Masulli, S. Rovetta
   Soft Transition from Probabilistic to Possibilistic Fuzzy Clustering
   We discuss the graded possibilistic model. We review some clustering algorithms derived from the basic c-Means and introduce a formalism to provide an alternative, unified perspective on these clustering algorithms, focused on the memberships rather than on the cost function. An interesting case is the concept of graded possibility. Its formulation includes as the two extreme cases the "probabilistic" assumption and the "possibilistic" assumption. A possible formulation can be stated as an interval equality constraint enforcing both the normality condition and the required graded possibilistic condition. We outline a basic example of graded possibilistic clustering algorithm. The experimental demonstrations presented aim at highlighting the different properties attainable through appropriate implementation of a suitable graded possibilistic model.
3. DISI-TR-02-02
   E. Bertino, G. Guerrini, M. Mesiti
   Measuring the Structural Similarity among XML Documents and DTDs
   Sources of XML documents are today proliferating on the Web. A relevant feature of such sources is that they are highly dynamic. New documents are continuously entered into such sources, by possibly acquiring them from other sources, and current documents are frequently updated. Being up to date is an imperative for many document sources. Such a wealth of documents requires exploiting database tools for managing these data. In this respect, an important feature of XML is that information on document structures is available on the Web together with the document contents. This information can be exploited to improve document handling and to improve query processing. However, in such a heterogeneous environment as the Web, it is not reasonable to assume that the XML documents entering a source always conform to a predefined DTD present in the source. There is therefore a strong need for methodologies and tools supporting the process of XML document classification with respect to DTD, and for grouping together documents with similar structure. In this paper we propose a metric for quantifying the structural similarity between an XML document and a DTD. A relevant application of this metric is document classification: the metric is used for selecting the DTD, among the ones in the source, whose structure is the most similar to the structure of the document. In the paper we motivate the choice of the metric, we present an algorithm for matching a document against a DTD to obtain their structural similarity value, and we present experimental results to assess how effective our approach is.
4. DISI-TR-02-01
   E. Danovaro, L. De Floriani, P. Magillo, E. Puppo
   Data Structures for 3D Multi-Tessellations: an Overview
   Multiresolution models support the interactive visualization of large volumetric data through selective refinement, an operation which permits to focus resolution only on the most relevant portions of the domain, or in the proximity of interesting field values. A three-dimensional Multi-Tessellation (MT) is a multiresolution tetrahedral mesh, consisting of a coarse tetrahedral mesh at low resolution, and of a set of updates refining such a mesh, arranged as a partial order. In this paper, we first describe a general data structure for a three-dimensional Multi-Tessellation based on the explicit representation of its tetrahedra, that we call an explicit representation of an MT. Then, we present two compact data structures which permit to encode a 3D MT built through the two most common techniques for incremental mesh simplification, i.e., edge collapse and vertex insertion. Such structures support selective refinement efficiently, and their storage cost is lower not only than that of the explicit structure, but also than the cost of encoding the mesh at full resolution.

top

2001

1. DISI-TR-01-13
   W. Cazzola, M. Ancona, F. Canepa, M. Mancini,V. Siccardi.
   Shifting up Java RMI from P2P to Multi-Point
   In this paper we describe how to realize a java RMI framework supporting multi-point method invocation. The package we have realized allows programmers to build group servers that provide services in two different modes: fault tolerant and parallel behavior. Our extension is based upon the creation of entities which maintain a common state between different servers. This has been done extending the existing registry interface. From the user's point of view the multi-point RMI acts just like the traditional RMI system, and really the same architecture has been used.
2. DISI-TR-01-12
   M. Bozzano, G. Delzanno
   Beyond Parameterized Verification: on Automated Verification of Multi-client Protocols with Unbounded Local Data
3. DISI-TR-01-11
   L. De Floriani, M. M. Mesmoudi, F. Morando, E. Puppo
   Decomposition of n-dimensional complex into quasi-manifold components
   In this paper we consider the problem of decomposing a non-manifold n-dimensional object described by an abstract simplicial complex into an assembly of 'more-regular' components. Manifolds, which would be natural candidates for components, cannot be used to this aim in high dimensions because they are not decidable sets. Therefore, we define d-quasi-manifolds, a decidable superset of the class of combinatorial d-manifolds that coincides with d-manifolds in dimension less or equal than two. We first introduce the notion of d-quasi-manifold complexes, then we sketch an algorithmic procedure to decompose an arbitrary complex into an assembly of quasi-manifold components abutting at non-manifold joints. This result provides a rigorous starting point for our future work, which includes designing efficient data structures for non-manifold modeling, as well as defining a notion of measure of shape complexity of such models.
4. DISI-TR-01-10
   M. M. Mesmoudi, L. De Floriani
   Topological structure of differentiable scalar fields in two and three dimensional domains
   In this report we give an overview on the properties of Morse functions, in the difeerentiable and discretes cases, and their related topological, geometric and metric notions. This report is organised as follows. In Section 2, we discuss the topological properties of isolines and isosurfaces of differentiable functions defined on 2D and 3D domains. In Section 3, we discuss some properties of Morse functions which are useful in practice. In Section 4, we give a topological classificationof compact isolines and isosurfaces. In Section 5, we recall the notion of curvature which is an intrinsic metric propertiy of curves and surfaces and we give a mathematical classification of points on a surface according to their principal curvatures. This classification is useful for classifying critical points of a scalar field defined on 2D domains and for isosurfaces correponding to 3D scalar fields. In Section 6, we give a decomposition of 2D and 3D domains into regular and critical level sets corresponding to a scalar field. This decompostion allows us to represent, in the last Section, the topology of a scalar field defined on 2D or 3D domains by Reeb graphs, Extended Reeb graphs and Hyper Reeb graphs. A classification of critical points of a differentiable function is given in Section 7 and, in Section 8, we give some properties of the gradient flow of a function and we describe how to decompose the domain into cells and extract a critical graph formed by critical points and integral curves of the gradient vector field of the function. In the last section we give an overview on the important results of discrete Morse theory recently introduced by Forman for cell complexes.
5. DISI-TR-01-09
   A. Barla, F. Odone, A. Verri
   A Hausdorff Kernel for Image-based 3D Object Acquisition and Detection
   Learning one class at a time can be seen as an effective solution to classification problems in which only the positive examples are easily identifiable. A kernel method to accomplish this goal consists of a representation stage - which computes the smallest sphere in feature space enclosing the positive examples - and a classification stage - which uses the obtained sphere as a decision surface to determine the positivity of new examples. In this paper we describe a kernel well suited to represent, identify, and recognize 3D objects from unconstrained images. The kernel we introduce, based on Hausdorff distance, is tailored to deal with grey-level image matching. The effectiveness of the proposed method is demonstrated on several data sets of faces and of 3D objects of artistical relevance, like statues.
6. DISI-TR-01-08
   G. Delzanno, S. Etalle
   A Proof Theoretic Analysis of Security Protocols
7. DISI-TR-01-07
   G. Valentini
   Classification of human lymphoma using gene expression data.
   DNA microarrays provide us with a large amount of information about gene expression, offering a wide picture of the functional status of a cell. Information obtained by DNA microarray technology gives a snapshot of the overall functional status of a cell, offering new insights into potential different types of lymphoma, discriminated on molecular and functional basis. We apply supervised machine learning methods to the recognition and classification of human lymphoma, using gene expression data from "Lymphochip", a specialized DNA microarray developed at Stanford University School of Medicine. We show that Multi-Layer Perceptrons and Support Vector Machines can correctly separate cancerous from normal tissues, and Output Coding ensembles of learning machines can identify different types of lymphoma. Moreover our experimental results confirm the existence of distinct tumoral diseases inside the class of diffuse large B-cell lymphoma, offering also insights into the role of sets of coordinately expressed genes in carcinogenic processes of lymphoid tissues.
8. DISI-TR-01-06
   C. Andujar, L. De Floriani
   Optimal Encoding of Triangulated Polygons
   In this paper an efficient scheme for compressing the connectivity of a triangulated polygon is presented. Our scheme improves the storage required by previously reported schemes, most of which can guarantee only a 2(n-2) storage cost for the incidence graph $G$ of a triangulated polygon with n vertices. Our approach achives the theoretical lower bound on the length of the representation of G by requiring only [log E(n)] bits, where E(n) is the number of different triangulations of a polygon with n vertices. The encoding algorithm finds the rank of a given triangulation in a fixed enumeration scheme and the decoding algorithm retrieves the triangulation corresponding to a given rank in O(n log n) time. Both algorithms are easy to implement and empirical results demonstrate that they are efficient enough to be used in real-time.
9. DISI-TR-01-05
   F. Masulli, G. Valentini
   Evaluating dependence among output errors in ECOC learning machines
   One of the main factors affecting the effectiveness of ECOC methods for classification is the dependence among the errors of the computed codeword bits. We present an extended experimental work for evaluating the dependence among output errors of the decomposition unit of ECOC learning machines. In particular we quantitatively compare the dependence between ECOC Multi Layer Perceptrons (ECOC MLP), made up by a single MLP, and ECOC ensembles made up by a set of independent and parallel dichotomizers (ECOC PND), using measures based on mutual information. The experimentation analyzes the relations between the design, the dependence among output errors and the performances of ECOC learning machines. Results show that the dependence among computed codeword bits is significantly smaller for ECOC PND, pointing out that ensembles of independent dichotomizers are better suited for implementing ECOC classification methods. Moreover the experimental results suggest the research of new architectures of ECOC learning machines for improving the independence among output errors and the diversity between base learners.
10. DISI-TR-01-04
    D. Gil, P. Magillo
    "VARIANT: VAriable Resolution Interactive Analysis of Terrains"
11. DISI-TR-01-03
    G. Delzanno, J.F. Raskin, L. Van Begin
    Attacking Symbolic State Explosion in Parameterized Verification
12. DISI-TR-01-02
    F. Masulli, G. Valentini.
    Mutual information methods for evaluating dependence among output errors in learning machines
    The evaluation of dependence between outputs of  multi input multi output learning machines can  highlight hidden interactions among their internal components that add noise to the learning process. In this paper we propose mutual information based measures for evaluating the independence among the outputs of a  learning machine.  We distinguish between dependence among outputs and dependence among output errors and show how we can use  mutual information related quantities to evaluate both these types of dependencies. Estimating the dependence among output errors, we can also compare different  models of learning machines in order to select the one best suited to a particular problem. An application of the proposed measures to an experimental compared evaluation of the dependence among output errors of two different models of learning machines is given.
13. DISI-TR-01-01
    M. Bozzano, G. Delzanno, M. Martelli
    An Effective Bottom-Up Semantics for First Order Linear Logic Programs and its Relationship with Decidability Results for Timed Petri Nets.

top

2000

1. DISI-TR-00-17
   G. Valentini
   Upper bounds on the training error of ECOC-SVM ensembles
   ECOC-SVM are ensembles of learning machines for multiclass problems exploiting the accuracy of SVM dichotomizers and the error recovering capabilities of ECOC ensembles. Upper bounds on the training error of ECOC-SVM ensembles are presented. These results can also be extended to other decomposition methods, as One-Per-Class and Correcting Classifiers. The upper bounds show that the training error depend on the complexity of the dichotomies induced by the decomposition and on the error recovering power of the decomposition scheme.
2. DISI-TR-00-16
   D. Ancona, G. Lagorio, E. Zucca
   A Core Calculus for Java Exceptions
3. DISI-TR-00-15
   F. Odone, E. Trucco, A. Verri
   A novel correlation measure for grey level images: evaluation and experiments.
   In this paper we propose a novel similarity measure for grey level images, and we place it in the context of correlation methods: given two image windows, the method checks pixel-wise if the grey values of one are contained in an appropriate interval around the corresponding grey values of the other. The method fits naturally an implementation based on comparison of data structures and requires no numerical computations whatsoever. Moreover, it is able to match images successfully in the presence of severe occlusions. We also describe the method from a different point of view, as a measure inspired by the notion of directed Hausdorff distance; in this optic, the method proposed can be seen as one of the first attempt to exploit the Hausdorff distance as a similarity measure between grey level patterns. Another interesting property of this similarity method is that, under certain hypothesis, it can be used as a kernel of a learning machine. This means that the good property of robustness to occlusions, can be extended to bigger image classification problems. We describe various examples of applications, with results on real images.
4. DISI-TR-00-14
   F. Morando
   Cutting and Stitching Decomposition of Non-Manifold Models in Higher Dimension
5. DISI-TR-00-13
   E. Appiani, M. Martelli, V. Mascardi
   A Multi-Agent Approach to Vehicle Monitoring in Motorway
   This paper describes CaseLP, a prototyping environment for Multi-Agent Systems (MAS), and its adoption for the development of a distributed industrial application. CaseLP employs architecture definition, communication, logic and procedural languages to model a MAS from the top-level architecture down to procedural behavior of each agent's instance. The executable specification which is obtained can be employed as a rapid prototype which helps in taking quick decisions on the best possible implementation solutions. Such capabilities have been applied to a distributed application of Elsag company, in order to assess the best policies for data communication and database allocation before the concrete implementation. The application consists in remote traffic control and surveillance over service areas on an Italian motorway, employing automatic detection and car plate reading at monitored gates. CaseLP allowed to predict data communication performance statistics under different policies of database allocation.
   Frameworks and metamodels for the integration of specification concepts; Experience reports on the effectiveness of development methods in industrial practice
6. DISI-TR-00-12
   D. Ancona, E. Zucca
   True Modules for Java Classes
7. DISI-TR-00-11
   P. Magillo, L. De Floriani, E. Puppo
   A Dimension- and Application-Independent Library for Multiresolution Geometric Modeling
   We present a general-purpose software library for multiresolution geometric modeling in arbitrary dimensions. The core of the library is the Multi-Tesselation(MT), a general multiresolution model for representing k-dimensional geometric objects through simplicial complexes. An MT provides both simple and general methods for handling representations at variable resolution efficiently, thus offering a basis for applications that need to manage the level-of-detail of complex objects. The library is fully parametric on dimensions of the simplicial complex and of the space embedding it, on the attributes that can be associated with its vertices and tiles, on the algorithms used for building the model, and on the criteria used for extracting variable-resolution representations from it.
8. DISI-TR-00-10
   R. Carvajal-Schiaffino, G. Delzanno, G. Chiola
   "Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets. -A New "Type 2" Validation Algorithm-"
   We propose a new validation algorithm for bounded Petri Nets. Our method combines state enumeration and structural techniques in order to compute under-approximations of the reachability set and graph of a net. The method is based on two heuristics that exploit the property of T-semiflows, the positive solutions of the system Cx = 0, C being the incidence matrix of the net. The main feature of the resulting algorithm is that it always works on a window covering a fixed-a-priori number of the last levels of the partially constructed reachability graph. This property allow us to use a specialized organization of the memory in which we maintain the space used to store the reachable markings as a circular array. This data structure allow us to re-use all memory allocated to markings outside the working window. Furthemore, our algorithm dynamically measures the quality of the approximation it computes. We apply the method for validating non-artificial systems modeled as Petri Nets w.r.t. safety properties like mutual exclusion. Preliminary experiments show that these mechanisms can save up to 98% of the memory space needed to store the entire reachability set. Furthermore, the algorithm returns exact results (i.e. it verifies the considered properties) in all considered examples.
9. DISI-TR-00-09
   W. Cazzola, M. Ancona
   mChaRM: a Reflective Middleware for Communication-Based Reflection
   There are several classes of features which cannot be modeled (or are hard to be modeled) within the currently available reflective models. One problem is represented by the lack of global view inherited from the object-oriented paradigm. This fact limits the potentialities of reflection, and reduces the application domain of the reflective paradigm especially when dealing with distributed programming. In the latter case, the more complex (often very hard to be treated) problems derive from communication mechanisms. In this paper we briefly examine the problems deriving when some enriching of the communication behavior is attempted via reflection. We also present a new reflective model, called the multi-channel reification approach, which extends some precedent proposal of the authors, and overcomes most of the limits of the actual reflective approaches. This model is especially designed both for designing and developing from scratch complex communication mechanisms or for extending the behavior of the communication mechanisms provided by the underlying system. To point out the soundness of our approach we also present mChaRM a reflective middleware, composed of a Java extension, an API, and a preprocessor, which realizes the approach described. Some applications realized with mChaRM are also presented.
10. DISI-TR-00-08
    E. Bertino, E. Ferrari, G. Guerrini, I. Merlo
    An ODMG Compliant Temporal Object Model Supporting Multiple Granularity Management
    In this paper we investigate some issues arising from the introduction of multiple temporal granularities in an object-oriented data model. Although issues concerning temporal granularities have been investigated in the context of temporal relational database systems, no comparable amount of work has been done in the context of object-oriented models. Moreover, the main drawback of the existing proposals is the lack of a formal basis -- which we believe is essential to manage the inherent complexity of the object-oriented data model. In this paper, we define a complete temporal object-oriented data model supporting multiple temporal granularities. We formally define the main notions of the data model such as types, legal values, classes, and objects. We address issues related to inheritance, type refinement, substitutability, and navigational access to objects. Finally, we describe the implementation of the presented model on top of an ODMG compliant DBMS.
11. DISI-TR-00-07
    P. Cignoni, L. De Floriani, P. Magillo, E. Puppo, R. Scopigno
    Visualization of Large Irregular Volume Datasets
12. DISI-TR-00-06
    M. Bozzano, G. Delzanno, M. Martelli
    A Bottom-up Semantics for LO - Preliminary Results
    The operational semantics of linear logic programming languages is given in terms of goal-driven sequent calculi for fragments of the logic. The proof-theoretic presentation is the natural counterpart of the top-down semantics of traditional logic programs. In this paper we investigate the theoretical foundation of an alternative operational semantics based on a bottom-up evaluation of linear logic programs via a fixpoint operator. The bottom-up fixpoint semantics is important in applications like active databases, and, more in general, for program analysis and verification. As a first case-study, we consider Andreoli and Pareschi's LO enriched with the connective 1. For this language, we give a fixpoint semantics based on an operator defined in the style of Tp. We give an algorithm to compute a single application of the fixpoint operator where constraints are used to represent in a finite way possibly infinite sets of provable goals. Furthermore, we show that the fixpoint semantics for propositional $LO$ without the connective 1 can be computed after finitely many steps. To our knowledge, this is the first attempt to define an effective fixpoint semantics for LO. We hope that our work will open interesting perspectives for the analysis and verification of linear logic programming languages.
13. DISI-TR-00-05
    G. Delzanno
    Verification of Consistency Protocols via Infinite-state Symbolic Model Checking - A Case Study -
    We apply infinite-state model checking for the verification of safety properties of a {\em parameterized} formulation of the IEEE FutureBus+ coherence protocol modeled at the behavior level in a system with split transaction. This case-study shows that verification techniques previously applied to hybrid and real-time systems can be used as tools for validating parameterized protocols. This technology transfer is achieved by combining abstraction techniques, symbolic representation via constraints, efficient operations based on real arithmetics, and reachability algorithms. To our knowledge this is the first time that safety properties for a parameterized version of the Futurebus+ protocol have been automatically verified.
14. DISI-TR-00-04
    F. Masulli, Gb. Cicioni, L. Studer
    Discontinuous and Intermittent Signal Forecasting: A Hybrid Approach.
    A constructive methodology for shaping a neural model of a non-linear process, supported by results and prescriptions related to the Takens-Mane theorem, has been recently proposed. Following this approach, the measurement of the first minimum of the mutual information of the output signal and the estimation of the embedding dimension using the method of global false nearest neighbors permits to design the input layer of a neural network or a neuro-fuzzy system to be used as predictor. In this paper we present an extension of this prediction methodology to discontinuous or intermittent signals. As the Universal function approximation theorems for neural networks and fuzzy systems requires the continuity of the function to be approximate, we apply the Singular-Spectrum Analysis (SSA) to the original signal, in order to obtain a family of time series components that are more regular than the original signal and can be, in principle, predicted one at a time using the mentioned methodology. On the basis of the properties of SSA, the prediction of the original series can be recovered as the sum of those of all the individual series components. We show an application of this prediction approach to a hydrology problem concerning the forecasting of daily rainfall intensity series, using a database collected for a period of 10 years from 135 stations distributed in the Tiber river basin.
15. DISI-TR-00-03
    G. Delzanno
    On Efficient Data Structures for the Verification of Parameterized Synchronous Systems
    We propose a fully-automatic method for checking safety properties of parameterized synchronous systems based on a backward reachability procedure working over real arithmetics. We consider here concurrent systems consisting of many identical (finite-state) processes and one monitor where processes may react non-deterministically to the messages sent by the monitor. This type of non-determinism allows us to model abstractions of situations in which processes are re-allocated according to individual properties. The resulting class of systems extend previously proposed models.

    We represent concisely collections of global states counting the number of processes in a given state during a run of the global system, i.e., we reason modulo symmetries. We use a special class of linear arithmetic constraints to represent collections of global system states. We define a decision procedure for checking safety properties for parameterized systems using efficient constraints operations defined over real arithmetics.

    The procedure can be implemented using existing constraint-based symbolic model checkers or tools for program analysis defined over real-arithmetics. In our experiments we have applied DMC and HyTech in order to verify safety properties for abstractions of control systems and cache coherence policies taken from the literature.

16. DISI-TR-00-02
    B. Catania, M. Martelli, L. Ventimiglia
    A constraint domain for combinatorial map simplification
    Constraint Logic Programming introduces constraints, belonging to a specific constraint domain, inside logical rules. The aim of this paper is the presentation of a constraint domain for combinatorial map simplification. Combinatorial map simplification is an important problem in geographical information systems and refers to the ability of specializing or generalizing the structure of a combinatorial map at different degrees of granularity. With combinatorial map we mean a map in which no metric aspects are considered. Rather, the map is only viewed in terms of the entities composing it and the relationships between them. In this paper, we first formally define the problem from a geometrical point of view. Then, we define a constraint domain supporting such application and we prove that it is well defined.
17. DISI-TR-00-01
    G. Delzanno
    Automatic Verification of Parameterized Cache Coherence Protocols
    We show that symbolic model checking techniques for {\em infinite-state systems} with numerical data variables can be applied successfully to the validation of {\em parameterized} cache coherence protocols. Cache coherence protocols are used to maintain data consistency in commercial multiprocessor systems where processors are equipped with local fast caches. Our approach exploits the symmetries present in the state-space of this class of infinite state-systems, by representing (possibly infinite) sets of global states as arithmetic constraints over integer counters. Preliminary experiments based on efficient constraint-based model checkers based on real arithmetics for hybrid and concurrent systems allowed us to validate automatically examples of widely implemented {\em write-invalidate} cache coherence policies like the Berkeley protocol and the Illinois Protocol. This application enlarges the scope of applicability of the techniques developed in the last years for hybrid and reactive systems to a new class of infinite-state systems.

top