Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)
arxiv(2020)
摘要
We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(*) contains the separating conjunction * from separation logic. Though both operators are second-order in nature, we show that ML(|) is as expressive as the graded modal logic GML (on finite trees) whereas ML(*) lies strictly between ML and GML. Moreover, we establish that the satisfiability problem for ML(*) is Tower-complete, whereas for ML(|) is (only) AExpPol-complete. As a by-product, we solve several open problems related to sister logics, such as static ambient logic, modal separation logic, and second-order modal logic on finite trees.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要