Bounded situation calculus action theories
From MaRDI portal
Publication:286407
DOI10.1016/J.ARTINT.2016.04.006zbMATH Open1357.68227arXiv1509.02012OpenAlexW2228999052MaRDI QIDQ286407FDOQ286407
Yves Lespérance, Fabio Patrizi, Giuseppe De Giacomo
Publication date: 20 May 2016
Published in: Artificial Intelligence (Search for Journal in Brave)
Abstract: In this paper, we investigate bounded action theories in the situation calculus. A bounded action theory is one which entails that, in every situation, the number of object tuples in the extension of fluents is bounded by a given constant, although such extensions are in general different across the infinitely many situations. We argue that such theories are common in applications, either because facts do not persist indefinitely or because the agent eventually forgets some facts, as new ones are learnt. We discuss various classes of bounded action theories. Then we show that verification of a powerful first-order variant of the mu-calculus is decidable for such theories. Notably, this variant supports a controlled form of quantification across situations. We also show that through verification, we can actually check whether an arbitrary action theory maintains boundedness.
Full work available at URL: https://arxiv.org/abs/1509.02012
Recommendations
- Incorporating action models into the situation calculus
- A unifying action calculus
- Logic, Probability and Action: A Situation Calculus Perspective
- Knowledge, action, and Cartesian situations in the situation calculus
- scientific article; zbMATH DE number 1523045
- Representing actions in logic programs and default theories a situation calculus approach
- Progression and verification of situation calculus agents with bounded beliefs
- scientific article; zbMATH DE number 1305385
- On the role of possibility in action execution and knowledge in the situation calculus
Knowledge representation (68T30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in artificial intelligence (68T27)
Cites Work
- ConGolog, a concurrent programming language based on the situation calculus
- Using Theorem Proving to Verify Properties of Agent Programs
- GOLOG: A logic programming language for dynamic domains
- Programming Multi-Agent Systems in AgentSpeak usingJason
- Nonmonotonic causal theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Propositional dynamic logic of regular programs
- A lattice-theoretical fixpoint theorem and its applications
- Reasoning about rational agents
- Title not available (Why is that?)
- Title not available (Why is that?)
- A logic-based calculus of events
- Title not available (Why is that?)
- Elements of finite model theory.
- Alternation
- Planning for temporally extended goals.
- How to progress a database
- TALplanner: A temporal logic based forward chaining planner
- From situation calculus to fluent calculus: State update axioms as a solution to the inferential frame problem
- MetateM: An introduction
- A verification framework for agent programming with declarative goals
- Intention is choice with commitment
- The logic of knowledge bases
- Verification on infinite structures.
- Title not available (Why is that?)
- Verification of agent-based artifact systems
- The Cognitive Agents Specification Language and Verification Environment
- Some contributions to the metatheory of the situation calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Representing action and change by logic programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Iterated belief change in the situation calculus
- Knowledge, action, and the frame problem
- Dynamic epistemic logic
- Property persistence in the situation calculus
Cited In (11)
- Lifted model checking for relational MDPs
- Action Theories over Generalized Databases with Equality Constraints
- Progression and verification of situation calculus agents with bounded beliefs
- Propositional epistemic logics with quantification over agents of knowledge
- The delay and window size problems in rule-based stream reasoning
- Verification of agent navigation in partially-known environments
- Knowledge-based programs as succinct policies for partially observable domains
- A Three-Value Abstraction Technique for the Verification of Epistemic Properties in Multi-agent Systems
- Situation calculus for controller synthesis in manufacturing systems with first-order state representation
- First-order \(\mu\)-calculus over generic transition systems and applications to the situation calculus
- Non-terminating processes in the situation calculus
Uses Software
This page was built for publication: Bounded situation calculus action theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286407)
