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

A. Rakib; H.M. Ul Haque

doi:10.1007/s11036-014-0520-0

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

A. Rakib, H.M. Ul Haque

University of Nottingham, Malaysia Campus

Research output: Contribution to journal › Article › peer-review

1 Citation (Scopus)

Abstract

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 language	English
Pages (from-to)	585-597
Number of pages	13
Journal	Mobile Networks and Applications
Volume	19
Issue number	5
Early online date	26 Sept 2014
DOIs	https://doi.org/10.1007/s11036-014-0520-0
Publication status	Published - Oct 2014
Externally published	Yes

Bibliographical note

Funder

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

Keywords

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

Access to Document

10.1007/s11036-014-0520-0

Cite this

@article{dd0c1db544c34ce38586f8187c2dad10,

title = "A Logical Framework for the Representation and Verification of Context-aware Agents",

abstract = "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.",

keywords = "Context-aware, Modal logic, Model checking, Multi-agent systems, Ontology",

author = "A. Rakib and {Ul Haque}, H.M.",

note = "{\textcopyright} 2014, Springer Science+Business Media New York.",

year = "2014",

month = oct,

doi = "10.1007/s11036-014-0520-0",

language = "English",

volume = "19",

pages = "585--597",

journal = "Mobile Networks and Applications",

issn = "1572-8153",

publisher = "Springer New York LLC",

number = "5",

}

TY - JOUR

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

AU - Rakib, A.

AU - Ul Haque, H.M.

PY - 2014/10

Y1 - 2014/10

N2 - 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.

AB - 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.

KW - Context-aware

KW - Modal logic

KW - Model checking

KW - Multi-agent systems

KW - Ontology

UR - http://www.scopus.com/inward/record.url?eid=2-s2.0-84912040974&partnerID=MN8TOARS

U2 - 10.1007/s11036-014-0520-0

DO - 10.1007/s11036-014-0520-0

M3 - Article

SN - 1572-8153

VL - 19

SP - 585

EP - 597

JO - Mobile Networks and Applications

JF - Mobile Networks and Applications

IS - 5

ER -

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

Abstract

Bibliographical note

Funder

Keywords

Access to Document

Other files and links

Fingerprint

Cite this