Workshop affiliated with LICS, as part of FLOC.

DaLí - Dynamic Logic: new trends and applications

NOW AN ONLINE EVENT

31 July and 1 August 2022

Slides of the talks are now available: just click on the title of the corresponding talk to see the slides! Alternatively, click here for downloading a zip file.

Overview

Dynamic logic (DL), a generalisation of the logic of Floyd-Hoare introduced in the 70s by Pratt, is a well-known and particularly powerful way of combining propositions, for capturing static properties of program states, and structured actions, responsible for transitions from a state to another (and typically combined through a Kleene algebra to express sequential, non-deterministic, iterative behaviour of systems), into a formal framework to reason about, and verify, classic imperative programs.

Over time Dynamic logic grew to encompass a family of logics increasingly popular in the verification of computational systems, and able to evolve and adapt to new, and complex validation challenges. In particular, the dynamic logic community is interested in the study of operators that can modify the structure in which they are being evaluated. Examples include dynamic logics tailored to specific programming problems or paradigms (e.g., separation logics to model the evolution of a program heap); languages to reason and represent evolving information (e.g., dynamic epistemic logics); and formalism that aim to model new computing domains, including probabilistic, continuous and quantum computation.

Dynamic logic is not only theoretically relevant, but it also shows enormous practical potential and it is indeed a topic of interest in several scientific venues, from wide-scope software engineering conferences to modal logic specific events. That being said, DaLí is the only event exclusively dedicated to this topic. It is our aim to once again bring together in a single place the heterogeneous community of colleagues which share an interest in Dynamic logic - from Academia to Industry, from Mathematics to Computer Science, - to promote their works, to foster great discussions and new collaborations.

