A Framework to Reason about the Knowledge of Agents in Continuous Dynamic Systems
Journal Title: International Journal of Advanced Computer Science & Applications - Year 2017, Vol 8, Issue 4
Abstract
Applying formal methods to a group of agents provides a precise and unambiguous definition of their behaviors, as well as verify properties of agents against implementations. Hybrid automaton is one of the formal approaches that are used by several works to model a group of agents. Several logics have been proposed, as extension of temporal logics to specify and hence verify those quantitative and qualitative properties of systems modeled by hybrid automaton. However, when it comes to agents, one needs to reason about the knowledge of other agents participating in the model. For this purpose, epistemic logic can be used to specify and reason about the knowledge of agents. But this logic assumes that the model of time is discrete. This paper proposes a novel framework that formally specifies and verifies the epistemic behaviors of agents within continuous dynamics. To do so, the paper first extends the hybrid automaton with knowledge. Second, the paper proposes a new logic that extends epistemic logic with quantitative real time requirement. Finally, the paper shows how to specify several properties that can be verified within our framework.
Authors and Affiliations
Ammar Mohammed, Ahmed M. Elmogy
Keywords
Related Articles
- EP ID EP258384
- DOI 10.14569/IJACSA.2017.080458
- Views 105
- Downloads 0
Statistical Implicative Similarity Measures for User-based Collaborative Filtering Recommender System
This paper proposes a new similarity measures for User-based collaborative filtering recommender system. The similarity measures for two users are based on the Implication intensity measures. It is called statistical imp...
2-D Object Recognition Approach using Wavelet Transform
Humans have supernatural ability to observe, analyze, and tell about the layout of the 3D world with the help of their natural visual system. But contrary to machine vision system, it remains a most difficult task to rec...
Exploring the Use of Digital Games as a Persuasive Tool in Teaching Islamic Knowledge for Muslim Children
Various digital games have been developed that focus on providing a sense of enjoyment and excitement for their players in order to be a modern tool for releasing stress or simply for pleasure. In recent years, digital g...
Comparison of Localization Free Routing Protocols in Underwater Wireless Sensor Networks
Underwater Wireless Sensor Network (UWSN) is newly developed branch of Wireless Sensor network (WSN). UWSN is used for exploration of underwater resources, oceanographic data collection, flood or disaster prevention, tac...
A Trapezoidal Cross-Section Stacked Gate FinFET with Gate Extension for Improved Gate Control
An improved trapezoidal pile gate bulk FinFET device is implemented with an extension in the gate for enhancing the performance. The novelty in the design is trapezoidal cross-section FinFET with stacked metal gate along...