Modal logics are widely used in computer science. The complexity of their satisfiability problems has been an active field of research since the 1970s. We prove that even very "simple" modal logics can be undecidable: We show that there is an undecidable modal logic that can be obtained by restricting the allowed models with a first-order formula in which only universal quantifiers appear.
Term modal logics (TML) are modal logics with unboundedly many modalities, with quantification over modal indices, so that we can have formulas of the form $\exists y. \forall x. (\Box_x P(x,y) \supset\Diamond_y P(y,x))$. Like First order modal logic, TML is also "notoriously" undecidable, in the sense that even very simple fragments are undecidable. In this paper, we show the decidability of one interesting fragment, that of two variable TML. This is in contrast to two-variable First order modal logic, which is undecidable.
We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of Horn formulas with diamonds is undecidable for any type of linear orders and semantics. On the contrary, satisfiability of Horn formulas with boxes is tractable over both discrete and dense orders under the reflexive semantics and over…
Most Properties are Undecidable for Transitive Tense Logics
The Tsinghua-UvA JRC for Logic Department of Philosophy Tsinghua University（清华大学哲学系清华-阿姆斯特丹逻辑联合研究中心）；Institute for Logic, Language and Computation University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）
Institute of Mathematical Sciences, Homi Bhabha National Institute（数学科学研究所，霍米·巴巴国家研究所）；Peking University（北京大学）
Quantified modal logic provides a natural logical language for reasoning about modal attitudes even while retaining the richness of quantification for referring to predicates over domains. But then most fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic) have been shown to be decidable. In this paper, we study fragments that bundle quantifiers and modalities together, inspired by earlier work on epistemic logics of know-how/why/what. As always with quantified modal logics, it makes a significant difference whether the doma…
We prove that the positive fragment of first-order intuitionistic logic in the language with two variables and a single monadic predicate letter, without constants and equality, is undecidable. This holds true regardless of whether we consider semantics with expanding or constant domains. We then generalise this result to intervals [QBL, QKC] and [QBL, QFL], where QKC is the logic of the weak law of the excluded middle and QBL and QFL are first-order counterparts of Visser's basic and formal logics, respectively. We also show that, for most "natural" first-order modal logics, the two-variable …
Propositional term modal logic is interpreted over Kripke structures with unboundedly many accessibility relations and hence the syntax admits variables indexing modalities and quantification over them. This logic is undecidable, and we consider a variable-free propositional bi-modal logic with implicit quantification. Thus $[\forall] α$ asserts necessity over all accessibility relations and $[\exists] α$ is classical necessity over some accessibility relation. The logic is associated with a natural bisimulation relation over models and we show that the logic is exactly the bisimulation invari…
This paper is focused on the study of modal logics defined from valued Kripke frames, and particularly, on computability and expressibility questions of modal logics of transitive Kripke frames evaluated over certain residuated lattices. It is shown that a large family of those logics -- including the ones arising from the standard MV and Product algebras -- yields an undecidable consequence relation. Later on, the behaviour of transitive modal Lukasiewicz logic is compared with that of its non transitive counterpart, exhibiting some particulars concerning computability and equivalence with ot…
In this work we study the decidability of a class of global modal logics arising from Kripke frames evaluated over certain residuated lattices, known in the literature as modal many-valued logics. We exhibit a large family of these modal logics which are undecidable, in contrast with classical modal logic and propositional logics defined over the same classes of algebras. This family includes the global modal logics arising from Kripke frames evaluated over the standard Lukasiewicz and Product algebras. We later refine the previous result, and prove that global modal Lukasiewicz and Product lo…
Relation-changing modal logics are extensions of the basic modal logic that allow changes to the accessibility relation of a model during the evaluation of a formula. In particular, they are equipped with dynamic modalities that are able to delete, add, and swap edges in the model, both locally and globally. We provide translations from these logics to hybrid logic along with an implementation. In general, these logics are undecidable, but we use our translations to identify decidable fragments. We also compare the expressive power of relation-changing modal logics with hybrid logics.
Arbitrary Arrow Update Logic is a dynamic modal logic that uses an arbitrary arrow update modality to quantify over all arrow updates. Some properties of this logic have already been established, but until now it remained an open question whether the logic's satisfiability problem is decidable. Here, we show that the satisfiability problem of Arbitrary Arrow Update Logic is co-RE hard, and therefore undecidable, by a reduction of the tiling problem.
In this article, we start with a two-player game that models communication under adverse circumstances in everyday life and study it from the perspective of a modal logic of graphs, where links can be deleted locally according to definitions available to the adversarial player. We first introduce a new language, semantics, and some typical validities. We then formulate a new type of first-order translation for this modal logic and prove its correctness. Then, a novel notion of bisimulation is proposed which leads to a characterization theorem for the logic as a fragment of first-order logic, a…
We investigate the modal logic of stepwise removal of objects, both for its intrinsic interest as a logic of quantification without replacement, and as a pilot study to better understand the complexity jumps between dynamic epistemic logics of model transformations and logics of freely chosen graph changes that get registered in a growing memory. After introducing this logic ($\textsf{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 for the logic of stepwise…
本文主要研究模态依赖逻辑.它是由Jouko Vääanänen在2007年引入的，作为一阶的扩展（分别为。模态）逻辑的依赖运算符=（）。一阶（resp.）命题）变量x_1，...，x_n，=（x_1，...，x_n）直观地说明x_n的值由x_1，.，x_n-1。我们认为片段的模态依赖逻辑通过限制允许模态和命题连接词的集合。我们对这些片段的可满足性和模型检查问题的复杂性进行了分类。对于可满足性，我们获得了从P over NP，Sigma_P^2和PSPACE到NEXP的复杂度，而对于模型检查，我们只根据它们的易处理性对片段进行分类，即我们在P中显示NP-完全性或包含性。对于这个扩展，我们再次分类的复杂性模型检查问题的片段。在这里，我们获得了从P over NP和coNP到PSPACE的复杂度。最后，我们分析了一阶依赖逻辑、独立友好逻辑及其二元片段。我们证明了两个变量的依赖逻辑的可满足性是NEXP-完全的，而两个变量的独立友好的逻辑，它是不可判定的，并使用这一点来证明，后者也比前者更有表现力。
In this paper, we tell a story about incompleteness in modal logic. The story weaves together a paper of van Benthem, `Syntactic aspects of modal incompleteness theorems,' and a longstanding open question: whether every normal modal logic can be characterized by a class of completely additive modal algebras, or as we call them, V-BAOs. Using a first-order reformulation of the property of complete additivity, we prove that the modal logic that starred in van Benthem's paper resolves the open question in the negative. In addition, for the case of bimodal logic, we show that there is a naturally …
Modal logic is a paradigm for several useful and applicable formal systems in computer science. It generally retains the low complexity of classical propositional logic, but notable exceptions exist in the domains of description, temporal, and spatial logic, where the most expressive formalisms have a very high complexity or are even undecidable. In search of computationally well-behaved fragments, clausal forms and other sub-propositional restrictions of temporal and description logics have been recently studied. This renewed interest on sub-propositional logics, which mainly focus on the com…
We establish a natural translation from word rewriting systems to strictly positive polymodal logics. Thereby, the latter can be considered as a generalization of the former. As a corollary we obtain examples of undecidable strictly positive normal modal logics. The translation has its counterpart on the level of proofs: we formulate a natural deep inference proof system for strictly positive logics generalizing derivations in word rewriting systems. We also formulate some open questions related to the theory of modal companions of superintuitionistic logics that was initiated by L.L. Maximova…
On the Decidability and Complexity of Some Fragments of Metric Temporal Logic
度量时态逻辑$\mtlfull$是研究最多的实时逻辑之一。它表现出相当大的多样性的表达性和可判定性的基础上允许的一套模式和时间间隔的限制$I$的性质。\oomit{The classical results of Alur and Henzinger showed that $\mtlfull$ is undecidable where as $\mitl$ which uses only non-singular intervals $NS$ is decidable. In a surprizing result, Ouaknine and Worrell showed that the satisfiability of $\mtl$ is decidable over finite pointwise models, albeit with NPR decision complexity, whereas it remains undecidable for infinite pointwise models or for continuous time.}在本文中，我们通过证明$\mtlsns$（其中$NS$表示非奇异区间）的可满足性在有限逐点严格单调时间上也是可判定的，从而加强了可判定性结果。我们利用时间投影技术给出了从Ouaknine和Worrell的逻辑$\mtls…
We study the expressivity and complexity of model checking linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking re…
Some prospects for semiproducts and products of modal logics
Institute for Information Transmission Problems, Russian Academy of Sciences（俄罗斯科学院信息传输问题研究所）；National Research University Higher School of Economics（国立高等经济大学）；Moscow State University（莫斯科大学）；School of Computer Science and Applied Mathematics, University of the Witwatersrand（威特沃特斯兰德大学计算机科学与应用数学学院）
A specification given as a formula in linear temporal logic (LTL) defines a system by its set of traces. However, certain features such as information flow security constraints are rather modeled as so-called hyperproperties, which are sets of sets of traces. One logical approach to this is team logic, which is a logical framework for the specification of dependence and independence of information. LTL with team semantics has recently been discovered as a logic for hyperproperties. We study the complexity theoretic aspects of LTL with so-called synchronous team semantics and Boolean negation, …
Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non punctuality called \…
Strategy Logic (SL, for short) has been introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns out to be very powerful, subsuming all major previously studied modal logics for strategic reasoning, including ATL, ATL*, and the like. Unfortunately, due to its high expressiveness, SL has a non-elementarily decidable model-checking problem and the satisfiability question is undecidable, specifically Sigma_1^1. In order to obtain a decidable sublogic, we introduce and study …
The choice of the right trade-off between expressiveness and complexity is the main issue in interval temporal logic. In their seminal paper, Halpern and Shoham showed that the satisfiability problem for HS (the temporal logic of Allen's relations) is highly undecidable over any reasonable class of linear orders. In order to recover decidability, one can restrict the set of temporal modalities and/or the class of models. In the following, we focus on the satisfiability problem for HS fragments under the homogeneity assumption, according to which any proposition letter holds over an interval if…
Putting Perspective into OWL [sic]: Complexity-Neutral Standpoint Reasoning for Ontology Languages via Monodic S5 over Counting Two-Variable First-Order Logic (Extended Version with Appendix)