Invited talks

  • Marta Bílková (Institute of Computer Science, Czech Academy of Sciences, CZ):

    • Belnapian logics for uncertainty

    Reasoning about information, its potential incompleteness, uncertainty, and contradictoriness need to be dealt with adequately. While incompleteness and uncertainty are typically accommodated within one formalism, e.g. within various models of imprecise probability, contradictoriness and uncertainty less so - conflict or contradictoriness of information is rather chosen to be resolved than to be reasoned with. To reason with conflicting information, positive and negative support - evidence in favour and evidence against - a statement are quantified separately in the semantics. This two-dimensionality gives rise to logics interpreted over twist-product algebras or bi-lattices, the well known Belnap-Dunn logic of First Degree Entailment being a prominent example. Belnap-Dunn logic with its double-valuation frame semantics can in turn be taken as a base logic for defining various uncertainty measures on de Morgan algebras, e.g. Belnapian (non-standard) probabilities or belief functions.
    In spirit similar to Belnap-Dunn logic, we have introduced many-valued logics suitable to reason about such uncertainty measures. They are interpreted over twist-product algebras based on the [0,1] real interval as their standard semantics and can be seen to account for the two-dimensionality of positive and negative component of (the degree of) belief or likelihood based on potentially contradictory information, quantified by an uncertainty measure. The logics presented in this talk include expansions of Łukasiewicz with a de-Morgan negation which swaps between the positive and negative semantical component.
    Our main objective is to utilise apparatus of two-layered logics to formalise reasoning with uncertain information, which itself might be non-classical, i.e., incomplete or contradictory. Many-valued logics with a two-dimensional semantics mentioned above are used on the outer layer to reason about belief, likelihood or certainty based on potentially incomplete or contradictory evidence, building on Belnap-Dunn logic as an inner logic of the underlying evidence. This results in two-layered logics suitable for reasoning scenarios when aggregated evidence yields a Belnapian probability measure or a belief function on a De Morgan algebra.

    (This talk is rooted in joint work with S. Frittella, D. Kozhemiachenko, O. Majer and S. Nazari.)

  • Nina Gierasimczuk (Technical University of Denmark, DK):

    • Learning and Dynamic Modal Logic

    In my talk I will discuss the modal-logical and topological perspective on learnability. The first links between dynamic epistemic logic and computational learning theory was introduced in [6,7,8], where it was shown that exact learning in finite time (also known as finite identification, see [10,11]) can be modelled in dynamic epistemic logic, and that the elimination process of learning by erasing [9] can be seen as iterated upgrade of dynamic doxastic logic. This bridge opened a way to study truth-tracking properties of doxastic upgrade methods on positive, negative, and erroneous input [2,4]. Switching from relational to topological semantics for modal logic allowed characterising favourable conditions for learning in the limit in terms of general topology [3] and culminated in proposing a Dynamic Logic for Learning Theory, which extends Subset Space Logics [5] with dynamic observation modalities and a learning operator [1].

    [1] Baltag, Gierasimczuk, Özgün, Vargas-Sandoval, and Smets, A dynamic logic for learning theory, Journal of Logical and Algebraic Methods in Programming, vol. 109 (2019), pp. 100485.
    [2] Baltag, Gierasimczuk, and Smets, Belief revision as a truth-tracking process, Proceedings of TARK’11, ACM, New York, 2011, pp. 187-190. [3] Baltag, Gierasimczuk, and Smets, On the solvability of inductive problems: A study in epistemic topology, Proceedings of TARK’15, vol. 215, EPTCS, 2016, pp. 81-98.
    [4] Baltag, Gierasimczuk, and Smets, Truth-tracking by belief revision, Studia Logica, vol. 107 (2019), no. 5, pp. 917-947.
    [5] Dabrowski, Moss, and Parikh, Topological reasoning and the logic of knowledge, Annals of Pure and Applied Logic, vol. 78 (1996), no. 1, pp. 73-110.
    [6] Gierasimczuk, Bridging learning theory and dynamic epistemic logic, Synthese, vol. 169 (2009), no. 2, pp. 371-384.
    [7] Gierasimczuk, Learning by erasing in dynamic epistemic logic, Proceedings of LATA’09, vol. 5457, LNCS, Springer, 2009, pp. 362-373.
    [8] Gierasimczuk, Knowing One’s Limits. Logical Analysis of Inductive Inference, PhD thesis, Universiteit van Amsterdam, The Netherlands, 2010.
    [9] Lange, Wiehagen, and Zeugmann, Learning by erasing, ALT 1996: Algorithmic Learning Theory, vol. 1160, LNCS, Springer, 1996, pp. 228-241.
    [10] Lange and Zeugmann, Types of monotonic language learning and their characterization, Proceedings of COLT’92, ACM, New York, 1992, pp. 377-390.
    [11] Mukouchi, Characterization of finite identi cation, Proceedings AII’92, vol. 642, LNCS, Springer, 1992, pp. 260-267.

  • Elaine Pimentel (University College London, UK):

    • Proof theory, countermodels and optimal complexity for modal logics - This is a joint talk with Tiziano Dalmonte.

    When referring to proof theory for modal logics, undoubtedly there are sequent calculi for a number of modal logics exhibiting many good properties (such as analyticity) which can be used in complexity-optimal decision procedures. However, their construction often seems ad-hoc, they are usually not modular, and they mostly lack philosophically relevant properties such as separate left and right introduction rules for the modalities. These problems are often connected to the fact that the modal rules in such calculi usually introduce more than one connective at a time.
    One way of solving this problem is by considering extensions of the sequent framework that are expressive enough for capturing these modalities using separate left and right introduction rules.
    In this talk we explore the connections between several sequent based calculi for normal and non-normal modal and deontic logics. By proposing local versions to ordinary sequent rules we obtain analytic calculi for a number of logics, including to our knowledge the first nested/hyper sequent calculi for a large class of simply dependent multimodal logics, and for many standard non-normal modal logics. The resulting systems are modular and have separate left and right introduction rules for the modalities. While this granulation of the sequent rules introduces more choices for proof search, we propose terminating proof search strategies in the calculi, shown optimal in most of the cases. Finally, we show how to directly extract countermodels for failed proof attempts and launch some ideas of applications to the Dynamic setting.

    This is a joint work with Tiziano Dalmonte, Nicola Olivetti and Björn Lellmann.

  • Fernando Velázquez Quesada (University of Bergen, NO):

    • (Arbitrary) partial communication

    Dynamic epistemic logic (DEL) is the extension of epistemic logic that focuses on representing actions that transform the individual and collective knowledge/beliefs of a set of agents. Its main feature is that actions are semantically represented as operations that modify the underlying semantic model. The paradigmatic DEL proposals (public and diverse forms of non-public announcements, belief revision) study epistemic actions through which the agents receive information from an external source. Yet, the agents do not need to wait for some external entity: they can also share their individual information with one another.
    This talk discusses some of such actions, focussing in particular on that of "partial communication": a set of agents sharing all their information about a particular topic. The first part of the talk defines the model operation representing this action, discussing some of its basic properties, presenting an axiom system for its modality, and comparing it with a public announcement. The second part of the talk introduces a further dynamic modality that quantifies over topics, a form of arbitrary partial communication. Once again, the talk discusses the action's basic properties, its axiom system as well as its relationship with its public announcement counterpart, arbitrary public announcements.

    This is joint work with Rustam Galimullin.

List of Accepted Papers (alphabetically, by first author)

A booklet with all accepted full papers can be found here.

List of Accepted Short Papers (alphabetically, by first author)

A booklet with all accepted short papers can be found here.

