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 92
- Downloads 0
Prolonging the Network Lifetime of WSN by using the Consumed Power Fairly Protocol
In wireless sensor networks (WSN), energy saving is always a key concern. Since nodes have limited power, some of them may use specific routes, thus leading to exhaustion of intermediate nodes. These nodes die, which res...
Semi Supervised Method for Detection of Ambiguous Word and Creation of Sense: Using WordNet
Machine Translation, Information Retrieval and Knowledge Acquisition are the three main applications of Word Sense Disambiguation (WSD). The sense of a target word can be identified from a dictionary using a ‘bag of word...
Analysis and Research of Communication Interrupt Fault for Shanghai Metro Data Transmission System
A line of Shanghai metro has been put into use for nearly fifteen years. There are three times extended during this time. The existing line’s data transmission system was modified over the last decades and has adopted ma...
A Study on Sentiment Analysis Techniques of Twitter Data
The entire world is transforming quickly under the present innovations. The Internet has become a basic requirement for everybody with the Web being utilized in every field. With the rapid increase in social network appl...
Software Bug Prediction using Machine Learning Approach
Software Bug Prediction (SBP) is an important issue in software development and maintenance processes, which concerns with the overall of software successes. This is because predicting the software faults in earlier phas...