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.
We expect to have three 45-minute talks that present surveys of what has been achieved, highlighting the difficulties arising from combining quantification and modalities. There will be three of these invited talks, up to 5 contributed talks, and an open problem session at the end of the day.
Erich Grädel (RWTH Aachen)
Ian Pratt-Hartmann (University of Manchester)
Frank Wolter (University of Liverpool)
We invite short abstracts of up to 5 pages in 12-point article style, outlining research in this area. We welcome accounts of already published research or work in progress. A special issue of a well-known journal is to be planned.