CELLO team is organizing a workshop on Tuesday, May 9th in room B013.
9:00 – 9:30
9:30 – 10:30
speaker: Thomas Studer, University of Bern, Switzerland
title: Blockchain Logic
abstract: Blockchains are distributed data structures that are used to achieve consensus in systems for cryptocurrencies (like Bitcoin) or smart contracts (like Ethereum). Although blockchains gained a lot of popularity recently, there is no logic-based model for blockchains available. In our talk, we present the basic principles and mechanisms of blockchains and discuss the need for various kinds of blockchain logics. Then we introduce BCL, an epistemic logic to reason about the belief change dynamics induced by blockchain updates. We establish soundness and completeness of BCL with respect to a simple blockchain model.
10:30 – 11:30
speaker: Philippe Balbiani, IRIT/CNRS, Toulouse
title: Unification in propositional logics
abstract: The research on admissibility and unification for logical systems was originally motivated by automatic deduction tools. Today, admissibility and unification constitute the heart of an active research area: Rybakov (1984) and, later on, Ghilardi (1999) demonstrated that several intermediate or modal logics have decidable admissibility and unification problems; Ghilardi (2000) established their unification types; Jerabek (2007) examined their complexity; applications in the design and maintenance of knowledge bases has been considered by Baader and Narendran (2001), Baader and Küsters (2001) and Baader and Morawska (2009) within the context of description logics. Nevertheless, much remains to be done, seeing that little is known about admissibility and unification in several non-classical logics such as intermediate logics, modal logics and description logics. In this talk, we will give a survey of the results on unification in these non-classical logics and we will present some of the open problems whose solution will have a great impact on the future of the area.
11:30 – 12:00
12:00 – 12:30
speaker: Louwe B. Kuijer, LORIA/CNRS (CELLO), Nancy & University of Liverpool, United Kingdom
title: Modal Logics, Grids and Undecidability
abstract: One of the standard methods for proving that the validity/satisfiability problem of a modal logic is undecidable, is to show that the logic in question can encode a ZxZ grid. This grid can then be used to encode various problems that are known to be undecidable, such as the tiling problem or the halting problem. In this talk, I discuss this method in general, and its application to several specific modal logics in particular.
12:30 – 13:00
speaker: Christophe Chareton, LORIA/CNRS (CELLO), Nancy
title: Strategy refinement
abstract: Temporal multi-agent logics such as ATL-ATL*, ATLsc, SL can express the capacities of agents to ensure the satisfaction of temporal properties. In particular, SL and ATLsc enable agents to interact in a semantic game. We propose a new formalism called Updating Strategy Logic (USL). In USL an agent can also refine its own strategy. USL is a modification of SL. The difference with SL is that the successor of a given state is not uniquely determined by a single choice by each agent. The language has an operator that is called an unbinder. It explicitely deletes the binding of a strategy to an agent. We show that USL is strictly more expressive than SL. The model checking complexity for USL and its memoryless version are the same as those of formalisms with implicit unbinders, such as SL and ATLsc.
13:00 – 14:00
Lunch in the LORIA restaurant
14:00 – 14:30
speaker: Zeinab Bakhtiari, LORIA/CNRS (CELLO), Nancy
title: Neighborhood contingency bisimulation
abstract: We introduce a notion of bisimulation for contingency logic interpreted on neighborhood structures, characterize this logic as bisimulation invariant fragment of modal logic and of first-order logic, and compare it with existing notions in the literature.
14:30 – 15:00
speaker: Ioannis Kokkinis, LORIA/CNRS (CELLO), Nancy
title: On the Complexity of the Satisfiability Problem in Probabilistic Logics
abstract: We present some probabilistic logics and we discuss methods for proving upper and lower complexity bounds for the satisfiability problem in these logics. This is joint work with Antonis Achilleos.
15:00 – 15:30
15:30 – 16:30
speaker: Francesco Belardinelli, University of Evry
title: A Logic for Global and Local Announcements
abstract: We introduce a dynamic epistemic logic called the Logic of Global and Local Announcements (GLAL). It has global announcement operators and local announcement operators, indexed to a subset A of the set of all agents. We provide a unified semantical account for both types of announcement in terms of pointed model updates, and illustrate the formal machinery by means of epistemic scenarios. GLAL is strictly more expressive than public announcement logic. We also analyse the expressive power of GLAL through bisimulation relations that preserve the interpretation of formulas in GLAL. The talk reports on current joint work with Hans van Ditmarsch and Wiebe van der Hoek.
16:30 – 17:30
speaker: Ramanujam, IMSc, Chennai, India
title: Identity and agency in epistemic logics
abstract: We start with what seem like natural notions of agency and social interaction between agents, and define what seem to be reasonable computational models for multi-agent systems. We discuss the use of modal epistemic logics, temporal logics and game-like logics for reasoning about different aspects of such systems, and point to conceptual difficulties in combining them.