Location: Haifa (or hybrid)
Date: July 31 2022
- R. Ramanujam (IMSc, India): firstname.lastname@example.org
- Yanjing Wang (Peking University, China): email@example.com
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. That is, 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 seems 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 [Hodkinson, Wolter, Zakharyaschev 2000]. Another recent idea is to bundle the quantifiers and modalities together in certain forms, inspired by applications in non-standard epistemic logic [Wang 2017] [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 will have three invited talks that present surveys of what has been achieved, highlighting the difficulties arising from combining quantification and modalities. There will be up to 5 contributed talks, and an open problem session at the end of the day.
Eugenio Orlandelli (University of Bologna)
Ian Pratt-Hartmann (University of Manchester)
Frank Wolter (University of Liverpool)