Research projects
Programs in the wild: Uncertainties, adaptabiLiTy and veRificatiON (ULTRON)
Official website: https://sites.google.com/view/projectultron/home-page
Participants:
Valentina Castiglioni (PI, Reykjavik University)
Luca Aceto (Reykjavik University and Gran Sasso Science Institute)
Anna Ingolfsdottir (Reykjavik University)
Michele Loreti (University of Camerino)
Simone Tini (University of Insubria)
Summary:
In this project we consider the problem of specifying and verifying the behaviour of systems characterised by a close interaction of a program with the environment. The latter includes user inputs, multiple heterogeneous interacting devices, and all the (physical) phenomena determining the conditions under which a program has to perform.
In this setting, the main challenge for formal analysis and verification is the unpredictability of the environment, which is usually characterised by a highly dynamical behaviour. For instance, some devices may appear, disappear, or become temporarily unavailable; arbitrary decisions by the users can change the behaviour of some components; some unexpected behaviour caused by the interplay of events that cannot be observed in practice or that were not predicted at design time may occur.
The introduction of uncertainties and approximations in design, modelling and analysis of these systems is therefore inevitable to achieve some degree of system robustness and resilience.
Moreover, each program should be able to adapt its behaviour with respect to the current environmental conditions.
Our main objective is to address the above-mentioned challenges by developing
a general framework for the modelling, analysis, and verification of systems under uncertainties.
In detail we aim at:
Defining a framework for the analysis of the robustness and adaptability of programs and their performance; and
Developing efficient verification techniques for the considered systems.
Participants:
The proposers: Luca Aceto (PI, Reykjavik University), Anna Ingolfsdottir (co-PI, Reykjavik University), Bas Luttik (co-proposer, TU Eindhoven), Alexandra Silva (co-proposer, University College London)
Postdocs: Valentina Castiglioni (Reykjavik University), Clemens Grabmayer (Gran Sasso Science Institute), Mathias R. Pedersen (Reykjavik University)
PhD students: Elli Anastasiadi (Reykjavik University)
Summary: The overarching goal of this project is to solve some of the challenging open problems in the equational axiomatization of behavioural equivalences over process calculi. In particular, the project aims at
obtaining complete equational axiomatizations of various notions of bisimilarity over terms (possibly including variables) in the recursion-free fragment of Milner's Calculus of Communicating Systems (CCS), using suitable auxiliary operators,
extending classic nonfinite axiomatizability results for strong bisimilarity over CCS to the setting of equivalences abstracting from internal steps in computations, and
developing general techniques for transferring positive and negative results on the existence of finite equational axiomatizations of process equivalences between languages and between versions of behavioural equivalences that differ in their treatment of internal steps in process behaviours.
Despite over thirty years of work in the field of algebraic process theory, those problems have not been completely solved in the literature. Thus, the results obtained within this project will lead to an improved understanding of the power of the classic logic of equations in describing and reasoning about a ubiquitous class of computing systems, and will have impact on future work on algebraic methods in concurrency theory. Moreover, the techniques used to achieve them will expand the toolbox of the working concurrency theorist and will be applied to specific, unsolved axiomatic questions that are within the scope of the project. The axiomatizations obtained within the project may also be applied in the computer-assisted analysis of concurrent systems using theorem-proving technology. Last, but not least, apart from the intrinsic scientific interest of the proposed work, building on the successful Polymath experience, the project will be the first one in concurrency theory (and perhaps in computer science as a whole) that uses large-scale on-line collaboration to solve problems in that field, thus providing a blueprint for future research cooperation.