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 85
- Downloads 0
Real-Time H.264/AVC Entropy Encoder Hardware Architecture in Baseline Profile
In this paper, we present a new hardware architecture of an entropy encoder for an H.264/AVC video encoder. The proposed design aims to employ a parallel module at a pre-encoding stage to reduce a critical path. Addition...
Application of the Tabu Search Algorithm to Cryptography
Tabu search is a powerful algorithm that has been applied with great success to many difficult combinatorial problems. In this paper, we have designed and implemented a symmetrical encryption algorithm whose internal str...
Review of Cross-Platforms for Mobile Learning Application Development
Mobile learning management systems are very important for training purpose. But considering the present scenario, the learners are equipped with a number of mobile devices that run by different operating systems with div...
Virtual Observation System for Earth System Model: An Application to ACME Land Model Simulations
Investigating and evaluating physical-chemical-biological processes within an Earth system model (EMS) can be very challenging due to the complexity of both model design and software implementation. A virtual observation...
A Tri-Level Industry-Focused Learning Approach for Software Engineering Management
Most engineering classes in higher education rely heavily on the traditional lecture format, despite the fact that a number of investigations have shown that lectures, even when given by good lecturers, have limited succ...