arXiv subjects

Fengkui Ju

Publications and source records attributed to Fengkui Ju.

11 recordsLinked to original sources

arXiv2026

Representation theorems for actual and alpha powers over general concurrent game frames without assuming independence of agents

Concurrent game frames are a standard semantic framework for logics of strategic reasoning. Two notions of coalition power can be derived from such frames: alpha powers and actual powers. An alpha power of a coalition is a set of possible futures such that the coalition has an action that forces the resulting future to lie in that set. An actual power of a coalition is a set of possible futures satisfying the following condition: the coalition has an action such that (1) the action forces the resulting future to lie in the set, and (2) every future in the set is compatible with that action. Recent generalizations of concurrent game frames separate three structural assumptions built into the standard model: seriality, independence of agents, and determinism. This yields eight classes of general concurrent game frames. In this paper, we prove that for actual powers, the four classes of general concurrent game frames, where independence of agents is not assumed, are representable by four corresponding classes of neighborhood frames. Building on this result, we show that for alpha powers, the same four classes of general concurrent game frames are likewise representable by four corresponding classes of neighborhood frames.

cs.GT↗

arXiv2026

Representation theorems for actual and alpha powers over two-agent general concurrent game frames

One of the most well-known connections between modal logic and games is Pauly's representation theorem: that the induced powers of individuals and coalitions in a concurrent game frame correspond, in a precise sense, to a certain class of neighborhood models. The precise sense here is what is called \emph{alpha effectivity} (or \emph{alpha power}): the power of a coalition is characterized by the sets of states which it can ensure the outcome to lie in by taking some joint action. This definition is inherently monotonic, and, as pointed out by \cite{benthem_new_2019}, that fact can obscure relevant information about the power structure in the game: we don't know whether two sets a coalition has the power to enforce correspond to the same or different joint actions. An alternative is to characterise the power of a coalition by its \emph{actual powers} (called \emph{basic powers} in \cite{benthem_new_2019}): the set of sets of states where each corresponds to one joint action by the coalition and all possible joint actions by the other agents. It has recently been argued \cite{li_minimal_2025, li_completeness_2026} that standard concurrent game frames rely on three assumptions that in some cases may be too strong: seriality, independence of agents, and determinism. This gives a total of eight different classes of \emph{general} concurrent game frames. In this paper, assuming two agents, we prove that for actual powers, the eight classes of general concurrent game frames are representable by eight corresponding classes of neighborhood frames. Building on this result, we show that for alpha powers, the same eight classes of general concurrent game frames are likewise representable by eight corresponding classes of neighborhood frames. This generalizes a result in \cite{benthem_new_2019}. We also show that the two-agent actual characterization does not extend to arbitrary finite agent sets.

cs.GT↗

arXiv2025

Seven kinds of equivalent models for generalized coalition logics

Coalition Logic is an important logic in logical research on strategic reasoning. In two recent papers, Li and Ju argued that generally, concurrent game models, models of Coalition Logic, have three too strong assumptions: seriality, independence of agents, and determinism. They presented eight coalition logics based on eight classes of general concurrent game models, determined by which of the three assumptions are met. In this paper, we show that each of the eight sets of valid formulas of the eight logics is determined by six other kinds of models, that is, single-coalition-first action models, single-coalition-first actual neighborhood models, clear grand-coalition-first action models, clear single-coalition-first actual neighborhood models, tree-like grand-coalition-first action models, and tree-like single-coalition-first actual neighborhood models.

cs.LO↗

arXiv2024

Completeness of coalition logics with seriality, independence of agents, or determinism

Coalition Logic is a central logic in logical research on strategic reasoning. In a recent paper, Li and Ju argued that generally, models of Coalition Logic, concurrent game models, have three too strong assumptions: seriality, independence of agents, and determinism. They presented a Minimal Coalition Logic based on general concurrent game models, which do not have the three assumptions. However, when constructing coalition logics about strategic reasoning in special kinds of situations, we may want to keep some of the assumptions. Thus, studying coalition logics with some of these assumptions makes good sense. In this paper, we show the completeness of these coalition logics in a uniform way.

cs.GT↗

arXiv2024

Logic for conditional strong historical necessity in branching time and analyses of an argument for future determinism

In this paper, we present a logic for conditional strong historical necessity in branching time and apply it to analyze a nontheological version of Lavenham's argument for future determinism. Strong historical necessity is motivated from a linguistical perspective, and an example of it is ``If I had not gotten away, I must have been dead''. The approach of the logic is as follows. The agent accepts ontic rules concerning how the world evolves over time. She takes some rules as indefeasible, which determine acceptable timelines. When evaluating a sentence with conditional strong historical necessity, we introduce its antecedent as an indefeasible ontic rule and then check whether its consequent holds for all acceptable timelines. The argument is not sound by the logic.

cs.LO↗

arXiv2024

Completeness of two fragments of a logic for conditional strategic reasoning

Classical logics for strategic reasoning, such as Coalition Logic and Alternating-time Temporal Logic, formalize absolute strategic reasoning about the unconditional strategic abilities of agents to achieve their goals. Goranko and Ju, in two recent papers, introduced a Logic for Conditional Strategic Reasoning (CSR). However, its completeness is still an open problem. CSR has three featured operators, and one of them has the following reading: For some action of A that guarantees the achievement of her goal, B has an action to guarantee the achievement of his goal. This operator makes good sense when A is cooperating with B. The logic about this operator is called Logic for Cooperating Conditional Strategic Reasoning (CCSR). In this paper, we prove the completeness of two fragments of CCSR: the liability fragment and the ability fragment. The key ingredients of our proof approach include standard disjunctions, the validity-reduction condition of standard disjunctions, abstract game forms, and their realization, and the derivability-reduction condition of standard disjunctions. The approach has good potential to be applied to the completeness of CSR and other strategic logics.

