|
IMT Research Seminars are open to the public, i.e. professors, researchers, students and
everyone who may be interested in the topic.
Guest speakers can be leading international academics and professionals or young scholars
who come to present their work in progress.
Upcoming Seminars
No upcoming seminars to display
Past Seminars
From January 24, 2012, 11:30 To 12:15, San Micheletto − Classroom 6 On the use of control Lyapunov R-functions for nonlinear stabilization Control Lyapunov functions provide a fundamental tool to support control design when robustness, constraints fulfillment and optimality have to be simultaneous addressed in system stabilization. However, such general control problem is very challenging and almost impossible to be solved using a single control Lyapunov function.
The recent framework of R-functions allow the design of innovative control Lyapunov functions having smooth and non-homothetic level sets.
In particular, given a control Lyapunov function with a "large" domain of attraction and a second one guaranteeing local optimality, our merging procedure yields the controlled domain of attraction of the former and the local performance of the latter. -
Sergio Grammatico
PhD student, Università di Pisa
|
From January 18, 2012, 16:00 To 17:30, Ex Boccherini − Conference Room Modelchecking evolution on-the-fly The coordination modeling language Paradigm distinguishes fine-grained behaviour of transitions between states and coarse-grained behaviour of transfers between phases in component-based systems. The semantics guarantees vertical consistency of states and phases within a component. Protocols maintain horizontal consistency for collaborations of components. By adapting the protocols at run-time, system evolution can be arranged on-the-fly. We discuss for examples of a critical-section problem and a production line how dynamic system adaptation using the symbolic model checker mCRL2 can be verified -
Erik De Vink
Technische Universiteit Eindhoven
|
From December 20, 2011, 16:00 To 17:30, San Micheletto − Classroom 6 Modelling session types using contracts Session types and contracts are two formalisms used to study client-server interactions. In this talk we show the relationship between them. In particular, we will show a natural interpretation of session types into a subset of contracts. This interpretation can be used to define a fully abstract model for the relation of sub-typing on session types. -
Giovanni Bernardi
Trinity College Dublin
|
From December 7, 2011, 16:00 To 17:30, Ex Boccherini − Conference Room Feed-forward Neural Networks - Analysis of Iterative Learning Algorithms
|
From December 1, 2011, 16:00 To November 1, 2011, 17:30, Ex Boccherini − Conference Room Rule Formats for Determinism and Idempotence Operational semantics describes the behaviour of programs in a language in terms of their execution on an abstract machine, which is often represented as a, possibly infinite, state machine. Structural Operational Semantics is a rule-based and syntax-driven approach to giving operational semantics to programming and specification languages.
Determinism is a semantic property of (a fragment of) a language that specifies that a program cannot evolve operationally in several different ways. Idempotence is a property of binary language constructs requiring that the composition of two identical specifications or programs will result in a piece of specification or program that is equivalent to the original components. In this talk,
I will discuss two (related) meta-theorems for guaranteeing determinism and idempotence of binary operators. These meta-theorems are formulated in terms of syntactic templates for operational semantics, called rule formats. I will argue for the applicability of the proposed formats by applying them to various operational semantics from the literature.
The talk is based on joint work with Arnar Birgisson (Chalmers), Anna Ingolfsdottir (Reykjavik University), MohammadReza Mousavi (TU Eindhoven) and Michel A. Reniers (TU Eindhoven). A journal paper based on this work will appear in Science of Computer Programming (http://dx.doi.org/10.1016/j.scico.2010.04.002). -
Luca Aceto
ICE-TCS, School of Computer Science, Reykjavik University
|
From November 23, 2011, 11:30 To 13:00, Ex Boccherini − Conference Room Performance and productivity in the multi-core era: challenges in software engineering and formal methods FastFlow is a programming framework specifically targeting multi- and many-cores architetcures. It is implemented as a stack of C++ template libraries built on top of lock-free (and memory fence free) synchronization mechanisms. Its philosophy is to combine programmability with performance. In particular, FastFlow promotes
(lock-free) pattern-based programming by providing programmers with extendible high-level parallel constructs, which are implemented as parametric streaming networks. They are realized by decoupling synchronizations of parallel activities, which are implemented in a message-passing style, and data exchange, which can be realized in both message-passing and shared-memory style (by way of pointer passing). This makes it possible: 1) to implement the whole run-time support in a lock-free and memory fence-free fashion, which ensures the efficient orchestration of fine-grained parallel activities on cache-coherent architectures (down to ~10 ns core-to-core synchronization latency); and 2) to employ different programming models to enhance locality or fast data movement according to the patterns’ high-level semantics. FastFlow’s expressivity will be illustrated by way of existing applications, which span different areas and include extensions to the programming model itself.
Throughout the talk, the technological and methodological advances we advocate will be discussed in the perspective of challenges in formal methods to support performance and productivity in programming models we believe will characterize the multi-core era. More information at http://di.unito.it/fastflow -
Marco Aldinucci
Università di Torino
|
From November 16, 2011, 16:00 To 17:30, Ex Boccherini − Conference Room Multi-core and GPU model checking: Challenges and Outlooks Model checking is one of the most successful formal techniques for the verification of software and hardware systems. Developed in the beginning of the eighties, nowadays it is used by major companies, like Microsoft, to improve the quality of their products.
In my talk I focus on improvements of model checking algorithms by exploiting the recent developments in the processor technology. In particular, the emphasis is on parallel algorithms for shared memory architectures, like multi-core systems and general purpose graphic processing units (GPGPUs). These research directions are quite new - the first papers on multi-core and GPU model checking were published in the last four years. Therefore, there are still many untrodden avenues for cooperation of experts from different computer science communities. For example, one of the main open problems is how to design an efficient (shared memory) parallel algorithm for finding cycles in the state space graph. In the recent years we have been using successfully GPUs for accelerating probabilistic model checking. The implementations in the probabilistic model checker PRISM achieve speedups of more than one order of magnitude compared to their sequential counterparts. Our approach crucially hinges on efficient parallel algorithms for sparse matrix vector multiplication.
The above mentioned issues, like cycle detection and multiplication algorithms, are in principle independent on their applications in model checking and as such can be interesting for other computer science areas. -
Dragan Bosnacki
Eindhoven University of Technology
|
From November 10, 2011, 16:00 To 17:30, Ex Boccherini − Conference Room Numerical methods for conservative problems -
Luigi Brugnano
Università degli Studi di Firenze
|
From October 26, 2011, 16:00 To 17:30, Ex Boccherini − Conference Room Security in e-Health scenarios Important progresses in medicine and healthcare has been made during
the last century. The duration of the life of human beings is dramatically
increased. Population of the developed countries is aging, causing serious
problems in the health sector. In Europe it is expected that the number of
citizens aged over 65 will rise up to 123 millions in 2030. This fact will have
a huge impact on social, economic, and health aspects. On the other hand,
access to healthcare treatment is not always granted in developing countries
where healthcare and communications infrastructures are missing. Electronic
health (e-Health) can help to overcome these problems. The aim is to make it
possible for patients to maintain a mobile and independent lifestyle. The e-Health
has the possibility to bring electronic healthcare treatments to citizens and regions,
which otherwise would not have access to it, and improves their quality of life.
Initiatives like Integrating the Healthcare Enterprise (IHE) have been
developed for the definition of standard methodologies for secure and
interoperable EHR exchanges among clinics and hospitals. Using the requisites
specified by these initiatives, many large-scale projects have been set up to
enable healthcare professionals to handle patients' EHRs. Applications deployed
in these settings are often considered safety-critical, thus ensuring such security
properties as confidentiality, authentication, and authorization is crucial for
their success.
This seminar will introduce de-facto security standards for e-Health software
interoperability (OASIS, Hl7, IHE) in Service Oriented Architectures. Common
problems and security flaws found in real project specifications will be covered. -
Massimiliano Masi
Università degli Studi di Firenze & Tiani-Spirit GmbH
|
From October 20, 2011, 11:30 To 13:00, Ex Boccherini − Conference Room Controlling reversibility in rhopi In rhopi every step can always be undone, and each process freely
moves back and forward. To make rhopi usable to program recoverable
systems, the ability to go back has to be controlled. Many
possibilities in this direction exist. We analyze one such
possibility, namely the introduction in rhopi of an explicit rollback
primitive. The definition of a proper semantics for such a primitive
is a surprisingly delicate matter because of the potential
interferences between concurrent rollbacks. We define a high-level
operational semantics allowing to capture concurrent rollbacks. We
also define a lower-level distributed semantics, which is closer to an
actual implementation of the rollback primitive. The two semantics are
equivalent with respect to weak barbed congruence. -
Ivan Lanese
Alma Mater Studiorum - Università di Bologna
|
From October 12, 2011, 16:00 To 17:30, Ex Boccherini − Conference Room Towards Reversible Systems The notion of reversible computation is attracting increasing interest because of its applications in diverse fields, in particular the study of programming abstractions for reliable systems. In this paper, we continue the study undertaken by Danos and Krivine on reversible CCS by defining a reversible higher-order pi-calculus (HOpi). We prove that reversibility in our calculus is causally consistent and that one can encode faithfully reversible HOpi into a variant of HOpi. -
Claudio Antares Mezzina
INRIA Rhone Alpes
|
From October 6, 2011, 16:00 To 17:30, Ex Boccherini − Conference Room Learning from constraints In this talk, I propose a functional framework to understand the emergence of intelligence in agents exposed to examples and knowledge granules. The theory is based on the abstract notion of constraint, which provides a representation of knowledge granules gained from the interaction with the environment. I give a picture of the “agent body” in terms of representation theorems by extending the classic framework of kernel machines in such a way to incorporate logic formalisms, like first-order logic. This is made possible by the unification of continuous and discrete computational mechanisms in the same functional framework, so as any stimulus, like supervised examples and logic predicates, is translated into a constraint. The learning, which is based on constrained variational calculus, is either guided by a parsimonious match of the constraints or by unsupervised mechanisms expressed in terms of the minimization of the entropy.
I show some experiments with different kinds of symbolic and sub-symbolic constraints, and then I give insights on the adoption of the proposed framework in computer vision. It is shown that in most interesting tasks the learning from constraints naturally leads to “deep architectures”, that emerge when following the developmental principle of focusing attention on “easy constraints”, at each stage. Interestingly, this suggests that stage-based learning, as discussed in developmental psychology, might not be primarily the outcome of biology, but it could be instead the consequence of optimization principles and complexity issues that hold regardless of the “body.” -
Marco Gori
Università degli Studi di Siena
|
From October 5, 2011, 16:00 To 17:30, Ex Boccherini − Conference Room Localised access control policies and global reasoning In distributed systems, the traditional way of enforcing security is by means of access control security policies. We propose a framework and some analyses that can be done over it. The framework allows attaching security policies in the various locations of the system, following a realistic and practical fashion. As the runtime system involves interaction of locations, groups of policies may be relevant thereby needing a logic and consistent way of combining them. This leads to a complex system of networks and security policies that are only sometimes relevant. The resulting global system cannot then be trivially certified by static means. We propose a model checking that does not explore the entire state space but is inspired in static analysis techniques instead. Our aim is to have a formal framework with which it is possible to design distributed systems with adaptable and certifiable security. -
Alejandro Mario Hernandez
Danmarks Tekniske Universitet
|
From July 5, 2011, 18:00 To 19:30, San Micheletto − Classroom 6 The experience of art in urban space The experience of art in urban space represents a very special case in the area of the studies of reception.
In museums or galleries, reception of art often tries visitors' membership of the "worlds of art" (H. S. Becker, 1988). But the whole "apparatus" of museums and galleries (as a "system of relations" between material and non material, human and non human elements - Foucault, 1973) generally can help them in going beyond this "trial".
In urban space, this apparatus is lacking, most of the time... In such a context, the meeting with a work of art is like this "astounding complex" (or "negative experience") Goffman described in his Frame analysis (1986). After an overlook on theories of reception, and its process that involves memories and affects, we particularly will point out the role that plays the apparatus in giving its "form" to the experience of art, including in urban space. On this "system of relations" basically depend the true nature of things (what is a work of art ?... Or another kind of symbolic objects) and our subjective "response" (Freedberg, 1986) : cognitive and emotional as well. -
Pierre Le Queau
Université Pierre Mendès - Grenoble 2
|
From June 29, 2011, 12:00 To 13:30, Ex Boccherini − Conference Room Model Repair for Probabilistic Systems We introduce the problem of Model Repair for Probabilistic Systems as follows. Given a probabilistic system M and a probabilistic temporal logic formula φ such that M fails to satisfy φ, the Model Repair problem is to find an M that satisfies φ and differs from M only in the transition flows of those states in M that are deemed controllable. Moreover, the cost associated with modifying M’s transition flows to obtain M should be minimized. Using a new version of parametric probabilistic model checking, we show how the Model Repair problem can be reduced to a nonlinear optimization problem with a minimal-cost objective function, thereby yielding a solution technique. We demonstrate the practical utility of our approach by applying it to a number of significant case studies, including a DTMC reward model of the Zeroconf protocol for assigning IP addresses, and a CTMC model of the highly publicized Kaminsky DNS cache-poisoning attack. -
Ezio Bartocci
University of Stony Brook
|
From June 17, 2011, 15:00 To 16:30, Ex Boccherini − Conference Room Behavioural equivalence in higher-order calculi A language is "higher-order" if program code can be passed around, that is, terms of the language can be values. Developing a theory of behavioural equivalence in higher-order languages can be hard.
Particularly challenging can be: (1) the proof of congruence, (2) obtaining definitions and results that scale to languages with different features.
In the talk, I will discuss the problems that higher-order languages present, and some approaches to tackle these problems. I will start from the lambda-calculus --the best known higher-order language-- and then move to the higher-order pi-calculus. -
Davide Sangiorgi
Alma Mater Studiorum - Università di Bologna
|
From May 23, 2011, 17:10 To 18:00, Ex Boccherini − Conference Room The sensitivity of risk measures to estimation error -
Imre Kondor
Eötvös University, Budapest
|
From May 23, 2011, 16:00 To 16:50, Ex Boccherini − Conference Room Similarity based networks with application to stock portfolios and investor's trading behavior -
Fabrizio Lillo
Scuola Normale Superiore, Università di Palermo and Santa Fe Institute, USA
|
From May 17, 2011, 16:30 To 18:30, Ex Boccherini − Conference Room Algorithmic Game Theory, Computational Aspects of Nash Equilibria and Congestion Games -
Michele Flammini
Università degli Studi dell'Aquila
|
From May 4, 2011, 15:30 To 17:00, Ex Boccherini − Conference Room Cross Layer Networking for Wireless Networks -
Izhak Rubin
Electrical Engineering Department, UCLA
|
From April 27, 2011, 16:30 To 18:00, Ex Boccherini − Conference Room Run-time Adaptation of Service-Based Applications Service-based applications are considered a promising technology since they are able to offer complex and flexible functionalities in widely distributed environments by composing different types of services. These applications have to be adaptable to unforeseen changes in the functionality offered by component services and to their unavailability or decreasing performances. Furthermore,
when applications are made available to a high number of potential users, they should also be able to dynamically adapt to the current context of use as well as to specific requirements and needs of the specific users. In order to address these issues, mechanisms that enable adaptation should be introduced in the life-cycle of applications, both in the design and in the runtime phases.
The seminar is organized in three parts. In the first part the speaker will present design principles and guidelines that are suitable to enable adaptation, discussing their effectiveness of the proposed methodology by means of real-world scenarios over various types of service-based applications. In the second Bucchiarone will present a formal framework designed and implemented with the goal to adapt the execution of service-based business processes at runtime in case of context changes. He will conclude with a demo to show all concepts behind adaptation of service-based applications. -
Antonio Bucchiarone
Bruno Kessler Foundation
|
From April 20, 2011, 17:15 To 18:30, Ex Boccherini − Conference Room Lessons from the philosophy of science to data mining and vice versa -
Abraham Meidan
Wizsoft Inc.
|
From April 13, 2011, 17:30 To 19:00, San Micheletto − Classroom 6 Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Concurrent Processes A Markovian bisimulation equivalence has been defined for sequential processes, which is weak in the sense that it reduces certain sequences of exponentially timed internal actions to single exponentially timed internal actions having the same average duration and execution probability as the corresponding sequences.
This weak Markovian bisimulation equivalence is a congruence for sequential processes with abstraction and turns out to induce an exact CTMC-level aggregation at steady state for all the processes. Unfortunately, it is not a congruence with respect to parallel composition. In this talk, we show how to extend it to concurrent processes in a way that a reasonable tradeoff among abstraction, compositionality, and exactness is achieved. In particular, by enhancing the abstraction capability when dealing with concurrent computations, it is possible to retrieve the congruence property with respect to parallel composition, with the resulting CTMC-level aggregation being exact at steady state for a certain class of concurrent processes.
-
Marco Bernardo
Università degli Studi di Urbino "Carlo Bo"
|
From April 13, 2011, 15:30 To 17:30, Ex Boccherini − Conference Room Understanding Cultural Objects as Objects In this seminar we focus on material culture, specifically how the physical properties of objects convey or inhibit our understanding of their social meaning -
Wendy Griswold
Northwestern University
|
From April 11, 2011, 11:00 To 13:00, Ex Boccherini − Conference Room Understanding Cultural Objects as Culture In this seminar we explore the links between social structure and culture by looking at the interplay among the social world, creators, audiences, and culture -
Wendy Griswold
Northwestern University
|
From April 8, 2011, 14:00 To 15:30, Ex Boccherini − Conference Room The Network of Countries and their Products: an analysis of the Wealth of Nations -
Luciano Pietronero
Director of the Institute of Complex Systems, CNR and Professor of Condensed Matter Physics, University of Rome "La Sapienza"
|
From April 6, 2011, 17:30 To 19:00, San Micheletto − Classroom 6 Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Sequential Processes The Markovian behavioral equivalences defined so far treat exponentially timed internal actions like any other action. Since an exponentially timed internal action has a nonzero duration, it can be observed whenever it is executed between a pair of exponentially timed noninternal actions. However, no difference may be noted between a sequence of exponentially timed internal actions and a single exponentially timed internal action as long as their average durations coincide. We show that Milner's construction to derive a weak bisimulation congruence for nondeterministic processes can be extended to sequential Markovian processes in a way that captures the above situation. We then prove that the resulting weak Markovian bisimulation congruence admits a sound and complete axiomatization, induces an exact CTMC-level aggregation at steady state, and is decidable in polynomial time for finite-state processes having no cycles of exponentially timed internal actions. -
Marco Bernardo
Università degli Studi di Urbino "Carlo Bo"
|
From March 22, 2011, 14:00 To February 22, 2011, 16:00, Ex Boccherini − Conference Room DESIGN FOR CULTURAL HERITAGE EXPERIENCES AND INTERPRETATIONS - A roadmap for the definition of the vision of the C3 unit The main objective of this seminar is to outline a roadmap for the definition of the vision of the Culture, Communication and Computing unit and discuss it with the students of the Management and Development of Cultural Heritage phd program. The C3 unit, Culture, Communication & Computing at the IMT Lucca aims at conducting innovative research and designing technologies and applications to explore new paradigms related to cultural heritage, to rethink how innovative technologies can improve users’ activities & experiences, and generate new concepts to enrich the user experience in the context of cultural heritage. During the seminar, a critical review of several case studies related to the intersection between interactive technologies and cultural heritage will be provided. The main assets of the C3 vision will be identified as well as long-term research objectives. Furthermore, the Locast Tourism - Lucca project will be introduced as the first concrete step of the unit. -
Leonardo Giusti
IMT Institute for Advanced Studies
|
From March 9, 2011, 17:00 To 18:30, Ex Boccherini − Conference Room Large-scale Performance Models with Stochastic Process Algebras This talk gives an overview of recent research concerning the use of stochastic process algebras for the quantitative evaluation of computer systems. The talk consists of three parts. The first part will introduce some basic notions on the usual discrete-state semantics in terms of continuous-time Markov chains. The second part will focus on the stochastic process algebra PEPA and discuss its fluid interpretation, a deterministic approximation with ordinary differential equations for the analysis of large-scale models. Finally, the third part will discuss how to compute typical measures of performance such as utilisation, throughput, and average response times from fluid models. Backed by theoretical results of asymptotic convergence, extensive numerical assays will show good accuracy of this approach for all practical purposes. -
Mirco Tribastone
Ludwig Maximilians Universität München
|
From January 20, 2011, 15:00 To 16:30, Ex Boccherini − Conference Room The Social Computer: a FET Flagship initiative for the new generation Internet -
Fausto Giunchiglia
Università degli Studi di Trento
|
From November 19, 2010, 12:30 To 13:30, Sala dei Servi, Complesso di San Micheletto Research Evaluation Tools -
Patrizia Ciucci
Università di Pisa and IMT Istitute for Advanced Studies, Lucca
|
From October 20, 2010, 15:00 To 16:30, Ex Boccherini − Conference Room DEZENT: A Completely Distributed Power Management and Distribution System for Renewable Energy Over the past few years, renewable energy (from sun, wind, or water power) has rapidly advanced as a economical and ecological factor, within the European Union and even world-wide. The production facilities (e.g. solar panels, wind or water power turbines) are typically widely distributed and are in the low-to-medium power range. While the traditional power distribution structure is organized in a top-down manner this is inadequate and more than inefficient for renewable energy. In the seminar the DEZENT will be presented where power management, distribution, and “market” negotiations are handled through bottom-up control.
In order to cope with the high amount of unpredictability of the regenerative sources we manage to do the whole business of negotiating, power distribution, grid stability checking and/or redistributing power flows within intervals (periods) of 0,5 sec, independent of the number of customers involved. (Keeping this rather tight deadline allows to assume that the negotiation situation, i.e. for demand and supply, is constant in the meantime.) The customer agents frequently adapt their strategies through distributed collaborative learning procedures (tailored Reinforcement Learning). Reserve energy needed for peak demand situations can be kept to a minimum because smart meters – as part of smart consumer facilities - would be utilized to dynamically make use of “conditional” consumers whereas in peak supply situations excessive power would be fed into large stationary batteries or grid-connected e-vehicles.
The emphasis of the talk will be on the technical context. Also steps into the future will be indicated. -
Horst Friedrich Wedde
Technische Universität Dortmund
|
From October 6, 2010, 15:00 To 16:30, Ex Boccherini − Conference Room Managing Adaptation and Evolution in Service Oriented Applications The service oriented computing (SOC) paradigm enables software application developers and service providers to dynamically grow application portfolios by seamlessly integrating services, information, and processes over the networks. One of the most relevant capabilities that this paradigm should provide is the ability of applications and services to adapt themselves and to evolve in reaction to unexpected changes of, e.g., technology, regulations, requirements, usage contexts, market opportunities. In the seminar, we will present a framework that we are developing in Trento, which supports the adaptation and evolution of service oriented applications developed according to the SOC paradigm. In particular, we will introduce the formal definition of adaptation and evolution adopted by the framework; then we will discuss the capabilities offered by the framework and the open problems in this context. -
Marco Pistore
Fondazione Bruno Kessler
|
From September 23, 2010, 15:00 To 16:30, Ex Boccherini − Conference Room Planning for the Future Internet of Services A lot of work has been done so far in the field of planning for web or software services. In this work, major tasks can be described in a planning framework: modeling of software services leads to a planning domain, their automated composition can be done by plan generation, their monitoring becomes monitoring of plan executions, and adaptation can done by re-planning.
Things change radically when we move to the framework envisioned by Future Internet. One of the major promises of the vision of Future Internet is the so called "Internet of Services", where applications "live" in the network and are available to end users as "real services" are available today to consumers in everyday life. According to this vision, software services are just software components that provide electronic access to "real services" (e.g., a software service for travel booking allows us to access the actual service behind it, namely "the possibility of traveling"). "Real services" are however very different from the corresponding software services, since they differ in their main characteristics, such as their duration, their accessibility, their constraints and conflicts, and their connection with the real world, which makes them highly dynamic. This new vision requires a shift in the research approach, as well as in the corresponding planning framework: Modeling should describe how the use of real services affects their consumers; Composition does not consist anymore in the generation of a new composed service, it becomes a task that finds relations among services based on emergent needs, constraints, opportunities of the consumers; Monitoring should not check software executions but rather focus on properties of the physical environment where the real services operate; Adaptation should move from reaction to changes in software services to reaction to changes in real services, in the physical environment where they operate, and to users' behaviors.
In this talk, I will first describe an approach to planning for software services, and I will then discuss some new research challenges for the future internet of services and how they are related to planning. -
Paolo Traverso
FBK, Center for Information Technology - IRST
|
From June 30, 2010, 17:00 To 18:30, San Micheletto − Classroom 6 Computing probabilities over DBM domains to integrate qualitative verification and quantitative evaluation of timed stochastic models In the development of reactive systems with nondeterministic densely-valued temporal parameters, qualitative
verification and quantitative evaluation play complementary roles, supporting the identification of feasible
behaviors and their association with a measure of probability. Though inherently coupled in the application
perspective, the two aspects yield contrasting needs that resulted in separate formalisms and techniques
developed upon different theoretical grounds.
We report the results of our research towards a unified approach of the two aspects based on the method of
stochastic state classes, which extends state space analysis based on Difference Bounds Matrix zones (DBM)
with the symbolic calculus of a density-function providing a measure for the probability of individual
states. To this end, we extend Time Petri Nets by associating a general probability distribution to the
static firing interval of each nondeterministic transition, and we explain how this stochastic information
induces a probability distribution for the states contained within a DBM class and how this probability
evolves in the enumeration of the reachability relation among classes. In particular, we show that the
state-density function accepts a continuous piecewise representation over a partition in DBM-shaped
subdomains, we develop a closed-form symbolic calculus of state-density functions under the assumption that
transitions in the sTPN model have expolynomial distributions over possibly bounded intervals, and we provide
an efficient approximation approach based on Bernstein Polynomials.
%
This enables the construction of a stochastic transition system that supports correctness verification based
on the theory of TPNs, provides a measure of probability for each feasible run, enables steady-state analysis
based on Markov Renewal Theory. -
Enrico Vicario
Università degli Studi di Firenze
|
From June 25, 2010, 10:00 To 11:30, Ex Boccherini − Conference Room Probabilistic automata and verification Christel Baier, Technische Universitaet Dresden Automata-based model checking relies on a representation of the system and the properties to be verified by finite-state automata. In the classical setting, nondeterministic automata are used for both the system and the properties, and verification amounts analyzing the product of these two nondeterministic automata by means of graph algorithms. In this talk, we address the automata-based approach for verifying randomized systems modeled by some kind of probabilistic automata. Technical problems in the definition of the product arise when dealing with nondeterministic automata for the property to be verified.
One solution is to switch to deterministic automata for the requirements, but this can cause a double exponential blow-up for the construction of an automata for a given logical formula (e.g., LTL) formalizing the requirements. An alternative obvious idea is the use of a probabilistic automata representing the properties. This, however, leads to the undecidability of the verification problem. Nevertheless there are some special instances of the verification problem that can be solved algorithmically in an elegant way using probabilistic automata for both the system and the property.
-
Christel Baier
Technische Universität Dresden
|
From June 24, 2010, 09:30 To 11:00, San Micheletto − Classroom 6 Formal Methods for Wireless Systems -
Massimo Merro
Università degli Studi di Verona
|
From June 18, 2010, 14:00 To 15:30, San Micheletto − Classroom 3 Weighted Bisimilarity in Linear (Co)Algebraic Form Weighted automata are used to describe quantitative properties in various areas such as probabilistic systems, image compression and speech-to-text processing.
The abstract behaviour of these automata is usually expressed in terms of weighted languages (also called formal power series), i.e., functions assigning to each word (in some alphabet) a weight (in some semiring).
Another abstract behaviour can be expressed in terms of weighted bisimilarity that, differently from the weighted-language semantics, takes into account the full branching structure.
In this talk, we show that (weighted) language semantics naturally arises from "linear coalgebras" on "vector spaces", while bisimilarity arises from "coalgebras" on "sets".
These observations are also crucial for defining some algorithms for computing these semantics.
-
Filippo Bonchi
LIX, Ecole Polytechnique
|
From June 17, 2010, 10:00 To 11:30, Ex Boccherini − Conference Room Algorithmic modeling of complex systems The convergence between computer science and biology occurred in successive waves, involving deeper and deeper concepts of computing. The current situation makes computer science a suitable candidate for becoming a philosophical foundation for systems biology with the same importance as mathematics, chemistry and physics. However, this significant opportunity is not a free lunch. New developments and a strong integration of different fields of computing are needed to face the challenges of systems biology. One of these developments is that of a complex and expanding applicative domain that can open entirely new avenues of research in computing and eventually help it become a natural, quantitative science. The main characteristic of highly parallelism and interaction-driven dynamics of biological systems make the conceptual and software framework developed for biological systems amenable to model, simulate and analyse any complex system whose evolution is determined by the interaction of its sub-components.
Therefore, economics, ecology, sociology and computing systems themselves are suitable applicative domains. More info in "Algorithmic Systems Biology", Communications of the ACM, 52(5):80-88, May 2009.
-
Corrado Priami
COSBI - The Microsoft Research - University of Trento Research center for Computational and Systems Biology
|
From June 9, 2010, 17:00 To 19:00, San Micheletto − Classroom 6 The European Institute of Innovation and Technology (EIT) - A new model of innovation, research and higher education The linkage between research, innovation and education (the so called knowledge dimensions) is gaining momentum in the European social and economic landscape. Most of European challenges and related opportunities are heavily affected by our capability to consolidate new models where the three dimensions of knowledge can fertilise each other in the framework of a sustainable economy. The talk is offering some reflection on these subjects by elaborating on the preliminary actions carried out by the European Institute of Innovation and Technology -
Giovanni Colombo
Istituto Superiore Mario Boella
|
February 19, 2010, 14:00, Ex Boccherini − Conference Room Learning, categorization and isomorphism in problem solving -
Massimo Egidi
Rettore, Università LUISS Guido Carli, Roma
|
From January 27, 2010, 17:00 To 18:30, San Micheletto − Classroom 6 Sessions and Session Types Sessions are a common and widespread mechanism of interaction in distributed architectures. The processes willing to interact establish a connection on a shared public channel. In this connection they agree on some private channel on which to have a conversation, dubbed session.
The conversation follows a given protocol which describes the kind and
order of the messages exchanged on the private channel. The messages
exchanged during a session may be synchronisation signals, basic values (e.g., integers, booleans, strings), names of public channels (those used to start sessions), or even names of private channels of already started sessions. In the last case one speaks of delegation since by sending to some other process the private channel of a session, the process delegates the receiver to continue that session.
Session types describe the sequences of messages exchanged on a private session channel and their possible branching based on labels: they prevent communication mismatches and session deadlocks.
The aim of this talk is to give an overview of sessions/session types and some hints on new proposals for incorporating secure information flow requirements within session types. -
Mariangiola Dezani
Università degli Studi di Torino
-
Mario Coppo
Università degli Studi di Torino
|
From December 9, 2009, 17:00 To 18:30, San Micheletto − Classroom 6 Wireless Vehicular Ad Hoc Networks: a survey on network protocols research solutions and open issues Wireless Vehicular Ad Hoc Networks (VANETs) have received an explosive attention under a research viewpoint in recent years, and a number of research groups worldwide are making efforts to explore the potential of vehicular communication as the enabling factor for a novel set of pervasive services and applications. This is also testified by the high number of recent and ongoing EU and US research projects in this field.
This survey illustrates a quick tour on the most challenging issues that have been considered in recent researches, and on some open problems that would need additional efforts and research solutions.
Specifically, this survey will focus on the MAC and Network protocol layers, by introducing the specific assumptions, limitations and potential of the VANET scenarios, and by exploring the most significant milestones so far achieved under a protocol design and optimization viewpoint. These guidelines are based on the overall evaluation of recent research results, projects, standards and directions for exploitation of the VANET potential under a service level viewpoint. -
Luciano Bononi
Università di Bologna
|
From December 2, 2009, 17:00 To 18:30, San Micheletto − Classroom 6 Avoiding correlation exceptions In service oriented computing, different instances of the same service may be available at a particular moment. Usually, a particular client is aimed at interacting with just one specific instance at a time.
Consequently, clients need to be able to identify service instances.
Correlation sets are a programming primitive that allows instance identification in orchestration languages.
A correlation set is a set of properties (i.e., values carried on by
messages) that are used to associate each received message with ``a unique'' process instance: every time a service receives a message, it inspects its content and determines a unique service instance that should handle the received message. If this is not possible (no instance or several instances are candidate), then the service raises an exception. In this talk we will present a formal model for correlation sets that accounts also for correlation exceptions. We also characterise a class of correlation exceptions, called avoidable, that can be prevented during service design. We also propose a type system that guarantees that orchestrators are free from avoidable exceptions. -
Hernan Claudio Melgratti
Universidad de Buenos Aires
|
From November 25, 2009, 17:00 To 18:30, San Micheletto − Classroom 6 Energy Efficient Wireless Internet Access In this talk we discuss the energy savings that can be obtained with the energy-aware cooperative management of the cellular access networks of the operators that offer service over the same area.
We show that a huge amount of energy can be saved by using all networks in high traffic conditions, but progressively switching off networks during the periods when traffic decreases, and eventually becomes so low that the desired quality of service can be obtained with just one network.
When a network is switched off, its customers are allowed to roam over those that remain powered on.
Several alternatives are studied, as regards the traffic profile, the switch-off pattern, the energy cost model, and the roaming policy. -
Marco Ajmone Marsan
Politecnico di Torino
|
From November 18, 2009, 17:00 To 18:30, San Micheletto − Classroom 6 Rate-based Transition Systems for Stochastic Process Calculi A variant of Rate Transition Systems (RTS) is introduced and used as the basic model for defining stochastic behaviour of processes and for associating Continuous Time Markov Chains to process terms. The transition relation used in our variant associates to each process, for each action, the set of possible futures paired with a measure indicating their rates.We show how RTS can be used for providing the operational semantics of stochastic extensions of classical formalisms, namely CSP and CCS. We also show that our semantics for stochastic CCS guarantees associativity of parallel composition. Similarly, in contrast with the original definition by Priami, we argue that a similar approach for defining the semantics of stochastic pi-calculus guarantees associativity of parallel composition.
-
Rocco De Nicola
IMT Institute for Advanced Studies, Lucca
|
From November 11, 2009, 17:00 To 18:30, San Micheletto − Classroom 6 Run-time models for dynamic resource management in distributed systems The success of Web related technologies is leading to the implementation of large networked systems that support heterogeneous, possibly critical, services. Dynamic capacity management of these services would increase efficiency and business productivity, but similar processes are difficult to be implemented in contexts characterized by extreme variability of workloads and resource states to the extent that it is difficult to identify stationary periods.
We propose an innovative multi-phase methodology that is based on stochastic representations of the resource measures and on accurate models for positioning the present and future state of the system resources with respect to their capacities. These models represent the basis of several runtime decision algorithms that are oriented to load balancing, access control, anomaly detection, energy saving. This research area is characterized by various open issues that will be outlined at the end of the talk. -
Michele Colajanni
Università di Modena e Reggio Emilia
|
From November 4, 2009, 17:00 To 18:30, San Micheletto − Classroom 6 A Constraint-based Model of QoS Negotiations in Service Composition -
Maria Grazia Buscemi
IMT Institute for Advanced Studies, Lucca
|
From October 28, 2009, 17:00 To 18:30, San Micheletto − Classroom 6 Network Calculus: a worst-case theory for QoS guarantees in packet networks -
Giovanni Stea
Università di Pisa
|
From October 21, 2009, 17:00 To 18:30, San Micheletto − Classroom 6 A theory of design-by-contract for distributed multiparty interactions Abstract Reliability is a critical issue in multi-organizational, distributed applications. Design by Contract traditionally addresses reliability by elaborating type signatures for sequential programs centring on asymmetric procedural invocations. This talk will present a generalisation of the Design by Contract paradigm to multiparty distributed applications each using one or more complex, and possibly long-running, application-level protocols. The main contribution is an assertion method for distributed multiparty interactions centring on the notion of global assertion, which specifies constraints on a whole interaction scenario by elaborating multiparty session types.
-
Emilio Tuosto
University of Leicester
|
From October 7, 2009, 17:00 To 19:00, San Micheletto − Classroom 6 Automatic Termination analysis of Loops -
Zohar Manna
Stanford University
|
PACo - Performability-Aware Computing: Logics, Models, and Languages -
Angelo Troina
-
Simona Bernardi
-
Simona Bernardi
-
Marco Bernardo
-
Marco Bernardo
-
Alessandro Aldini
-
Liliana D'Errico
-
Diego Latella
-
Michele Loreti
-
Catia Trubiani
-
Vittorio Cortellessa
-
Maria Rita Di Berardini
-
Federico Buti
-
Luca Tesei
|
June 17, 2009 Programming and Reasoning on Global Computers with Evolving Topologies -
Rocco De Nicola
Università degli Studi di Firenze
|
|
|
Opportunistic and Delay Tolerant Networks
|
May 13, 2009 Probabilistic CEGAR
|
May 6, 2009 Model Checking for Nominal Calculi -
Ugo Giovanni Erasmo Montanari
Università di Pisa
|
March 20, 2009 Dynamics on complex networks -
Romualdo Pastor Satorras
Universitat Politècnica de Catalunya
|
November 10, 2008 Technological Change and the Wealth of Nations
|
October 17, 2008 The Internet is Flat: a Brief History of Networking in the Next Ten Years -
Donald Towsley
University of Massachusetts at Amherst
|
September 17, 2008 Core Calculi for Service Oriented Computing - Workshop
|
June 20, 2008 Muse: Multiparty sessions in SOC -
Hernan Claudio Melgratti
University of Buenos Aires
|
May 24, 2007 Symbolic Applied Pi-calculus
|
January 16, 2007 Lightweight Model Driven Development of data-intensive Web Applications
|
June 13, 2006 On the Exploitation of User Aggregation Strategies in Heterogeneous Wireless Networks -
Leonardo Badia
Research fellow IMT Lucca Institute for Advanced Studies
|
May 31, 2006 Repetita Iuvant? Constructive and destructive effects of redundancy and repetition in art, biology and computer science -
Davide Bacciu
IMT Institute for Advanced Studies, Lucca
|
May 30, 2006 The Million Minds Approach: From Reading to On-line Knowledge Discovery -
Barend Mons
University Medical Centre Rotterdam Leiden University Medical Centre, The Netherlands
|
May 23, 2006 Routing and channel assignment in multihop wireless mesh networks with multiple radios -
Habiba Skalli
IMT Institute for Advanced Studies, Lucca
|
May 11, 2006 Automatic email classification: an application-oriented review -
Alessio Botta
IMT Institute for Advanced Studies, Lucca
|
May 6, 2006 Signal Calculus: a process calculus for event notification based coordination -
Roberto Guanciale
IMT Institute for Advanced Studies, Lucca
|
March 28, 2006 Transactional composition of Services -
Hernan Claudio Melgratti
IMT Institute for Advanced Studies, Lucca
|
Issues in Processing Large Data Sets
|
November 18, 2005 L'allocazione delle risorse radio nei sistemi cdma cellular networks and wireless lans -
Leonardo Badia
Università degli Studi di Ferrara
|
If you are interested in getting informed about computer science and applications research seminars or other IMT activities or opportunities, you can fill out our form " Join IMT!"
|
|