Author name cluster
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
FLAP Journal 2025 Journal Article
We give some characterizations of the class of intuitionistic predicate Kripke frames validating the Kuroda formula. We, first, prove that the Kuroda formula does not define a class of frames definable by a classical first-order sentence and, second, establish a criterion for countable frames to validate this formula.
TCS Journal 2022 Journal Article
We prove that branching-time temporal logics CTL and CT L ⁎ are polynomial-time embeddable into their single-variable fragments. It follows that satisfiability for CTL and CT L ⁎, and therefore also for alternating-time temporal logics ATL and ATL ⁎, in languages with one propositional variable is as algorithmically hard as satisfiability for the full logic: EXPTIME-complete for CTL and ATL, and 2EXPTIME-complete for CT L ⁎ and ATL ⁎. We discuss applicability of the technique used in the proofs to other modal and temporal logics, including propositional dynamic, epistemic, and temporal-epistemic logics, as well as many-dimensional and first-order modal and temporal logics.
AAMAS Conference 2009 Conference Paper
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). General Terms Theory