logo ISTI

Istituto di Scienza e Tecnologie
dell’Informazione “A. Faedo”

an Institute of the National Research Council of Italy CNR

Probabilistic PCTL*: The deductive way

03 October 2016, 10:00 - Location: C-29

Luis Ferrer Fioriti (Dependable Systems and Software group, Saarland University, Saarbreucken, Germany)
Mieke Massink

Complex probabilistic temporal behaviours need to be guaranteed in robotics and various other control domains, as well as in the context of families of randomized protocols. At its core, this entails checking infinite-state probabilistic systems with respect to quantitative properties specified in probabilistic temporal logics. Model checking methods are not directly applicable to infinite-state systems, and techniques for infinite-state probabilistic systems are limited in terms of the specifications they can handle.

We present a deductive approach to the verification of countable-state systems against properties specified in probabilistic CTL*, on models featuring both nondeterministic and probabilistic choices. The deductive proof system we propose lifts the classical proof system by Kesten and Pnueli to the probabilistic setting. However, the soundness arguments are completely distinct and go via the theory of martingales. Completeness results for the weakly finite case illustrate the theoretical effectiveness of our approach.

This is joint work with Rayna Dimitrova, Holger Hermanns and Rupak Majumdar.

Mozart's Laptop: Implications for Creativity in Multimedia Digital Libraries and Beyond

03 October 2016, 15:00 - Location: C-29

David Bainbridge (Professor of Computer Science at the University of Waikato - New Zealand )
Vittore Casarosa

If Mozart were alive today, what sorts of musical apps would such an innovative composer use on his laptop? In this seminar I will attempt to answer - at least in part - this question. We will metaphorically drop in on Wolfgang composing at home in the morning, at an orchestra rehearsal in the afternoon, and find him unwinding in the evening playing a spot of the new game Piano Hero which is (in my fictional narrative) all the rage in the Viennese coffee shops! From a pedagogical perspective, these three scenarios are chosen because they cover the main forms of digital music representation: audio, sheet music, and symbolic notation. In each case I will demonstrate software prototypes that combines digital music library and music information retrieval research to provide novel forms of access and management of musical digital content. I will then broaden the discussion and relate the work to other forms of media, and (going beyond this) contemplate whether the presented research fits the established definition of a digital library, or if it is perhaps time to repurpose traditional ideas about the structure and capabilities of digital libraries, or even revisit what we define as a digital library.
Professor Bainbridge is Director of the New Zealand Digital Library Research Project

more news...