A Model Checker for Epistemic Hybrid Automata Using Constraints Logic Programming
جاري التحميل...
التاريخ
المؤلفين
عنوان الدورية
ردمد الدورية
عنوان المجلد
الناشر
International Journal of Computer Science and Information Technologies
خلاصة
The idea of epistemic hybrid automata goes around how a set of agents interact by sharing their knowledge using synchronized events. Each agent takes his decision according to the gained knowledge from the interacting agents, in a previous work, we showed how to formally model systems in epistemic hybrid automata by extending the definition of hybrid automata with epistemic notations. Additionally, we presented a formal specification language to specify the requirements of those systems which are modeled using epistemic hybrid automata. In this paper, we present a model checker for epistemic hybrid automata. As far as we know no research presented a model checker for epistemic hybrid automata. The model checker allows us to reason about the dynamical behaviors of systems as well as the satisfaction of several epistemic properties. The proposed model checker is implemented using mathematical intervals in Constraints logic programming. As far as we know no research tried to present a model checking for EPH, no further work reported in this area, to this end this paper aims to present a model checking for EPH using CLP to verify systems that reason about knowledge with time constraints.