3rd World Congress on Formal Methods 2019

2nd DaLí Workshop

Dynamic Logic: New Trends and Applications

Porto, 9 October, 2019

NEW: Post-proceedings published as Springer LNCS 12005

NEW: Workshop Programme (pdf)

Overview

Building on the pioneer intuitions of Floyd-Hoare logic, dynamic logic was introduced in the 70's 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 lead 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.

The workshop is promoted by the PT-FLAD Chair on Smart Cities and Smart Governance and 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

Call for Papers: (pdf) (txt)

Invited Speaker

    Dexter Kozen, Cornell University.

    On Free ω-Continuous and Regular Ordered Algebras

    Ordered algebras abound in program logics and programming language semantics: ω-continuous semirings, star-continuous Kleene algebras and Kleene algebras with tests, context-free languages, OI-macro languages, iteration theories, recursion schemes, and Scott domains, among many others. These structures are all examples of varieties of ordered Σ-algebras with restricted completeness and continuity properties. In this talk I will give a general characterization of the free algebras of such varieties in terms of submonads of the monad of Σ-coterms. Varieties of this form are called quasi-regular. For example, the free star-continuous Kleene algebra is the subalgebra of the corresponding free ω-continuous semiring determined by those elements denoted by the regular Σ-coterms, where Σ is the signature of Kleene algebra. This is a special case of a more general construction that applies to any quasi-regular family, including all the examples mentioned above. The talk report on joint work with Zoltán Ésik.

Accepted Papers

  • The trace modality (Dominic Steinhöfel and Reiner Hähnle)
  • Iterative division in the product-free distributive full non-associative Lambek calculus (Igor Sedlar)
  • Persuasive argumentation and epistemic attitudes (Carlo Proietti and Antonio Yuste-Ginel)
  • A four-valued hybrid logic with non-dual modal operators (Diana Costa and Manuel A. Martins)
  • Behavioural and abstractor specifications for dynamic logic with binders and silent transitions (Rolf Hennicker, Alexander Knapp, Alexandre Madeira and Felix Mindt)
  • Mechanizing bisimulation theorems for relation-changing logics in Coq (Raul Fervari, Francisco Trucco and Beta Ziliani)
  • A dynamic epistemic logic analysis of the equality negation task (Eric Goubault, Marijana Lazic, Jérémy Ledent and Sergio Rajsbaum)
  • The logic of AGM learning from partial observations (Alexandru Baltag, Aybüke Özgün and Ana Lucia Vargas Sandoval)
  • Dynamic preference logic as a logic of belief change (Marlo Souza and Alvaro Moreira)
  • A logical analysis of the interplay between social influence and friendship selection (Sonja Smets and Fernando R. Velázquez-Quesada)
  • Stit semantics for epistemic notions based on information disclosure in interactive settings (Aldo Iván Ramírez Abarca and Jan Broersen)
  • Resource separation in dynamic logic of propositional assignments (Joseph Boudou, Andreas Herzig and Nicolas Troquard

Accepted Short Papers

  • A dynamic logic for QASM programs (Carlos Tavares)
  • A labelled sequent calculus for dynamic predicate logic (Elio La Rosa)
  • On the construction of multi-valued concurrent dynamic logic (Leandro Gomes)

Topics

Submissions were invited 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

Submission and publication

Submissions of original papers (unpublished and not submitted for publication elsewhere), up to 15 pages in LNCS style, are invited through this link.

As in the previous edition, the post-proceedings will be published by Springer as a Lecture Notes in Computer Science volume.

Selected papers will be invited for an extended submssion to a Special Issue of the Journal of Logical and Algebraic Methods in Programming, Elsevier.

Venue

Information is available at FM Week 2019

Chairs

Programme Committee

  • Guillaume Aucher (IRISA, FR)
  • Carlos Areces (U Cordoba, AR)
  • Mário Benevides (UFRJ, BR)
  • Johan van Benthem (U Stanford, USA)
  • Patrick Blackburn, (U Roskilde, DK)
  • Thomas Bolander (DTU, Denmark)
  • Zoe Christoff (U Bayreuth, Germany)
  • Fredrik Dahlqvist (UCL, UK)
  • Hans van Ditmarsch (LORIA, Nancy, FR)
  • Nina Gierasimczuk (DTU, Denmark)
  • Valentin Goranko (U Stockholm, SE)
  • Davide Grossi (U Groningen, NL)
  • Reiner Hähnle (TU Darmstadt, DE)
  • Rolf Hennicker (LMU, Munchen, DE)
  • Andreas Herzig (U Toulouse, FR)
  • Dexter Kozen (Cornell, USA)
  • Clemens Kupke (U Strathclyde, UK)
  • Alexandre Madeira (U Aveiro, PT)
  • Manuel A. Martins (U Aveiro, PT)
  • Paulo Mateus (IST, PT)
  • Stefan Mitsch (CMU, USA)
  • Renato Neves (U Minho, PT)
  • Valéria de Paiva (Nuance Comms, USA)
  • Aybuke Ozgun (ILLC, NL)
  • Fernando Velazquez-Quesada (ILLC, NL)
  • Olivier Roy (U Bayreuth, DE)
  • Lutz Schröder (FAU, Erlangen-Nürnberg, DE)
  • Alexandra Silva (UCL, UK)
  • Sonja Smets (UvA, NL)
  • Rui Soares Barbosa (U Oxford, UK)
  • Tinko Tinchev (Sofia U, BG)
  • Renata Wassermann (USP, BR)

Previous Edition

Important Dates

  • Paper Submission (EXTENDED): Jun 28, 2019
  • Notification: Jul 19, 2019
  • Revised version (for the workshop): Sep 2, 2019
  • Camera Ready (post-proceedings): Oct 25, 2019
  • Workshop: Oct 9, 2019

Post-Proceedings

Special Issue