Multi-Agent Systems (MASs) is the sub eld of Artificial Intelligence that aims at providing principles for building of complex systems involving several interacting agents. Specifying behaviors of MASs is a demanding task, especially when they are applied in safety critical applications. In such applications, the specifcation of the behavior has to be done carefully in order to avoid side effects that might bring unwanted behaviors or even disastrous. To tackle this challenge, formal techniques based on mathematical models of the system under design are helpful. An example of the of the formal techniques is to use a kind of Modal logis that is used to formally describe the Dynamic changes of MASs.
Usually, 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. Usually, agents interact within their environment based on sharing the knowledge. As a result of the interactions, agents gain knowledge over the time. Each agent interacts according to its own behavior that leads to gaining additional knowledge. However, hybrid automata lack to specify the changes of agent’s knowledge; that is the common knowledge or distributed knowledge between agents.
However, the formal model of hybrid automata does not al- low to reason about knowledge of agents. Thus, the main goal of this paper is to propose what is called epistemic hybrid automata to capture both continuous dynamics on one and reason about the knowledge of agents on the other hand. To achieve this goal, the paper extends hybrid automata with epistemic logic.
The paper shows the syntax and semantics of the proposed model. Additionally, The paper illustrates with examples the proposed methods to specify some properties.