Base-based Model Checking for Multi-Agent Only Believing (long version)
We present a novel semantics for the language of multi-agent only believing exploiting belief bases, and show how to use it for automatically checking formulas of this language and of its dynamic extension with private belief expansion operators. We provide a PSPACE algorithm for model checking relying on a reduction to QBF and alternative dedicated algorithm relying on the exploration of the state space. We present an implementation of the QBF-based algorithm and some experimental results on computation time in a concrete example.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Exploiting Belief Bases for Building Rich Epistemic Structures
We introduce a semantics for epistemic logic exploiting a belief base abstraction. Differently from existing Kripke-style semantics for epistemic logic in which the notions of possible world and epistemic alternative are…
On the Computational Complexity of Model Checking for Dynamic Epistemic Logic with S5 Models
Dynamic epistemic logic (DEL) is a logical framework for representing and reasoning about knowledge change for multiple agents. An important computational task in this framework is the model checking problem, which has b…
Model Checking for Closed-Loop Robot Reactive Planning
In this paper, we show how model checking can be used to create multi-step plans for a differential drive wheeled robot so that it can avoid immediate danger. Using a small, purpose built model checking algorithm in situ…
Autonomous VehiclesmodelTrajectory PlanningTwo Stage Transformer Model for COVID-19 Fake News Detection and Fact Checking
The rapid advancement of technology in online communication via social media platforms has led to a prolific rise in the spread of misinformation and fake news. Fake news is especially rampant in the current COVID-19 pan…
Fact CheckingFake News DetectionMisinformationNatural Language InferenceTurn-based Multi-Agent Reinforcement Learning Model Checking
In this paper, we propose a novel approach for verifying the compliance of turn-based multi-agent reinforcement learning (TMARL) agents with complex requirements in stochastic multiplayer games. Our method overcomes the …
modelMulti-agent Reinforcement Learningreinforcement-learningReinforcement Learning