Workshop co-located with TABLEAUX, FROCOS and ITP 2017

DaLí - Dynamic Logic: new trends and applications

Brasília, 23 and 24 September, 2017


Building on the pioneer intuitions of Floyd-Hoare logic, Dynamic Logic was introduced in the 70's by Pratt as a suitable logic to reason about, and verify, classic imperative programs. Since then, the original intuitions grew to an entire family of logics, which became increasingly popular for assertional reasoning about a wide range of computational systems. Simultaneously, their object (i.e. the very notion of a program) evolved in unexpected ways. This leads to dynamic logics tailored to specific programming paradigms and extended to new computing domains, including probabilistic, continuous and quantum computation. Both its theoretical relevance and practical potential make Dynamic Logic a topic of interest in a number of scientific venues, from wide-scope software engineering conferences to modal logic specific events. However, no specific event is exclusively dedicated to it. This workshop aims at filling fill such a gap, joining an heterogeneous community of colleagues, from Academia to Industry, from Mathematics to Computer Science. Furthermore, it will provide a forum for disseminating and sharing new trends and applications of Dynamic Logic. Co-location with TABLEAUX, FroCoS, and ITP offers the perfect conditions for a fruitful fostering of synergies.

The workshop is promoted by the project DaLí - Dynamic logics for cyber-physical systems: towards contract based design (POCI-01-0145-FEDER-016692), a R&D project supported by the Portuguese Foundation for Science and Technology

Invited talks

  • Alexandru Baltag. LOGIC GOES VIRAL: dynamic modalities for social networks
  • Hermann Haeusler. Propositional Dynamic Logic with Petri net programs: A discussion and a logical system

    Accepted Papers

    Regular papers (to appear in the LNCS volume)

  • Alexandru Baltag, Nina Gierasimczuk, Ana Lucia Vargas, Aybuke Özgün and Sonja Smets. A Dynamic Logic for Learning Theory
  • Carlos Areces, Raul Fervari, Guillaume Hoffmann and Mauricio Martel. Undecidability of Relation-Changing Modal Logics
  • Helle Hvid Hansen, Clemens Kupke, Johannes Marti and Yde Venema. Parity Games and Automata for Game Logic
  • Philippe Balbiani and Joseph Boudou. Axiomatization and computability of a variant of iteration-free PDL with fork
  • José Luiz Fiadeiro, Ionut Tutu, Antónia Lopes and Dusko Pavlovic Logics for Actor Networks: a case study in constrained hybridization
  • Luis Barbosa. Layered logics, coalgebraically
  • Marlo Souza, Alvaro Moreira and Renata Vieira. Dynamic Preference Logic as a logic of Belief Change
  • Raul Fervari and Fernando R. Velázquez-Quesada. Dynamic Epistemic Logics of Introspection
  • Sophie Pinchinat, Francois Schwarzentruber and Tristan Charrier. Model checking against arbitrary public announcement logic: A first-order-logic prover approach for the existential fragment
  • Sonja Smets and Fernando R. Velázquez-Quesada. The Creation and Change of Social Networks: a logical study based on group size
  • Vaughan Pratt. Dynamic Logic: A personal perspective
  • Yuri David Santos. A Dynamic Informational-Epistemic Logic

    Short Presentations

  • Carlos Tavares. Towards a quantum-probabilistic dynamic logic
  • Daniel Figueiredo and Manuel A. Martins. Bisimulations for reactive frames
  • Diana Costa and Édi Duarte. Checkers Game in Deontic logic
  • Diego Fernandes Expressiveness comparisons of modal logics
  • Konstantinos Gkikas and Alexandru Baltag. Stable beliefs and conditional probability spaces
  • Leandro Gomes. Contract-based design for software verification
  • Luiz Carlos Pereira. Constructive fragments of Classical Modal Logic and the Ecumenical Perspective
  • Fabricio Chalub, Alexandre Rademaker, Edward Hermann Haeusler and Christiano Braga. Fixing the proof of completeness of ALC Sequent Calculus
  • Sophie Pinchinat and Francois Schwarzentruber. The Hintikka’s world project


  • Time Table

    Important dates

  • May 26, 2017 June 18 : Abstract deadline
  • June 2, 2017 June 18: Full paper deadline
  • July 14, 2017 July 23: Author notification
  • TBA: Final version 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. Submissions should be handled with this EasyChair link and will be published in a Lecture Notes of Computer Science Volume, Springer.

    Extended versions of the DaLí contributions will be invited to a special issue in the Journal of Logic and Algebraic Methods in Programming, Elsevier.

    Extended abstracts with preliminarily results and work in progress (2-5 pag) are also welcomed for short presentations. They are subject of a light reviewing and will be available at conference in a informal booklet. Submissions should be handled with this EasyChair link.


    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

  • Chairs

    Invited Speaker

    Program Committee


  • information is available at TABLEAUX, FROCOS and ITP 2017


  • is now open in this form