A Logical Framework for the Representation and Verification of Context-aware Agents

A. Rakib, H.M. Ul Haque

Research output: Contribution to journalArticlepeer-review


We propose a logical framework for modelling and verifying context-aware multi-agent systems. We extend CTL∗ with belief and communication modalities, and the resulting logic 𝓛OCRS allows us to describe a set of rule-based reasoning agents with bound on time, memory and communication. The set of rules which are used to model a desired systems is derived from OWL 2 RL ontologies. We provide an axiomatization of the logic and prove it is sound and complete. We show how Maude rewriting system can be used to encode and verify interesting properties of 𝓛OCRS models using existing model checking techniques.
Original languageEnglish
Pages (from-to)585-597
Number of pages13
JournalMobile Networks and Applications
Issue number5
Early online date26 Sept 2014
Publication statusPublished - Oct 2014
Externally publishedYes

Bibliographical note

© 2014, Springer Science+Business Media New York.


This work is partially supported by the Faculty of Science Pump Priming & Equipment Research Fund at the University of Nottingham Malaysia Campus.


  • Context-aware
  • Modal logic
  • Model checking
  • Multi-agent systems
  • Ontology


Dive into the research topics of 'A Logical Framework for the Representation and Verification of Context-aware Agents'. Together they form a unique fingerprint.

Cite this