cs.LO↗

arXiv2024

A minimal coalition logic

Coalition Logic is an important logic in logical studies of strategic reasoning, whose models are concurrent game models. In this paper, first, we systematically discuss three assumptions of concurrent game models and argue that they are too strong. The first is seriality; that is, every coalition always has an available joint action. The second is the independence of agents; that is, the merge of two available joint actions of two disjoint coalitions is always an available joint action of the union of the two coalitions. The third is determinism; that is, all available joint actions of the grand coalition always have a unique outcome. Second, we present a coalition logic based on general concurrent game models which do not have the three assumptions and show its completeness. This logic seems minimal for reasoning about coalitional powers.

cs.LO↗

arXiv2022

A logical theory for conditional weak ontic necessity based on context update

Weak ontic necessity is the ontic necessity expressed by ``should'' or ``ought to'' in English. An example of it is ``I should be dead by now''. A feature of this necessity is whether it holds does not have anything to do with whether its prejacent holds. In this paper, we present a logical theory for conditional weak ontic necessity based on context update. A context is a set of ordered defaults, determining expected possible states of the present world. Sentences are evaluated with respect to contexts. When evaluating the conditional weak ontic necessity with respect to a context, we first update the context with the antecedent, then check whether the consequent holds with respect to the updated context. The logic is complete. Our theory combines premise semantics and update semantics for conditionals.

cs.CL↗

arXiv2022

Historical/temporal necessities/possibilities, and a logical theory of them in branching time

In this paper, we do three kinds of work. First, we recognize four notions of necessity and two notions of possibility related to time flow, namely strong/weak historical/temporal necessities, as well as historical/temporal possibilities, which are motivated more from a linguistic perspective than from a philosophical one. Strong/weak historical necessities and historical possibility typically concern the possible futures of the present world, and strong/weak temporal necessities and temporal possibility concern possible timelines of alternatives of the present world. Second, we provide our approach to the six notions and present a logical theory of them in branching time. Our approach to the six notions is as follows. The agent has a system of ontic rules that determine expected timelines. She treats some ontic rules as undefeatable, determining accepted timelines. The domains of strong/weak historical necessities, respectively, consist of accepted and expected timelines passing through the present moment, and historical possibility is the dual of strong historical necessity. The domains of strong/weak temporal necessities, respectively, consist of accepted and expected timelines, and temporal possibility is the dual of strong temporal necessity. The logical theory has six operators: a last-moment operator, a next-moment operator, and four operators for the four notions of necessity. Formulas' evaluation contexts consist of a tree-like model representing a time flow, a context representing the agent's system of ontic rules, a timeline, and an instant. Third, we offer an axiomatic system for the logical theory and show its soundness and completeness.

cs.CL↗

arXiv2021

A Logic for Conditional Local Strategic Reasoning

We consider systems of rational agents who act and interact in pursuit of their individual and collective objectives. We study and formalise the reasoning of an agent, or of an external observer, about the expected choices of action of the other agents based on their objectives, in order to assess the reasoner's ability, or expectation, to achieve their own objective. To formalize such reasoning we extend Pauly's Coalition Logic with three new modal operators of conditional strategic reasoning, thus introducing the Logic for Local Conditional Strategic Reasoning ConStR. We provide formal semantics for the new conditional strategic operators in concurrent game models, introduce the matching notion of bisimulation for each of them, prove bisimulation invariance and Hennessy-Milner property for each of them, and discuss and compare briefly their expressiveness. Finally, we also propose systems of axioms for each of the basic operators of ConStR and for the full logic.

cs.GT↗

arXiv2017

A logic for temporal conditionals and a solution to the Sea Battle Puzzle

Temporal reasoning with conditionals is more complex than both classical temporal reasoning and reasoning with timeless conditionals, and can lead to some rather counter-intuitive conclusions. For instance, Aristotle's famous "Sea Battle Tomorrow" puzzle leads to a fatalistic conclusion: whether there will be a sea battle tomorrow or not, but that is necessarily the case now. We propose a branching-time logic LTC to formalise reasoning about temporal conditionals and provide that logic with adequate formal semantics. The logic LTC extends the Nexttime fragment of CTL*, with operators for model updates, restricting the domain to only future moments where antecedent is still possible to satisfy. We provide formal semantics for these operators that implements the restrictor interpretation of antecedents of temporalized conditionals, by suitably restricting the domain of discourse. As a motivating example, we demonstrate that a naturally formalised in our logic version of the `Sea Battle' argument renders it unsound, thereby providing a solution to the problem with fatalist conclusion that it entails, because its underlying reasoning per cases argument no longer applies when these cases are treated not as material implications but as temporal conditionals. On the technical side, we analyze the semantics of LTC and provide a series of reductions of LTC-formulae, first recursively eliminating the dynamic update operators and then the path quantifiers in such formulae. Using these reductions we obtain a sound and complete axiomatization for LTC, and reduce its decision problem to that of the modal logic KD.

cs.LO↗