Algorithmic properties of modal logics with restricted languages
Modal logics, both propositional and predicate, have been used in computer science since the late 1970s. One of the most important properties of modal logics of relevance to their applications in computer science is the complexity of their satisﬁability problem. The complexity of satisﬁability for modal logics is rather high: it ranges from NP-complete to undecidable for propositional logics and is undecidable for predicate logics. This has, for a long time, motivated research in drawing the borderline between tractable and intractable fragments of propositional modal logics as well as between decidable and undecidable fragments of predicate modal logics. In the present thesis, we investigate some very natural restrictions on the languages of propositional and predicate modal logics and show that placing those restrictions does not decrease complexity of satisﬁability. For propositional languages, we consider restricting the number of propositional variables allowed in the construction of formulas, while for predicate languages, we consider restricting the number of individual variables as well as the number and arity of predicate letters allowed in the construction of formulas. We develop original techniques, which build on and develop the techniques known from the literature, for proving that satisﬁability for a ﬁnite-variable fragment of a propositional modal logic is as computationally hard as satisﬁability for the logic in the full language and adapt those techniques to predicate modal logics and prove undecidability of fragments of such logics in the language with a ﬁnite number of unary predicate letters as well as restrictions on the number of individual variables. The thesis is based on four articles published or accepted for publication. They concern propositional dynamic logics, propositional branchingand alternating-time temporal logics, propositional logics of symmetric rela tions, and ﬁrst-order predicate modal and intuitionistic logics. In all cases, we identify the “minimal,” with regard to the criteria mentioned above, fragments whose satisﬁability is as computationally hard as satisﬁability for the entire logic.
In this article, we investigate the logical structure of memory models of theoretical and practical interest. Our main interest is in “the logic behind a fixed memory model”, rather than in “a model of any kind behind a given logical system”. As an effective language for reasoning about such memory models, we use the formalism of separation logic. Our main result is that for any concrete choice of heap-like memory model, validity in that model is undecidable even for purely propositional formulas in this language.
The main novelty of our approach to the problem is that we focus on validity in specific, concrete memory models, as opposed to validity in general classes of models.
Besides its intrinsic technical interest, this result also provides new insights into the nature of their decidable fragments. In particular, we show that, in order to obtain such decidable fragments, either the formula language must be severely restricted or the valuations of propositional variables must be constrained.
In addition, we show that a number of propositional systems that approximate separation logic are undecidable as well. In particular, this resolves the open problems of decidability for Boolean BI and Classical BI.
Moreover, we provide one of the simplest undecidable propositional systems currently known in the literature, called “Minimal Boolean BI”, by combining the purely positive implication-conjunction fragment of Boolean logic with the laws of multiplicative *-conjunction, its unit and its adjoint implication, originally provided by intuitionistic multiplicative linear logic. Each of these two components is individually decidable: the implication-conjunction fragment of Boolean logic is co-NP-complete, and intuitionistic multiplicative linear logic is NP-complete.
All of our undecidability results are obtained by means of a direct encoding of Minsky machines.
Key Words and Phrases: Separation logic, undecidability, memory models, bunched logic
This two-volume set (CCIS 905 and CCIS 906) constitutes the refereed proceedings of the Second International Conference on Advances in Computing and Data Sciences, ICACDS 2018, held in Dehradun, India, in April 2018. The 110 full papers were carefully reviewed and selected from 598 submissions. The papers are centered around topics like advanced computing, data sciences, distributed systems organizing principles, development frameworks and environments, software verification and validation, computational complexity and cryptography, machine learning theory, database theory, probabilistic representations.
Language and relational models, or L-models and R-models, are two natural classes of models for the Lambek calculus. Completeness w.r.t. L-models was proved by Pentus and completeness w.r.t. R-models by Andréka and Mikulás. It is well known that adding both additive conjunction and disjunction together yields incompleteness, because of the distributive law. The product-free Lambek calculus enriched with conjunction only, however, is complete w.r.t. L-models (Buszkowski) as well as R-models (Andréka and Mikulás). The situation with disjunction turns out to be the opposite: we prove that the product-free Lambek calculus enriched with disjunction only is incomplete w.r.t. L-models as well as R-models. If the empty premises are allowed, the product-free Lambek calculus enriched with conjunction only is still complete w.r.t. L-models but in which the empty word is allowed. Both versions are decidable (PSPACE-complete in fact). Adding the multiplicative unit to represent explicitly the empty word within the L-model paradigm changes the situation in a completely unexpected way. Namely, we prove undecidability for any L-sound extension of the Lambek calculus with conjunction and with the unit, whenever this extension includes certain L-sound rules for the multiplicative unit, to express the natural algebraic properties of the empty word. Moreover, we obtain undecidability for a small fragment with only one implication, conjunction, and the unit, obeying these natural rules. This proof proceeds by the encoding of two-counter Minsky machines.
We consider the quantifier-free languages, Bc and Bc°, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of Rn (n ≥ 2) and, additionally, over the regular closed semilinear sets of Rn. The resulting logics are examples of formalisms that have recently been proposed in the Artificial Intelligence literature under the rubric Qualitative Spatial Reasoning. We prove that the satisfiability problem for Bc is undecidable over the regular closed semilinear sets in all dimensions greater than 1, and that the satisfiability problem for Bc and Bc° is undecidable over both the regular closed sets and the regular closed semilinear sets in the Euclidean plane. However, we also prove that the satisfiability problem for Bc° is NP-complete over the regular closed sets in all dimensions greater than 2, while the corresponding problem for the regular closed semilinear sets is ExpTime-complete. Our results show, in particular, that spatial reasoning is much harder over Euclidean spaces than over arbitrary topological spaces.
It is well-known that the Dolev–Yao adversary is a powerful adversary. Besides acting as the network, intercepting, decomposing, composing and sending messages, he can remember as much information as he needs. That is, his memory is unbounded. We recently proposed a weaker Dolev–Yao like adversary, which also acts as the network, but whose memory is bounded. We showed that this Bounded Memory Dolev–Yao adversary, when given enough memory, can carry out many existing protocol anomalies. In particular, the known anomalies arise for bounded memory protocols, where although the total number of sessions is unbounded, there are only a bounded number of concurrent sessions and the honest participants of the protocol cannot remember an unbounded number of facts or an unbounded number of nonces at a time. This led us to the question of whether it is possible to infer an upper-bound on the memory required by the Dolev–Yao adversary to carry out an anomaly from the memory restrictions of the bounded protocol. This paper answers this question negatively (Theorem 8).
Filtration is a standard tool for establishing the finite model property of modal logics. We consider logics and classes of frames that admit filtration, and identify some operations on them that preserve this property. In particular, the operation of adding the inverse or the transitive closure of a relation is shown to be safe in this sense. These results are then used to prove that every regular grammar logic with converse admits filtration. We present filtration constructions for right-linear and left-linear grammar logics. We also give a simple example of a grammar modal logic that is undecidable and hence does not admit filtration.
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called “Lambek’s restriction,” that is, the antecedent of any provable sequent should be non-empty. In this paper we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek’s restriction. We present several versions of the Lambek calculus extended with exponential modalities and prove that those extensions are undecidable, even if we take only one of the two divisions provided by the Lambek calculus.
A model for organizing cargo transportation between two node stations connected by a railway line which contains a certain number of intermediate stations is considered. The movement of cargo is in one direction. Such a situation may occur, for example, if one of the node stations is located in a region which produce raw material for manufacturing industry located in another region, and there is another node station. The organization of freight traﬃc is performed by means of a number of technologies. These technologies determine the rules for taking on cargo at the initial node station, the rules of interaction between neighboring stations, as well as the rule of distribution of cargo to the ﬁnal node stations. The process of cargo transportation is followed by the set rule of control. For such a model, one must determine possible modes of cargo transportation and describe their properties. This model is described by a ﬁnite-dimensional system of diﬀerential equations with nonlocal linear restrictions. The class of the solution satisfying nonlocal linear restrictions is extremely narrow. It results in the need for the “correct” extension of solutions of a system of diﬀerential equations to a class of quasi-solutions having the distinctive feature of gaps in a countable number of points. It was possible numerically using the Runge–Kutta method of the fourth order to build these quasi-solutions and determine their rate of growth. Let us note that in the technical plan the main complexity consisted in obtaining quasi-solutions satisfying the nonlocal linear restrictions. Furthermore, we investigated the dependence of quasi-solutions and, in particular, sizes of gaps (jumps) of solutions on a number of parameters of the model characterizing a rule of control, technologies for transportation of cargo and intensity of giving of cargo on a node station.
Let k be a field of characteristic zero, let G be a connected reductive algebraic group over k and let g be its Lie algebra. Let k(G), respectively, k(g), be the field of k- rational functions on G, respectively, g. The conjugation action of G on itself induces the adjoint action of G on g. We investigate the question whether or not the field extensions k(G)/k(G)^G and k(g)/k(g)^G are purely transcendental. We show that the answer is the same for k(G)/k(G)^G and k(g)/k(g)^G, and reduce the problem to the case where G is simple. For simple groups we show that the answer is positive if G is split of type A_n or C_n, and negative for groups of other types, except possibly G_2. A key ingredient in the proof of the negative result is a recent formula for the unramified Brauer group of a homogeneous space with connected stabilizers. As a byproduct of our investigation we give an affirmative answer to a question of Grothendieck about the existence of a rational section of the categorical quotient morphism for the conjugating action of G on itself.
Let G be a connected semisimple algebraic group over an algebraically closed field k. In 1965 Steinberg proved that if G is simply connected, then in G there exists a closed irreducible cross-section of the set of closures of regular conjugacy classes. We prove that in arbitrary G such a cross-section exists if and only if the universal covering isogeny Ĝ → G is bijective; this answers Grothendieck's question cited in the epigraph. In particular, for char k = 0, the converse to Steinberg's theorem holds. The existence of a cross-section in G implies, at least for char k = 0, that the algebra k[G]G of class functions on G is generated by rk G elements. We describe, for arbitrary G, a minimal generating set of k[G]G and that of the representation ring of G and answer two Grothendieck's questions on constructing generating sets of k[G]G. We prove the existence of a rational (i.e., local) section of the quotient morphism for arbitrary G and the existence of a rational cross-section in G (for char k = 0, this has been proved earlier); this answers the other question cited in the epigraph. We also prove that the existence of a rational section is equivalent to the existence of a rational W-equivariant map T- - - >G/T where T is a maximal torus of G and W the Weyl group.