Showing 1–14 of 14 results for author: Shkatov, D

Algorithmic properties of QK4.3 and QS4.3

Authors: M. Rybakov, D. Shkatov

Abstract: We prove that predicate modal logics QK4.3 and QS4.3 are undecidable in languages with two individual variables, one modandic predicate letter, and one proposition letter. We prove that predicate modal logics QK4.3 and QS4.3 are undecidable in languages with two individual variables, one modandic predicate letter, and one proposition letter. △ Less

Submitted 6 July, 2023; originally announced July 2023.

Comments: Smirnov Readings, 2021, Moscow

Algorithmic properties of first-order modal logics of linear Kripke frames in restricted languages

Authors: Mikhail Rybakov, Dmitry Shkatov

Abstract: We study the algorithmic properties of first-order monomodal logics of frames $\langle \mathbb{N}, \leq \rangle$, $\langle \mathbb{N}, < \rangle$, $\langle \mathbb{Q}, \leq \rangle$, $\langle \mathbb{Q}, < \rangle$, $\langle \mathbb{R}, \leq \rangle$, $\langle \mathbb{R}, < \rangle$, as well as some related logics, in languages with restrictions on the number of individual variables as well as the… ▽ More We study the algorithmic properties of first-order monomodal logics of frames $\langle \mathbb{N}, \leq \rangle$, $\langle \mathbb{N}, < \rangle$, $\langle \mathbb{Q}, \leq \rangle$, $\langle \mathbb{Q}, < \rangle$, $\langle \mathbb{R}, \leq \rangle$, $\langle \mathbb{R}, < \rangle$, as well as some related logics, in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We show that the logics of frames based on $\mathbb{N}$ are $Π^1_1$-hard -- thus, not recursively enumerable -- in languages with two individual variables, one monadic predicate letter and one proposition letter. We also show that the logics of frames based on $\mathbb{Q}$ and $\mathbb{R}$ are $Σ^0_1$-hard in languages with the same restrictions. Similar results are obtained for a number of related logics. △ Less

Submitted 25 May, 2021; originally announced May 2021.

Recursive enumerability and elementary frame definability in predicate modal logic

Authors: Mikhail Rybakov, Dmitry Shkatov

