This article is a follow-up study on the modal logic of stepwise removal of objects, MLSR, which was first introduced by van Benthem et al. [13]. We recapitulate the main results from [13] and also provide some new results. After introducing MLSR and its corresponding removal modality, we analyze its expressive power and prove a bisimulation characterization theorem. We then provide a complete Hilbert-style axiomatization in a hybrid language enriched with nominals and public announcement operators. Next, we show that model-checking for MLSR is PSPACE-complete, that MLSR lacks the finite model property, and that its satisfiability problem is undecidable—even when we forbid the nesting of removal operators by restricting the removal operator to formulas in the basic modal language. Then, we consider an issue of fine-structure: the expressive power gained by adding the stepwise removal modality to various fragments of first-order logic. Lastly, to conclude our investigation of the complexity threshold from decidable to undecidable, we propose a decidable protocol variant of MLSR.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A New Look at the Modal Logic of Stepwise Removal

  • Johan van Benthem,
  • Krzysztof Mierzewski,
  • Francesca Zaffora Blando

摘要

This article is a follow-up study on the modal logic of stepwise removal of objects, MLSR, which was first introduced by van Benthem et al. [13]. We recapitulate the main results from [13] and also provide some new results. After introducing MLSR and its corresponding removal modality, we analyze its expressive power and prove a bisimulation characterization theorem. We then provide a complete Hilbert-style axiomatization in a hybrid language enriched with nominals and public announcement operators. Next, we show that model-checking for MLSR is PSPACE-complete, that MLSR lacks the finite model property, and that its satisfiability problem is undecidable—even when we forbid the nesting of removal operators by restricting the removal operator to formulas in the basic modal language. Then, we consider an issue of fine-structure: the expressive power gained by adding the stepwise removal modality to various fragments of first-order logic. Lastly, to conclude our investigation of the complexity threshold from decidable to undecidable, we propose a decidable protocol variant of MLSR.