Modeling and verifying context-aware non-monotonic reasoning agents

Rakib, Abdur; Haque, Hafiz Mahfooz Ul

Abstract

© 2015 IEEE. This paper complements our previous work on formal modeling of resource-bounded context-aware systems, which handle inconsistent context information using defeasible reasoning, by focusing on automated analysis and verification. A case study demonstrates how model checking techniques can be used to formally analyze quantitative and qualitative properties of a context-aware system based on message passing among agents. The behavior (semantics) of the system is modeled by a term rewriting system and the desired properties are expressed as LTL formulas. The Maude LTL model checker is used to perform automated analysis of the system and verify non-conflicting context information guarantees it provides.

• Presentation Conference Type: Conference Paper (published)
• Conference Name: 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015
• Start Date: Sep 21, 2015
• End Date: Sep 23, 2015
• Acceptance Date: Jul 24, 2015
• Publication Date: Nov 30, 2015
• Deposit Date: Jun 16, 2017
• Publicly Available Date: Jun 20, 2017
• Peer Reviewed: Peer Reviewed
• Pages: 61-69
• Book Title: 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)
• DOI: https://doi.org/10.1109/MEMCOD.2015.7340471
• Keywords: formal modeling, model checking, context-aware; systems, rule-based reasoning, defeasible reasoning, multi-agent systems
• Public URL: https://uwe-repository.worktribe.com/output/802350
• Publisher URL: http://dx.doi.org/10.1109/MEMCOD.2015.7340471
• Related Public URLs: http://ieeexplore.ieee.org/document/7340471/?reload=true
• Additional Information: Title of Conference or Conference Proceedings : The 13th ACM-IEEE International Conference on Formal Methods and Models for System Design
• Contract Date: Jun 16, 2017