Technical reports


List of technical reports of year 2007

Bodei, Chiara and Degano, Pierpaolo and Gao, Han and Brodo, Linda
Detecting and Preventing Type flaws: a Control Flow Analysis with tags
December 9, 2014
UnipiEprints view

Download (html PUBLIC "-//W3) abstract

A type flaw attack on a security protocol is an attack where an honest principal is cheated on interpreting a field in a message as the one with a type other than the intended one. In this paper, we shall present an extension of the LySa calculus with tags attached to each field, indicating the intended types. We developed a control flow analysis for analysing the extended LySa, which over-approximates all the possible behaviour of a protocol and hence is able to capture any type confusion that may happen during the protocol execution. The control flow analysis has been applied to a number of security protocols, either subject to type flaw attacks or not. The results show that it is able to capture type flaw attacks on those security protocols.

Ghelli, Giorgio and Colazzo, Dario and Sartiani, Carlo
Efficient Inclusion for a Class of XML Types with Interleaving and Counting
December 9, 2014
UnipiEprints view

Inclusion between XML types is important but expensive, and is much more expensive when unordered types are considered. We prove here that inclusion for XML types with interleaving and counting can be decided in polynomial time in presence of two important restrictions: no element appears twice in the same content model, and Kleene star is only applied to disjunctions of single elements. Our approach is based on the transformation of each such type into a set of constraints that completely characterizes the type. We then provide a complete deduction system to verify whether the constraints of one type imply all the constraints of another one.

Nicotra, Luca and Micheli, Alessio and Starita, Antonina
A Comparative Study of Tree Generative Kernels for Gene Function Prediction
December 9, 2014
UnipiEprints view

In this report we perform a comparative study of kernel functions defined on generative models with the goal to embed phylogenetic information into a discriminative learning approach. We describe three generative tree kernels: a sufficient statistics kernel, a Fisher kernel, and a probability product kernel; their key features are the adaptivity to the input domain and the ability to deal with structured data. In particular, kernel adaptivity is obtained through the estimation of the parameters of a tree structured model of evolution from an input domain of phylogenetic profiles encoding the presence or absence of specific proteins in a set of fully sequenced genomes. We report results obtained in the prediction of the functional class of the proteins of the yeast S. Cervisae together with comparisons with a standard vector based kernel and with a non-adaptive tree kernel function. To further analyze the impact of the discriminative learning phase, and to provide an assessment of the information retained by the learned generative models we apply them directly to classification through log-odds. Finally, the advantage achieved through adaptivity for two of the new kernels is assessed through a comparison with similar kernels based on randomly initialized generative models where no learning is performed, and to kernels where parameters are set only on the base of biological considerations.

Pedreschi, Dino and Ruggieri, Salvatore and Turini, Franco
Discrimination-aware data mining
December 9, 2014
UnipiEprints view

In the context of civil rights law, discrimination refers to unfair or unequal treatment of people based on membership to a category or a minority, without regard to individual merit. Rules extracted from databases by data mining techniques, such as classification or association rules, when used for decision tasks such as benefit or credit approval, can be discriminatory, in the above sense. This deficiency of classification and association rules poses ethical and legal issues, as well as obstacles to practical application. In this paper, the notion of discriminatory classification rules is introduced and studied. Examples of potentially discriminatory attributes include gender, race, job, and age. A measure, termed $\alpha$-protection, of the discrimination power of a classification rule containing a discriminatory item is defined and its properties studied. We show that the introduced notion is non-trivial, in the sense that discriminatory rules can be derived from apparently safe ones under natural assumptions about background knowledge. Finally, we discuss how to check $\alpha$-protection and provide an empirical assessment on the German credit dataset.

Bruni, Roberto and Lluch Lafuente, Alberto and Montanari, Ugo and Tuosto, Emilio
Style-Based Architectural Reconfigurations
December 9, 2014
UnipiEprints view

We introduce Architectural Design Rewriting (ADR), an approach to deal with the design of reconfigurable software architectures. The key features we promote are: (i) rule-based approach (over graphs); (ii) hierarchical design; (iii) algebraic presentation; and (iv) inductively-defined reconfigurations. Architectures are suitably modeled by graphs whose edges and nodes respectively represent components and connection ports. Architectures are designed hierarchically by a set of edge replacement rules that fix the architectural style. Depending on their reading, productions allow: (i) top-down design by refinement, (ii) bottom-up typing of actual architectures, and (iii) well-formed composition of architectures. The key idea is to encode style proofs as terms and to exploit such information at run-time for guiding reconfigurations. The main advantages of ADR are that: (i) instead of reasoning on flat architectures, ADR specifications provide a convenient hierarchical structure, by exploiting the architectural classes introduced by the style, (ii) complex reconfiguration schemes can be defined inductively, and (iii) style-preservation is guaranteed.

Aldinucci, Marco and Danelutto, Marco and Kilpatrick, Peter
Orc + metadata supporting grid programming
December 9, 2014
UnipiEprints view

Following earlier work demonstrating the utility of Orc as a means of specifying and reasoning about grid applications we propose the enhancement of such specifications with metadata that provide a means to extend an Orc specification with implementation oriented information. We argue that such specifications provide a useful refinement step in allowing reasoning about implementation related issues ahead of actual implementation or even prototyping. As examples, we demonstrate how such extended specifications can be used for investigating security related issues and for evaluating the cost of handling grid resource faults. The approach emphasises a semi-formal style of reasoning that makes maximum use of programmer domain knowledge and experience.

Ferragina, Paolo and Nitto, Igor and Venturini, Rossano
Succinct Oracles for Exact Distances in Undirected Unweighted Graphs
December 9, 2014
UnipiEprints view

Let G be an unweighted and undirected graph of n nodes, and let D be the n x n matrix storing the All-Pairs-Shortest-Path distances in G. Since D contains integers in [n], its plain storage takes n^2log (n + 1) bits. However, a simple counting argument shows that n^2/2 bits are necessary to store D. In this paper we investigate the question of finding a succinct representation of D that requires O(n^2) bits of storage and still supports constant-time access to each of its entries. This is asymptotically optimal in the worst case, and far from the information-theoretic lower-bound by a multiplicative factor log 3 \simeq 1.585. As a result O(1) bits per pairs of nodes in G are enough to retain constant-time access to their shortest-path distance. We achieve this result by reducing the storage of D to the succinct storage of labeled trees and ternary sequences, for which we properly adapt and orchestrate the use of known compressed data structures.

Aldinucci, Marco and Campa, Sonia and Danelutto, Marco and Kilpatrick, Peter and Dazzi, Patrizio and Laforenza, Domenico and Tonellotto, Nicola
Behavioural skeletons for component autonomic management on grids
December 9, 2014
UnipiEprints view

We present behavioural skeletons for the CoreGrid Component Model, which are an abstraction aimed at simplifying the development of GCM-based self-management applications. Behavioural skeletons abstract component self-man-agent in component-based design as design patterns abstract class design in classic OO development. As here we just want to introduce the behavioural skeleton framework, emphasis is placed on general skeleton structure rather than on their autonomic management policies.

Aldinucci, Marco and Torquati, Massimo and Vanneschi, Marco and Alessandro, Gervaso and Zuccato, Pierfrancesco and cacitti, Manuel
VirtuaLinux Design Principles
December 9, 2014
UnipiEprints view

VirtuaLinux is a Linux meta-distribution that allows the creation, deployment and administration of virtualized clusters with no single point of failure. VirtuaLinux architecture supports disk-less configurations and provides an efficient, iSCSI based abstraction of the SAN. Clusters running VirtuaLinux exhibit no master node to boost resilience and flexibity.

Cappanera, Paola and Scutellà, Maria Grazia
Color-coding algorithms to the balanced path problem: computational issues
December 9, 2014
UnipiEprints view

Given a weighted directed network G, we consider the problem of computing k balanced paths from given source nodes to given destination nodes of G, i.e., k paths such that the difference in cost between the longest and the shortest path is minimized. Although not yet investigated by the OR scientific community, except for some preliminary theoretical results concerning the special case of acyclic networks, balanced path problems arise in several interesting applications, both in transportation and in telecommunication settings. For example, in load balancing of multiple Quality of Service (QoS) paths in the IP Telephony service, the problem of minimizing the end-to-end delay difference between the longest and the shortest path in multiple path management schemes has been suggested in the literature as a promising line of research. In this work the focus is on the computation of node-disjoint balanced paths in the general case, where the input graph G may have any structure. Starting from some algorithmic ideas proposed for acyclic networks, a general framework is firstly described, which is based on the color-coding method for computing simple paths. Then the general framework is specialized and a pool of algorithms is designed which includes both an exact approach as well as alternative heuristics. The algorithms have been tested on a large suite of instances generated from some benchmark telecommunication instances. The obtained computational results are very interesting: in some cases, the exact color-coding algorithm produces the optimal solution very rapidly; in the remaining cases, some of the proposed heuristics are able to generate high quality solutions in a very quick time.

Baldan, Paolo and Bracciali, Andrea and Bruni, Roberto
A Semantic Framework for Open Processes
December 9, 2014
UnipiEprints view

We propose a general methodology for analysing the behaviour of open systems modelled as "coordinators" , i.e., open terms of suitable process calculi. A coordinator is understood as a process with holes or place-holders where other coordinators and components (i.e., closed terms) can be plugged in, thus influencing its behaviour. The operational semantics of coordinators is given by means of a symbolic transition system, where states are coordinators and transitions are labelled by spatial/modal formulae expressing the potential interaction that plugged components may enable. Behavioural equivalences for coordinators, like strong and weak bisimilarities, can be straightforwardly defined over such a transition system. Differently from other approaches based on universal closures, i.e., where two coordinators are considered equivalent when all their closed instances are equivalent, our semantics preserves the openness of the system during its evolution, thus allowing dynamic instantiation to be accounted for in the semantics. To further support the adequacy of the construction, we show that our symbolic equivalences provide correct approximations of their universally closed counterparts, coinciding with them over closed components. For process calculi in suitable formats, we show how tractable symbolic semantics can be defined constructively using unification.

Bigi, Giancarlo and Frangioni, Antonio and Zhang, Qinghua
Outer Approximation Algorithms for Canonical Reverse-Polar Problems
December 9, 2014
UnipiEprints view

In this paper we propose a novel generalization of the canonical DC problem and we study the convergence of outer approximation (cutting planes) algorithms for its solution which use an “approximated” oracle for checking the global optimality conditions to the problem. Although the approximated optimality conditions are similar to those of the canonical DC problem, the new class of Canonical Reverse Polar (CRP) problems is shown to significantly differ from its special case. We also show that outer approximation approaches for DC problems need be substantially modified in order to cope with (CRP); interestingly, some outer approximation approaches for the latter cannot be applied to the formers, thus the more general problem allows for novel algorithms. We develop a hierarchy of conditions that guarantee the convergence of cutting plane algorithms;relying on these conditions, we build four cutting plane algorithms for solving (CRP), which seem to be new and cannot be reduced to each other.

Bacciu, Davide and Micheli, Alessio and Starita, Antonina
Feature-wise Competitive Repetition Suppression Learning for Gene Data Clustering and Feature Ranking
December 9, 2014
UnipiEprints view

The paper extends Competitive Repetition-suppression (CoRe) learning to deal with high dimensional data clustering. We show how CoRe can be applied to the automatic detection of the unknown cluster number and the simultaneous ranking of the features according to learned relevance factors. The effectiveness of the approach is tested on two freely available data sets from gene expression data and the results show that CoRe clustering is able to discover the true data partitioning in a completely unsupervised way, while it develops a feature ranking that is consistent with the state-of-the-art lists of gene relevance.

Aldinucci, Marco and Danelutto, Marco and Kilpatrick, Peter
Management in distributed systems: a semi-formal approach
December 9, 2014
UnipiEprints view

Formal tools can be used in a ''semi-formal'' way to support distributed program analysis and tuning. We show how ORC has been used to reverse engineer a skeleton based programming environment and to remove one of the skeleton system's recognized weak points. The semi-formal approach adopted allowed these steps to be performed in a programmer-friendly way.

Bigi, Giancarlo and Frangioni, Antonio and Zhang, Qinghua
Outer Approximation Algorithms for Canonical DC Problems
December 9, 2014
UnipiEprints view

The paper discusses a general framework for outer approximation type algorithms for the canonical DC optimization problem. A thorough analysis of properties which guarantee convergence is carried out: different sets of general conditions are proposed and compared. They are exploited to build six different algorithms, which include the first cutting plane algorithm proposed by Tuy but also new ones. Approximate optimality conditions are introduced to guarantee the termination of the algorithms and the relationships with the global optimal value are discussed.

Ciriani, Valentina and Cordone, Roberto
An Approximation Algorithm for Fully Testable kEP-SOP Networks
December 9, 2014
UnipiEprints view

Multi-level logic synthesis yields much more compact expressions of a given Boolean function with respect to standard two-level sum of products (SOP) forms. On the other hand, minimizing an expression with more than two-levels can take a large time. In this paper we introduce a novel algebraic four-level expression, named k-EXOR-projected sum of products (kEP-SOP) form,whose synthesis can be performed in polynomial time with an approximation algorithm starting from a minimal SOP.Our experiments show that the resulting networks can be obtained in very short computational time and often exhibit a high quality. We also study the testability of these networks under the Stuck-at-fault model, and show how fully testable circuits can be generated from them by adding at most a constant number of multiplexer gates. Experimental results show the effectiveness of this method both for four-level logic and general multi-level logic synthesis.

Bartoletti, Massimo and Degano, Pierpaolo and Ferrari, Gianluigi
Planning and Verifying Service Composition
December 9, 2014
UnipiEprints view

A static approach is proposed to study secure composition of services. We extend the lambda-calculus with primitives for selecting and invoking services that respect given security requirements. Security-critical code is enclosed in policy framings with a possibly nested, local scope. Policy framings enforce safety and liveness properties. The actual run-time behaviour of services is over-approximated by a type and effect system. Types are standard, and effects include the actions with possible security concerns - as well as information about which services may be invoked at run-time. An approximation is model-checked to verify policy framings within their scopes. This allows for removing any run-time execution monitor, and for determining the plans driving the selection of those services that match the security requirements on demand.

Colazzo, Dario and Sartiani, Carlo
Efficient Subtyping for Unordered XML Types
December 9, 2014
UnipiEprints view

While XML is an ordered data format, many applications outside the document processing area just drop ordering and manipulate XML data as they were unordered. In these contexts, hence, XML is essentially used as a way for representing unordered, unranked trees. The wide use of unordered XML data should be coupled with a careful and detailed analysis of their theoretical properties. One of the operations that is mostly affected by the presence of a global ordering relation is semantic subtype-checking, i.e., language inclusion. In an unordered context, inclusion has been proved to be inherently more complex than in the ordered case: in particular, subtype-checking for ordered single-type EDTDs is in PSPACE, while the same operation for single-type EDTDs with unordered types is in EXPSPACE (the same complexity result holds for unordered DTDs). Comparing two unordered XML types for inclusion, hence, is very expensive; as a consequence, it becomes very important to identify restrictions defining type classes for which inclusion is tractable or, at least, less complex. This paper identifies two large subclasses of unordered XML types for which inclusion can be computed by an EXPTIME and a PTIME algorithm, respectively. These classes are defined by restrictions on the use of element, repetition, and union types, and comprise many DTDs and XML Schemas used in practice.

Bevilacqua, Roberto and Bozzo, Enrico
The Sylvester-Kac matrix space
December 5, 2014
UnipiEprints view

The Sylvester-Kac matrix is a tridiagonal matrix with integer entries and integer eigenvalues that appears in a variety of applicative problems. We show that it belongs to a four dimensional linear space of tridiagonal matrices that can be simultaneously reduced to triangular form. We name this space after the matrix.

Frangioni, Antonio and d'Antonio, Giacomo
Deflected Conditional Approximate Subgradient Methods
December 4, 2014
UnipiEprints view

Subgradient methods for constrained nondifferentiable problems benefit from projection of the search direction onto the (normal cone of) the feasible set prior to computing the steplength, that is, from the use of conditional subgradient techniques. In general, subgradient methods also largely benefit from deflection, i.e., defining the search direction as a (convex) combination of the previous direction and the current subgradient. However, combining the two techniques is not straightforward, especially if an inexact oracle is available which can only compute approximate function values and subgradients. We present a convergence analysis of several different variants, both conceptual and implementable, of approximate conditional deflected subgradient methods. Our analysis extends the available results in the literature by using the main stepsize rules presented so far while allowing deflection in a more flexible way; to allow for (diminishing/square summable) rules where the stepsize is tightly controlled a-priori, we propose a new class of deflection-restricted approaches where it is the deflection parameter, rather than the stepsize, which is dynamically adjusted using the "target value" of the optimization sequence. For both Polyak-type and diminishing/square summable stepsizes, we propose a "correction" of the standard formula which shows that, in the inexact case, knowledge about the error computed by the oracle (which is available in several practical applications) can be exploited in order to strengthen the convergence properties of the method.



NOTE. Starting January 2015 Technical reports can be inserted in the Open Access repository UnipiEprints.
Once published, they will be visible also in these pages. The old TR service is no longer maintained.

Data imported from UnipiEprints