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

Nous proposons un cadre logique pour la modélisation et la vérification des systèmes multi-agents sensibles au contexte. Nous étendons C T L ∗ avec des modalités de croyance et de communication, et la logique résultante OCRS nous permet de décrire un ensemble d'agents de raisonnement basés sur des règles avec des limites de temps, de mémoire et de communication. L'ensemble des règles utilisées pour modéliser un système souhaité est dérivé des ontologies OWL 2 RL. Nous fournissons une axiomatisation de la logique et prouvons qu'elle est solide et complète. Nous montrons comment le système de réécriture Maude peut être utilisé pour coder et vérifier les propriétés intéressantes des modèles OCRS en utilisant les techniques de vérification de modèle existantes.
Proponemos un marco lógico para modelar y verificar sistemas multiagente sensibles al contexto. Ampliamos C T L * con modalidades de creencia y comunicación, y la lógica resultante OCRS nos permite describir un conjunto de agentes de razonamiento basados en reglas con límite de tiempo, memoria y comunicación. El conjunto de reglas que se utilizan para modelar un sistema deseado se deriva de las ontologías OWL 2 RL. Proporcionamos una axiomatización de la lógica y demostramos que es sólida y completa. Mostramos cómo se puede utilizar el sistema de reescritura Maude para codificar y verificar propiedades interesantes de los modelos OCRS utilizando técnicas de verificación de modelos existentes.
We propose a logical framework for modelling and verifying context-aware multi-agent systems. We extend C T L ∗ 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.
نقترح إطارًا منطقيًا لنمذجة الأنظمة متعددة الوكلاء الواعية بالسياق والتحقق منها. نقوم بتوسيع CTL * مع طرق الاعتقاد والتواصل، ويسمح لنا المنطق الناتج عن OCRS بوصف مجموعة من عوامل التفكير القائمة على القواعد مع الالتزام بالوقت والذاكرة والتواصل. مجموعة القواعد المستخدمة لنمذجة الأنظمة المرغوبة مشتقة من أنطولوجيات OWL 2 RL. نقدم بديهية المنطق ونثبت أنه سليم وكامل. نوضح كيف يمكن استخدام نظام مود لإعادة الكتابة لتشفير والتحقق من الخصائص المثيرة للاهتمام لنماذج OCRS باستخدام تقنيات التحقق من النموذج الحالية.