Important dates

  • May 3rd, 2022 -- May 18th, 2022 (Extended!): Abstract deadline
  • May 10th, 2022 -- May 25th, 2022 (Extended!): Full paper deadline
  • June 15th, 2022 -- July 2nd, 2022 (Extended!): Author notification
  • July 15th, 2022: Final version deadline (booklet)
  • TBA: Post proceedings deadline
  • TBA: Special issue invitation

Submissions and publications

Authors are invited to submit original papers (unpublished and not submitted for publication elsewhere) up to 15 pages in LNCS style. Papers will be published in a Lecture Notes in Computer Science Volume, Springer.

Extended versions of selected contributions will be published in a special issue of the Journal of Logical and Algebraic Methods in Programming, Elsevier.

Extended abstracts with preliminarily results and work in progress (2-5 pag) are also welcomed for short presentations.

Submissions should be handled with Easychair, following this link.

Topics

We invite submissions on the general field of Dynamic Logic, its variants and applications, including, but not restricted to:
  • Dynamic logic, foundations and applications
  • Logics with regular modalities
  • Modal/temporal/epistemic logics
  • Kleene and action algebras and their variants
  • Quantum dynamic logic
  • Coalgebraic modal/dynamic logics
  • Graded and fuzzy dynamic logics
  • Dynamic logics for cyber-physical systems
  • Dynamic epistemic logic
  • Complexity and decidability of variants of dynamic logics and temporal logics
  • Model checking, model generation and theorem proving for dynamic logics

Venue and Registration

DaLí is now an online event and will be hosted on Zoom.

Registration is free. Please register using the following link: DaLí registration.

Galaofspheres
Galatea of the Spheres, Salvador Dalí (1952)

Chairs

Invited Speakers

Program Committee

  • Thomas Ågotnes (U. Bergen, NO)
  • Natasha Alechina (Utrecht U., NL)
  • Carlos Areces (U. Córdoba, AR)
  • Philippe Balbiani (IRIT, FR)
  • Serenella Cerrito (U. d'Evry Val d'Essonne, FR)
  • Diana Costa (U. Lisbon, PT)
  • Giovanna D'Agostino (U. Udine, IT)
  • Stéphane Demri (CNRS, FR)
  • Hans van Ditmarsch (Open University, NL)
  • Raul Fervari (U. Córdoba, AR)
  • Sabine Frittella (LIFO, FR)
  • Nina Gierasimczuk (TU Denmark, DK)
  • Rajeev Goré (Vienna U. of Technology, AU and Polish A. of Science, PO)
  • Rolf Hennicker (LMU Munich, DE)
  • Reiner Hähnle (TU Darmstadt, DE)
  • Sophia Knight (U. Minnesota, USA)
  • Clemens Kupke (U. Strathclyde, UK)
  • Stepan Kuznetsov (Steklov Mathematical Institute, RU)
  • Alexandre Madeira (U. Aveiro, PT)
  • Sonia Marin (U. Birmingham, UK)
  • Manuel A. Martins (U. Aveiro, PT)
  • Larry Moss (Indiana University Bloomington, USA)
  • Cláudia Nalon (U. Brasília, BR)
  • Nicola Olivetti (Aix-Marseille U., FR)
  • Eric Pacuit (U. Maryland, USA)
  • Alessandra Palmigiano (Vrije Universiteit Amsterdam, NL)
  • Vít Punčochář (Czech Academy of Sciences, CZ)
  • Katsuhiko Sano (Hokkaido U., JP)
  • Igor Sedlár (Czech Academy of Sciences, CZ)
  • Rineke Verbrugge (U. Groningen, NL)
  • Frank Wolter (U. Liverpool, UK)

    • Steering Committee

    • Alexandru Baltag (U. Amsterdam, NL)
    • Alexandre Madeira (U. Aveiro, PT)
    • Andreas Herzig (IRIT, U. Paul Sabatier, FR)
    • David Harel (The Weizmann Institute of Science, IL)
    • Dexter Kozen (Cornell U., USA)
    • Fenrong Liu (Tsinghua U., CH)
    • Johan van Benthem (U. Amsterdam, NL)
    • Hans van Ditmarsch (Open University, NL)
    • Igor Sedlár (Czech Academy of Sciences, CZ)
    • Luís Soares Barbosa (U. Minho, PT), Chair
    • Manuel Martins (U. Aveiro, PT)
    • Mário Benevides (Federal U. Rio de Janeiro, BR)
    • Nina Gierasimczuk (U. Amsterdam, NL)
    • Sonja Smets (U. Amsterdam, NL)
    • Vaughan Pratt (Stanford U., USA)

      • Program

    • Timetable 2022

Authors: C. Areces, D. Costa, chairs of DaLí 2022. Website hosted by Faculty of Sciences, University of Lisbon. Last updated 25/07/2022.