Research map / Vision-language and multimodal / Human and embodied modeling

A Modal Logic of Optimality (Student Abstract)

AAAI 2025 · Vision-language and multimodal › Human and embodied modeling · approach: Abstract visual reasoning benchmarks · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Introduces OPT, a modal logic of optimality whose semantics quantify over optimal reward-maximizing paths in reward-weighted transition systems, and proves it is a normal modal logic and checks several standard axioms (D holds, T fails, 4 holds).

Problem

Optimality has no formal logic treatment despite its central role in AI; existing modal/temporal logics (MTL0, DCTL) lack a dedicated optimality operator.

Approach

Defines a unary modal operator □φ ("it is optimal that φ") true at a state iff φ eventually holds forever on all reward-maximizing paths from that state, placing optimality as the sole primitive operator on top of CTL-style path semantics.

Key results

• Proves OPT is a normal modal logic: necessitation rule (Lemma 1) and K axiom (Lemma 2) hold.
• Proves the D axiom holds in OPT (Lemma 3), using that the set of optimal paths is nonempty for finite state sets.
• Shows the T axiom fails via a two-state counterexample (Lemma 4) and proves the 4 axiom holds (Lemma 5).

Surprising findings

• The T axiom (□φ → φ) fails for optimality, contrary to the authors' linguistic expectation that 'optimal φ' implies φ is not guaranteed at the current state.

Limitations

• No full axiomatization, proof theory, or soundness/completeness results yet (C4, B, 5 only hypothesized).
• Semantics handles infinite-path reward divergence with an ad hoc stopgap (reward set to 0), which may not be computable.
• Applications to AI, ethics and planning are discussed only as proposals without implementation or empirical evaluation.

Experimental setup

Baselines: MTL0 DCTL

Builds on: CTL Markov Temporal Logic (MTL0) Discounted Computational Tree Logic (DCTL)

Closest papers by meaning

• On the Expressivity of Objective-Specification Formalisms in Reinforcement Learning (ICLR 2024 · similarity 0.84)
• Minimal Change in Modal Logic S5 (AAAI 2025 · similarity 0.83)
• Reward-Respecting Subtasks for Model-Based Reinforcement Learning (Abstract Reprint) (AAAI 2024 · similarity 0.82)
• Beyond Scalar Rewards: An Axiomatic Framework for Lexicographic MDPs (NeurIPS 2025 · similarity 0.82)
• Reinforcement Learning with LTL and $\omega$-Regular Objectives via Optimality-Preserving Translation to Average Rewards (NeurIPS 2024 · similarity 0.82)
• Step-by-Step Optimization-like Reasoning in LLMs over Expanding Search Spaces (NeurIPS 2026 · similarity 0.82)