Affiliated Workshop of ICLAPLiCS 2020 in Beijing

Venue: Peking University

Date: July 6th 2020

Organizers:

 

Background

Propositional Modal Logic has found major applications in computer science in the formal specification and verification of finite-state systems in general, and multi-agent systems in AI. In the last two decades, researchers have been attempting to extend verification techniques to infinite-state systems that arise in distributed computing, database theory, and security theory. Reasoning about such systems typically involves both modalities (to express state transitions and1 reachability) and quantifiers (to refer to unbounded data, dynamically created processes, etc). This naturally leads us to the realm of first-order modal logic (FOML).

Indeed, early formulations of programming logics in the 1980s like Dynamic logic, Hoare logic, etc were first-order modal logics. However, unlike propositional modal logics which are robustly decidable(in the sense that natural ex-tensions of many kinds are decidable), FOML is notoriously undecidable. Thatis, it is very hard to find non-trivial decidable fragments of FOML. The thorough knowledge that we have obtained in the past decades about decidable fragments of first-order logic and decidable extensions of modal logic seem to help very little. For example, the two-variable fragment of FOML is already undecidable. The combination of modalities and quantifiers causes new problems that occur neither in the first-order case nor in the propositional modal case.

Despite such discouragement, this century has seen some small steps with positive results on new fragments, such as the monodic fragments which restrict the appearance of variables in the scope of modalities [Wolter & Zakharyaschev2001]. Another recent idea is to bundle the quantifiers and modalities together in certain forms, inspired by applications in non-standard epistemic logic [Wang2017] [Padmanabha, Ramanujam and Wang 2018]. Developments in Term-modal logics, a close cousin of FOML suggest that more fragments may be hiding beneath the surface: for instance, the two-variable fragment of Term-modal logic is decidable and constitutes an as-yet uncharacterized fragment of FOML.

This workshop aims to bring the leading researchers on this evolving direction of research and identify both potentially useful fragments of FOML and techniques for constructing decision procedures.

Format

We expect to have five 45-minute talks that present surveys of what has been achieved, highlighting the difficulties arising from combining quantification and modalities. There will be three talks before lunch and two after, with a one-hour open problem session at the end of the day.

Invited Speakers (to be completed)

Ian Pratt-hartmann (University of Manchester)

Frank Wolter (University of Liverpool)