Ph.D. Theses of 2007

• Flavio Baronti, Hypothesis Testing with Classifier Systems
  
  Abstract. This thesis presents a new ML algorithm, HCS, taking inspiration from Learning Classifier Systems, Decision Trees and Statistical Hypothesis Testing, aimed at providing clearly understandable models of medical datasets. Analysis of medical datasets has some specific requirements not always fulfilled by standard Machine Learning methods. In particular, heterogeneous and missing data must be tolerated, the results should be easily interpretable. Moreover, often the combination of two or more attributes leads to non-linear effects not detectable for each attribute on its own. Although it has been designed specifically for medical datasets, HCS can be applied to a broad range of data types, making it suitable for many domains. We describe the details of the algorithm, and test its effectiveness on five real-world datasets.
  [pdf]
  
  
• Yan He, Integrating LEO Satellite Constellations into Internet Backbone
  
  Abstract. Low Earth Orbit (LEO) satellite constellations have been used for ubiquitous and flexible Internet access services. However, a number of problems related to the integration of terrestrial with satellite hosts should be resolved for the effective exploitation of LEO constellations. LEO constellations are different from terrestrial Internet because of its special properties, which result in a lot of problems. A key issue is how to route Internet packets to the LEO constellation. In the thesis (1) the background of LEO constellations was introduced; (2) the obstacles of routing between the satellites and Internet were outlined; (3) The particular problem, which must be solved, is the routing burst stream traffic in LEO satellite constellations. Two novel routing algorithmsControl Route Transmission (CRT) and CRT with bandwidth allocation (BCRT)were utilized to address the bursts routing problem. CRT is an adaptive protocol which is able to minimize the congestion in the constellations. BCRT is a CRT extension which is allowed to class the traffic (e.g. video) with different QoS requirements and guarantees. Both of CRT and BCRT work in time epochs. Routes are computed on the basis of a directed weighted graph representing the global traffic traveling in the constellations. Both CRT and BCRT were evaluated via simulation and compared with other proposals in the literatures. The results showed that CRT is a simple algorithm, but the strategy produced by CRT could avoid the congestion and enhance the global resource usage in different traffic conditions. Moreover, the explicit reservation and reroute of BCRT greatly improve the performance of CRT. In particular, the dropping rate of BCRT is very low and the average delivery time is comparable with other proposals in the literatures.
  [pdf]
  
  
• Paolo Milazzo, Qualitative and Quantitative Formal Modeling of Biological Systems
  
  Abstract. Cell Biology, the study of the morphological and functional organization of cells, is now an established field in biochemical research. Computer Science can help the research in Cell Biology in several ways. For instance, it can provide biologists with models and formalisms able to describe and analyze complex systems such as cells. In the last few years many formalisms, originally developed by computer scientists to model systems of interacting components, have been applied to Biology. Among these, there are Petri Nets, Hybrid Systems, and the pi-calculus. Moreover, formalisms such as P Systems, originally developed to study new computational paradigms inspired by Biology, have recently found application to the description of biological phenomena. Finally, some new formalisms have been proposed to describe biomolecular and membrane interactions.
  The first advantage of using formal models to describe biological systems is that they avoid ambiguities. In fact, ambiguity is often a problem of the notations used by biologists. Moreover, the formal modeling of biological systems allows the development of simulators, which can be used to understand how the described system behaves in normal conditions, and how it reacts to changes in the environment and to alterations of some of its components. Furthermore, formal models allow the verification of properties of the described systems, by means of tools (such as model checkers) which are well established and widely used in other application fields of Computer Science, but unknown to biologists. In this thesis we develop a formalism for the description of biological systems, called Calculus of Looping Sequences (CLS), based on term rewriting and including some typical features of process calculi for concurrency. What we want to achieve is a formalism that allows describing proteins, DNA fragments, membranes and other macromolecules, without ignoring the physical structure of these elements, and by keeping the syntax and the semantics of the formalism as simple as possible.
  CLS terms are constructed from an alphabet of basic symbols (representing simple molecules) and include operators for the creation of sequences (representing proteins and DNA fragments), of closed sequences which may contain something (representing membranes), and of multisets of all these elements (representing juxtaposition). A CLS term describes the structure of the system under study, and its evolution is given by the application of rewrite rules describing the events that may occur in the system, and how the system changes after the occurrence of one of these events. We equip CLS with an operational semantics describing the possible evolutions of the system by means of application of given rewrite rules, and we show that other formalisms for the description of membranes can be encoded into CLS in a sound and complete way.
  We propose bisimilarity as a tool to verify properties of the described systems. Bisimilarity is widely accepted as the finest extensional behavioral equivalence one may want to impose on systems. It may be used to verify a property of a system by assessing the bisimilarity of the considered system with a system one knows to enjoy that property. To define bisimilarity of systems, these must have semantics based on labeled transition relations capturing potential external interactions between systems and their environment. A labeled transition semantics for CLS is derived from rewrite rules by using as labels contexts that would allow rules to be applied. We define bisimulation relations upon this semantics, and we show them to be congruences with respect to the operators on terms. In order to model quantitative aspects of biological systems, such as the the frequency of a biological event, we develop a stochastic extension of CLS, called Stochastic CLS. Rates are associated with rewrite rules in order to model the speeds of the described activities. Therefore, transitions derived in Stochastic CLS are driven by exponential distributions, whose rates are obtained from the rates of the applied rewrite rules and characterize the stochastic behavior of the transitions. The choice of the next rule to be applied and of the time of its application is based on the classical Gillespie’s algorithm for simulation of chemical reactions.
  Stochastic CLS can be used as a formal foundation for a stochastic simulator, but also to build models to be given as an input to model checking tools. In fact, the transition system obtained by the semantics of Stochastic CLS can be easily transformed into a Continuous Time Markov Chain (CTMC). If the set of states of the CTMC is finite (namely, if the set of reachable CLS terms is finite) a standard probabilistic model checker (such as PRISM) can be used to verify properties of the described system. Finally, we propose a translation of Kohn Molecular Interaction Maps (MIMs), a compact graphical notation for biomolecular systems, into Stochastic CLS. By means of our translation, a simulator of systems described with Stochastic CLS can be used to simulate also systems described by using MIMs.
  [pdf]
  
  
• Razvan Andrei Popescu, Aggregation and Adaptation of Web Services
  
  Abstract. Service-oriented computing highly supports the development of future business applications through the use of (Web) services. Two main challenges for Web services are the aggregation of services into new (complex) business applications, and the adaptation of services presenting various types of interaction mismatches.
  The ultimate objective of this thesis is to define a methodology for the semiautomated aggregation and adaptation of Web services capable of suitably overcoming semantic and behaviour mismatches in view of business process integration within and across organisational boundaries.
  We tackle the aggregation and adaptation of services described by service contracts, which consist of signature (WSDL), ontology information (OWL), and behaviour specification (YAWL). We first describe an aggregation technique that automatically generates contracts of composite services satisfying (behavioural) client requests from a registry of service contracts. Further on, we present a behaviouraware adaptation technique that supports the customisation of services to fulfil client requests. The adaptation technique can be used to adapt the behaviour of services to satisfy both functional and behavioural requests.
  In order to support the generation of service contracts from real-world service descriptions, we also introduce a pattern-based compositional translator for the automated generation of YAWL workflows from BPEL business processes. In this way, we pave the way for the formal analysis, aggregation, and adaptation of BPEL processes.
  [pdf]