Abstract: We investigate the relationship between recursive enumerability and elementary frame definability in first-order predicate modal logic. On the one hand, it is well-known that every first-order predicate modal logic complete with respect to an elementary class of Kripke frames, i.e., a class of frames definable by a classical first-order formula, is recursively enumerable. On the other, numerous ex… ▽ More We investigate the relationship between recursive enumerability and elementary frame definability in first-order predicate modal logic. On the one hand, it is well-known that every first-order predicate modal logic complete with respect to an elementary class of Kripke frames, i.e., a class of frames definable by a classical first-order formula, is recursively enumerable. On the other, numerous examples are known of predicate modal logics, based on `natural' propositional modal logics with essentially second-order Kripke semantics, that are either not recursively enumerable or Kripke incomplete. This raises the question of whether every Kripke complete, recursively enumerable predicate modal logic can be characterized by an elementary class of Kripke frames. We answer this question in the negative, by constructing a normal predicate modal logic which is Kripke complete, recursively enumerable, but not complete with respect to an elementary class of frames. We also present an example of a normal predicate modal logic that is recursively enumerable, Kripke complete, and not complete with respect to an elementary class of rooted frames, but is complete with respect to an elementary class of frames that are not rooted. △ Less

Submitted 20 December, 2019; v1 submitted 21 November, 2019; originally announced November 2019.

MSC Class: 03B45; 03D25

Complexity of the universal theory of bounded residuated distributive lattice-ordered groupoids

Authors: Dmitry Shkatov, C. J. Van Alten

Abstract: We prove that the universal theory and the quasi-equational theory of bounded residuated distributive lattice-orderegroupoids are both EXPTIME-complete. Similar results areproven for bounded distributive lattices with a unary or binary operator and for some special classes of bounded residuated distributive lattice-ordered groupoids. We prove that the universal theory and the quasi-equational theory of bounded residuated distributive lattice-orderegroupoids are both EXPTIME-complete. Similar results areproven for bounded distributive lattices with a unary or binary operator and for some special classes of bounded residuated distributive lattice-ordered groupoids. △ Less

Submitted 12 October, 2019; originally announced October 2019.

MSC Class: 06F99; 06D99; 03G25

Journal ref: Algebra Universalis, 80(3), 2019, article 36

Complexity of finite-variable fragments of propositional modal logics of symmetric frames

Authors: Mikhail Rybakov, Dmitry Shkatov

Abstract: While finite-variable fragments of the propositional modal logic S5--complete with respect to reflexive, symmetric and transitive frames--are polynomial-time decidable, the restriction to finite-variable formulas for logics of reflexive and transitive frames yields fragments that remain "intractable." The role of the symmetry condition in this context has not been investigated. We show that symmet… ▽ More While finite-variable fragments of the propositional modal logic S5--complete with respect to reflexive, symmetric and transitive frames--are polynomial-time decidable, the restriction to finite-variable formulas for logics of reflexive and transitive frames yields fragments that remain "intractable." The role of the symmetry condition in this context has not been investigated. We show that symmetry either by itself or in combination with reflexivity produces logics that behave just like logics of reflexive and transitive frames, i.e. their finite-variable fragments remain intractable, namely PSPACE-hard. This raises the question of where exactly the borderline lies between modal logics whose finite-variable fragments are tractable and the rest. △ Less

Submitted 5 October, 2019; originally announced October 2019.

MSC Class: 03B45

Journal ref: Logic Journal of the IGPL, Volume 27, Issue 1, February 2019, Pages 60-68

Complexity and expressivity of propositional dynamic logics with finitely many variables

Authors: Mikhail Rybakov, Dmitry Shkatov

Abstract: We investigate the complexity of satisfiability for finite-variable fragments of propositional dynamic logics. We consider three formalisms belonging to three representative complexity classes, broadly understood,---regular PDL, which is EXPTIME-complete, PDL with intersection, which is 2EXPTIME-complete, and PDL with parallel composition, which is undecidable. We show that, for each of these logi… ▽ More We investigate the complexity of satisfiability for finite-variable fragments of propositional dynamic logics. We consider three formalisms belonging to three representative complexity classes, broadly understood,---regular PDL, which is EXPTIME-complete, PDL with intersection, which is 2EXPTIME-complete, and PDL with parallel composition, which is undecidable. We show that, for each of these logics, the complexity of satisfiability remains unchanged even if we only allow as inputs formulas built solely out of propositional constants, i.e. without propositional variables. Moreover, we show that this is a consequence of the richness of the expressive power of variable-free fragments: for all the logics we consider, such fragments are as semantically expressive as entire logics. We conjecture that this is representative of PDL-style, as well as closely related, logics. △ Less

Submitted 18 January, 2019; originally announced January 2019.

Journal ref: Logic Journal of the IGPL, 26(5), 2018, pp. 539--547

Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables

Authors: Mikhail Rybakov, Dmitry Shkatov

Abstract: We show that Branching-time temporal logics CTL and CTL*, as well as Alternating-time temporal logics ATL and ATL*, are as semantically expressive in the language with a single propositional variable as they are in the full language, i.e., with an unlimited supply of propositional variables. It follows that satisfiability for CTL, as well as for ATL, with a single variable is EXPTIME-complete, whi… ▽ More We show that Branching-time temporal logics CTL and CTL*, as well as Alternating-time temporal logics ATL and ATL*, are as semantically expressive in the language with a single propositional variable as they are in the full language, i.e., with an unlimited supply of propositional variables. It follows that satisfiability for CTL, as well as for ATL, with a single variable is EXPTIME-complete, while satisfiability for CTL*, as well as for ATL*, with a single variable is 2EXPTIME-complete,--i.e., for these logics, the satisfiability for formulas with only one variable is as hard as satisfiability for arbitrary formulas. △ Less

Submitted 18 January, 2019; v1 submitted 22 October, 2018; originally announced October 2018.

Comments: Prefinal version of the published paper

Journal ref: Bernd Fischer and Tarmo Uustalu (eds.) Theoretical Aspects of Computing -- ICTAC 2018. Lecture Notes in Computer Science,Vol. 11187, Springer 2018, pp. 396--414

Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter

Authors: Mikhail Rybakov, Dmitry Shkatov

Abstract: 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… ▽ More 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 fragment with a single monadic predicate letter, without constants and equality, is undecidable, regardless of whether we consider semantics with expanding or constant domains. These include all sublogics of QKTB, QGL, and QGrz -- among them, QK, QT, QKB, QD, QK4, and QS4. △ Less

Submitted 12 June, 2022; v1 submitted 15 June, 2017; originally announced June 2017.

Comments: Corrected version of the paper published in Studia Logica, 107(2), 695-717 (2019). doi:10.1007/s11225-018-9815-7.},doi:10.1007/s11225-018-9815-7

MSC Class: 03B45

Journal ref: Studia Logica, 107(2), 2019, 695-717

On complexity of propositional Linear-time Temporal Logic with finitely many variables

Authors: Mikhail Rybakov, Dmitry Shkatov

Abstract: It is known [DemriSchnoebelen02] that both satisfiability and model-checking problems for propositional Linear-time Temporal Logic, LTL, with only a single propositional variable in the language are PSPACE-complete, which coincides with the complexity of these problems for LTL with an arbitrary number of propositional variables [SislaClarke85]. In the present paper, we show that the same result ca… ▽ More It is known [DemriSchnoebelen02] that both satisfiability and model-checking problems for propositional Linear-time Temporal Logic, LTL, with only a single propositional variable in the language are PSPACE-complete, which coincides with the complexity of these problems for LTL with an arbitrary number of propositional variables [SislaClarke85]. In the present paper, we show that the same result can be obtained by modifying the original proof of SPACE-hardness for LTL from [SislaClarke85]; i.e., we show how to modify the construction from [SislaClarke85] to model the computations of polynomially-space bound Turing machines using only formulas of one variable. We believe that our alternative proof of the results from [DemriSchnoebelen02] gives additional insight into the semantic and computational properties of LTL. △ Less

Submitted 25 November, 2018; v1 submitted 13 June, 2017; originally announced June 2017.

Journal ref: Prifinal version of the paper published in: In van Niekerk J., Haskins B. (eds). Proceedings of SAICSIT'18. ACM, 2018. pp. 313-316

Tableau-based decision procedure for the multi-agent epistemic logic with all coalitional operators for common and distributed knowledge

Authors: Mai Ajspur, Valentin Goranko, Dmitry Shkatov

Abstract: We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi-agent epistemic logic CMAEL(CD) with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for CMAEL(CD) and prove that satisfiability in such structures is equivalent to satisfiabilit… ▽ More We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi-agent epistemic logic CMAEL(CD) with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for CMAEL(CD) and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using that result, we design an incremental tableau-building procedure that eventually constructs a satisfying Hintikka structure for every satisfiable input set of formulae of CMAEL(CD) and closes for every unsatisfiable input set of formulae. △ Less

Submitted 25 January, 2012; originally announced January 2012.

Comments: Substantially extended and corrected version of arXiv:0902.2125. To appear in: Logic Journal of the IGPL, special issue on Formal Aspects of Multi-Agent Systems

MSC Class: 03B35; 03B42; 03B70; 68T27; 68T15 ACM Class: F.4.1; I.2.4

Tableau-based procedure for deciding satisfiability in the full coalitional multiagent epistemic logic

Authors: Valentin Goranko, Dmitry Shkatov

Abstract: We study the multiagent epistemic logic CMAELCD with operators for common and distributed knowledge for all coalitions of agents. We introduce Hintikka structures for this logic and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using this result, we design an incremental tableau based decision procedure for testing satisfiability in CMAELCD. We study the multiagent epistemic logic CMAELCD with operators for common and distributed knowledge for all coalitions of agents. We introduce Hintikka structures for this logic and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using this result, we design an incremental tableau based decision procedure for testing satisfiability in CMAELCD. △ Less

Submitted 12 February, 2009; originally announced February 2009.

Comments: Appeared in S. Artemov, A. Nerode (editors). Logical Foundations of Computer Science 2009. Lecture Notes in Computer Science. Vol. 5407. Springer, 2009. pp. 197--213

ACM Class: F.4.1; I.2.4; I.2.11

Tableau-based decision procedure for full coalitional multiagent temporal-epistemic logic of linear time

Authors: Valentin Goranko, Dmitry Shkatov

Abstract: We develop a tableau-based decision procedure for the full coalitional multiagent temporal-epistemic logic of linear time CMATEL(CD+LT). It extends LTL with operators of common and distributed knowledge for all coalitions of agents. The tableau procedure runs in exponential time, matching the lower bound obtained by Halpern and Vardi for a fragment of our logic, thus providing a complexity-optimal… ▽ More We develop a tableau-based decision procedure for the full coalitional multiagent temporal-epistemic logic of linear time CMATEL(CD+LT). It extends LTL with operators of common and distributed knowledge for all coalitions of agents. The tableau procedure runs in exponential time, matching the lower bound obtained by Halpern and Vardi for a fragment of our logic, thus providing a complexity-optimal decision procedure for CMATEL(CD+LT). △ Less

Submitted 21 November, 2019; v1 submitted 12 February, 2009; originally announced February 2009.

Comments: Proceedings of 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 09)

MSC Class: F.4.1; I.2.4; I.2.11 ACM Class: F.4.1; I.2.4; I.2.11

Journal ref: 8th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2009), Budapest, Hungary, May 10-15, 2009, Volume 2. IFAAMAS 2009, ISBN 978-0-9817381-7-8

Tableau-based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge

Authors: Valentin Goranko, Dmitry Shkatov

Abstract: We develop an incremental-tableau-based decision procedure for the multi-agent epistemic logic MAEL(CD) (aka S5_n (CD)), whose language contains operators of individual knowledge for a finite set Ag of agents, as well as operators of distributed and common knowledge among all agents in Ag. Our tableau procedure works in (deterministic) exponential time, thus establishing an upper bound for MAEL(… ▽ More We develop an incremental-tableau-based decision procedure for the multi-agent epistemic logic MAEL(CD) (aka S5_n (CD)), whose language contains operators of individual knowledge for a finite set Ag of agents, as well as operators of distributed and common knowledge among all agents in Ag. Our tableau procedure works in (deterministic) exponential time, thus establishing an upper bound for MAEL(CD)-satisfiability that matches the (implicit) lower-bound known from earlier results, which implies ExpTime-completeness of MAEL(CD)-satisfiability. Therefore, our procedure provides a complexity-optimal algorithm for checking MAEL(CD)-satisfiability, which, however, in most cases is much more efficient. We prove soundness and completeness of the procedure, and illustrate it with an example. △ Less

Submitted 29 August, 2008; originally announced August 2008.

Comments: To appear in the Proceedings of the 6th IEEE Conference on Software Engineering and Formal Methods (SEFM 2008)

ACM Class: F.4.1; I.2.4; I.2.11

Tableau-based decision procedures for logics of strategic ability in multi-agent systems

Authors: Valentin Goranko, Dmitry Shkatov

Abstract: We develop an incremental tableau-based decision procedures for the Alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we claim that our tableau is practically more efficient in the average case than other decision procedures for ATL known so far. Besides, the ease of its adaptation to variants of ATL demon… ▽ More We develop an incremental tableau-based decision procedures for the Alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we claim that our tableau is practically more efficient in the average case than other decision procedures for ATL known so far. Besides, the ease of its adaptation to variants of ATL demonstrates the flexibility of the proposed procedure. △ Less

Submitted 9 September, 2008; v1 submitted 15 March, 2008; originally announced March 2008.

Comments: To appear in ACM Transactions on Computational Logic. 48 pages

ACM Class: F.4.1; I.2.3; I.2.4; I.2.11