Invited Speakers
Luca Bortolussi (University of Trieste, Italy) Joanna Golinska-Pilarek (Institute of Philosophy, University of Warsaw, Poland) Arnaud Sangnier (Laboratoire IRIF, Université Paris Diderot, France)
Short Bios and Talk's Abstracts
Since November 2015, Luca Bortolussi is an Associate Professor of Computer Science at the Department of Mathematics and Geosciences of the University of Trieste, Italy. From June 2014 to May 2015, he has been guest professor at the department of Computer Science of the University of Saarland in Saarbruecken, Germany. Before that, he was assistant professor (Ricercatore) of Computer Science at the Department of Mathematics and Geosciences of the University of Trieste, Italy. He graduated in Mathematics at the University of Trieste in 2003 and got a PhD in Computer Science form the University of Udine in 2007. He is also associate researcher at ISTI-CNR in Pisa. His research interests are mostly focussed on quantitative formal methods, particularly for the analysis of stochastic models of complex systems. He has been recently working, in particular, on the integration of formal verification with stochastic approximation and with machine learning ideas.
Abstract: Many current scientific and technological challenges are related to understanding, designing and controlling complex systems, from epidemic spreading to performance of computer systems, from biological networks to bike and car sharing.
Model-based approaches are one of the key strategies to face such challenges. Models of such systems are typically specified in terms of local interactions between entities involved, but the interest is in global behaviours at the system level, typically known as emergent properties.
Our goal is to study such properties, starting from a stochastic Markov model, with the machinery of formal verification. More precisely, the focus is on the formalisation of such properties in a suitable logical language and on the automatic verification of these properties in a given model (the so called model checking problem), which in a probabilistic setting takes the form of computing the probability with which such properties are satisfied.
However, the models we can construct are always uncertain, in particular in the value of their parameters, due to lack of information and their phenomenological nature. To deal consistently with such an uncertainty, we have combined formal verification techniques with state-of-the-art Machine Learning statistical tools, based on Gaussian Processes.
We will show how to efficiently compute the satisfaction probability of a behavioural property when model parameters are unknown, but assumed to lie in a bounded interval, a method we called Smoothed Model Checking. Combining these ideas with Bayesian Optimisation, we can then efficiently solve system design problems, i.e. fixing controllable model parameters so that the system robustly exhibits a desired behaviour.
This talk will be a gentle introduction to these ideas.
Joanna Golinska-Pilarek is an assistant professor at the Institute of Philosophy (Section of Logic) at the University of Warsaw (since 2006). She received MA in philosophy with honors in 1999, BS in mathematics in 2003, and PhD in logic in 2004 at the University of Warsaw. In 2004-2011 she was an assistant professor at the Department of Advanced Information Technologies at the National Institute of Telecommunications in Poland. She is a recipient of several project grants funded by the Polish Ministry of Science and Higher Education and National Science Centre in Poland. Since 2014 she is the deputy director for research and international cooperation at the Institute of Philosophy. Her research interests are focused on non-classical logics and their applications in cognitive science and computer science. For details see her webpage: www.joannagolinska.com.
Due to personal reasons, Joanna will not be able to attend GandALF 2016. Her talk will be presented by Michał Zawidzki (University of Lodz, Poland).
Michał Zawidzki received the MA degree in political science in 2008, the MA degree in philosophy in 2009 and the BSc degree in mathematics in 2012 from the University of Lodz. His PhD thesis was devoted to hybrid logics, their computational complexity and decision procedures for them. From December 2011 to December 2013 he was a principal investigator in the project "Deductive systems and decidability problem for hybrid logics" funded by the National Science Centre of Poland. He is an author of a monograph on deductive systems for standard and non-standard hybrid logics. His current research interests are located in the fields of modal logics, hybrid logics, decidability and computational complexity of non-classical logics, tableau and sequent calculi, applications of logics in modeling human interactions.
Currently, he is an assistant professor in the Department of Logic at the University of Lodz. Since 2013 he is also a member of the research team of the project "Logics for qualitative reasoning team" under the supervision of dr. Joanna Golinska-Pilarek.
Abstract: Relational decision procedures are based on relational dual tableaux, a powerful tool for verification of validity as well as for proving entailment, model checking and satisfiability checking. Dual tableaux are `top-down’ validity checkers and it holds a duality relation between them and the well known tableau systems. The common language of most relational dual tableaux is the logic of binary relations which was introduced as a logical counterpart to the class of representable relation algebras defined by Tarski.
The methods of relational deduction may be applied to various theories that are translatable into an appropriate fragment and/or extension of the relational logic. Thus, the main advantage of the relational methodology is that it makes it possible to represent within a uniform formalism the three basic components of formal systems: syntax, semantics, and deduction apparatus. Research from the last few decades has shown that the relational approach can be seen as a general framework for representing, investigating, implementing and comparing theories with incompatible languages and/or semantics.
In this talk, we will present some basics of relational dual tableaux methodology and discuss the current state of research on relational decision procedures. We will also show some new results concerning relational decision procedures for some qualitative logics for order of magnitude reasoning.
Arnaud Sangnier obtained his PhD at the Laboratoire Spécification et Vérification of ENS Cachan (France) in 2008. His doctoral thesis was on the automatic verification of programs manipulating pointers and counters. During the year 2009, he did a post-doctoral stay at the university of Torino where he studied together with Jeremy Sproston probabilistic systems equipped with counters à la Petri nets. After that he spent 9 month at Genova to work with Giorgio Delzanno on the verification of parameterized networks. Since autumn 2010, he is associate professor at the University Paris Diderot and a member of the Institut de Recherche en Informatique Fondamentale (IRIF). During the last years he has continued to work in both directions of parameterized verification and analysis of systems with counters.
Abstract: VASS (Vector Addition Systems with States), which are equivalent to Petri nets, are automata equipped with natural variables that can be decremented or incremented. VASS are a powerful model which has been intensively studied in the last decades. Many verification techniques have been developed to analyse them and the frontier between the decidable and undecidable problems related to VASS begins to be well known. One interesting point is that the model-checking of linear temporal logics (like LTL or linear mu-calculus) is decidable for this model but this is not anymore the case when considering branching time temporal logics. However some restrictions can be imposed on the logics and on the studied system in order to regain decidability.
In this talk, we will present these results concerning the model-checking of VASS and the techniques leading to the decidability results. We will then show how these techniques and results can be used to analyse some extensions of VASS with probabilities, namely probabilistic VASS and VASS Markov Decision Processes.
Important Dates
Abstract submission: May 20, 2016
Paper submission: May 27, 2016
Abstract & Paper submission: June 6, 2016
Notification: July 8, 2016
Camera-ready: August 5, 2016
Early registration: August 21, 2016
Late registration: September 4, 2016