Epistemic Hybrid Tree Logic
Ammar Mohamed, Rana Mohamed, Hesham Ahmed Hefny · 2015
In multi-agent systems, reasoning about the behavior of each agent is influenced by its acquired knowledge at each point of time. Each agent has two types of behaviors, a dynamic behavior representing its continuous evolution in the environment and a discrete behavior representing how the agent moves from mod to mod. The later kinds of behaviors can be modeled using hybrid automata. However, the formal model of hybrid automata does not allow to reason about knowledge of agents. Thus, the main goal of this paper is to present a novel model that allows us to represent the continuous dynamics behavior of agents on one hand, and to reason about knowledge of agents on the other hand. To achieve this goal, the paper introduces epistemic hybrid automata that extend hybrid automata with epistemic logic. Additionally, the formal semantics of the proposed model allows us to propose an epistemic hybrid tree logic in order to specify and hence to verify properties of agents within the model of epistemic hybrid automata logic.