DISI Technical Reports
2002 
2001 
2000
2002

DISITR0204
M. Ancona, W. Cazzola
The Programming Language Io

DISITR0203
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
cMeans 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.

DISITR0202
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.

DISITR0201
E. Danovaro, L. De Floriani, P. Magillo, E. Puppo
Data Structures for 3D MultiTessellations: 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
threedimensional MultiTessellation (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
threedimensional MultiTessellation 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

DISITR0113 W. Cazzola, M. Ancona, F. Canepa, M. Mancini,V. Siccardi.
Shifting up Java RMI from P2P to MultiPoint
In this paper we describe how to realize a java RMI framework
supporting multipoint 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 multipoint RMI acts just like the traditional RMI
system, and really the same architecture has been used.

DISITR0112 M. Bozzano, G. Delzanno
Beyond Parameterized Verification: on Automated Verification of
Multiclient Protocols with Unbounded Local Data

DISITR0111 L. De Floriani, M. M. Mesmoudi, F. Morando, E. Puppo
Decomposition of ndimensional complex into quasimanifold components
In this paper we consider the problem of decomposing a nonmanifold
ndimensional object described by an abstract simplicial complex into an
assembly of 'moreregular' 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 dquasimanifolds, a decidable superset of the
class of combinatorial dmanifolds
that coincides with dmanifolds in dimension less or equal than two.
We first introduce the notion of dquasimanifold complexes,
then we sketch an algorithmic procedure to decompose an arbitrary complex
into an assembly of quasimanifold components abutting at nonmanifold
joints.
This result provides a rigorous starting point for our future work, which
includes designing efficient data structures for nonmanifold
modeling, as well as defining a notion of measure of shape complexity of
such models.

DISITR0110 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.

DISITR0109 A. Barla, F. Odone, A. Verri
A Hausdorff Kernel for Imagebased 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 greylevel 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.

DISITR0108 G. Delzanno, S. Etalle
A Proof Theoretic Analysis of Security Protocols

DISITR0107 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 MultiLayer 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 Bcell
lymphoma, offering also
insights into the role of sets of coordinately expressed genes in
carcinogenic processes of
lymphoid tissues.

DISITR0106 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(n2)
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 realtime.

DISITR0105 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.

DISITR0104 D. Gil, P. Magillo
"VARIANT: VAriable Resolution Interactive Analysis of Terrains"

DISITR0103 G. Delzanno, J.F. Raskin, L. Van Begin
Attacking Symbolic State Explosion in Parameterized Verification

DISITR0102 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.

DISITR0101 M. Bozzano, G. Delzanno, M. Martelli
An Effective BottomUp Semantics for First Order Linear Logic Programs and its Relationship with Decidability Results for Timed Petri Nets.
top
2000

DISITR0017 G. Valentini
Upper bounds on the training error of ECOCSVM ensembles
ECOCSVM 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 ECOCSVM ensembles are presented.
These results can also be extended to other decomposition methods, as OnePerClass
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.

DISITR0016 D. Ancona, G. Lagorio, E. Zucca
A Core Calculus for Java Exceptions

DISITR0015 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
pixelwise 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.

DISITR0014 F. Morando
Cutting and Stitching Decomposition of NonManifold Models in Higher
Dimension

DISITR0013 E. Appiani, M. Martelli, V. Mascardi
A MultiAgent Approach to Vehicle Monitoring in Motorway
This paper describes CaseLP, a prototyping environment for
MultiAgent 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 toplevel
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

DISITR0012 D. Ancona, E. Zucca
True Modules for Java Classes

DISITR0011 P. Magillo, L. De Floriani, E. Puppo
A Dimension and ApplicationIndependent Library
for Multiresolution Geometric Modeling
We present a generalpurpose software library for multiresolution
geometric modeling in arbitrary dimensions.
The core of the library is the MultiTesselation(MT),
a general multiresolution model for representing kdimensional 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 levelofdetail 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 variableresolution representations from it.

DISITR0010 R. CarvajalSchiaffino, 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 underapproximations of the reachability set and graph of a
net. The method is based on two heuristics that exploit the property of
Tsemiflows, 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 fixedapriori 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 reuse 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 nonartificial 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.

DISITR0009 W. Cazzola, M. Ancona
mChaRM: a Reflective Middleware for CommunicationBased 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 objectoriented
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 multichannel 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.

DISITR0008 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 objectoriented 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 objectoriented 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 objectoriented data model.
In this paper, we define a complete temporal objectoriented 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.

DISITR0007 P. Cignoni, L. De Floriani, P. Magillo, E. Puppo, R. Scopigno
Visualization of Large Irregular Volume Datasets

DISITR0006 M. Bozzano, G. Delzanno, M. Martelli
A Bottomup Semantics for LO  Preliminary Results
The operational semantics of linear logic programming languages is
given in terms of goaldriven sequent calculi for fragments of the
logic.
The prooftheoretic presentation is the natural counterpart
of the topdown semantics of traditional logic programs.
In this paper we investigate the theoretical foundation of an
alternative
operational semantics based on a bottomup evaluation of linear
logic programs via a fixpoint operator.
The bottomup fixpoint semantics is important in applications
like active databases, and, more in general, for program analysis
and verification.
As a first casestudy, 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.

DISITR0005 G. Delzanno
Verification of Consistency Protocols via Infinitestate
Symbolic Model Checking  A Case Study 
We apply infinitestate 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 casestudy shows that verification techniques previously applied to
hybrid
and realtime 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.

DISITR0004 F. Masulli, Gb. Cicioni, L. Studer
Discontinuous and Intermittent Signal Forecasting: A Hybrid Approach.
A constructive methodology for shaping a neural model of a nonlinear
process, supported by results and prescriptions related to the
TakensMane 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 neurofuzzy 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 SingularSpectrum 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.

DISITR0003 G. Delzanno
On Efficient Data Structures for the Verification of
Parameterized Synchronous Systems
We propose a fullyautomatic 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 (finitestate) processes and one monitor
where
processes may react nondeterministically to the messages sent by the
monitor. This type of nondeterminism allows us to model abstractions of
situations in which processes are reallocated 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 constraintbased
symbolic model checkers or tools for program analysis defined over
realarithmetics. 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.

DISITR0002 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.

DISITR0001 G. Delzanno
Automatic Verification of Parameterized Cache Coherence Protocols
We show that symbolic model checking techniques for {\em infinitestate
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 statespace of this
class of infinite statesystems,
by representing (possibly infinite) sets of global states as arithmetic
constraints over integer counters.
Preliminary experiments based on efficient constraintbased model
checkers based on real arithmetics
for hybrid and concurrent systems allowed us to validate automatically
examples of widely
implemented {\em writeinvalidate} 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 infinitestate
systems.
top

