scholarly journals Model Checking Multi-Agent Systems against LDLK Specifications

2017 ◽  
Author(s):  
Jeremy Kong ◽  
Alessio Lomuscio
Keyword(s):  
Model Checking ◽  
Common Knowledge ◽  
Source Model ◽  
Multi Agent System ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Knowledge States ◽  
Multi Agent ◽  
Epistemic Modalities ◽  
Alternating Automata

We define the logic LDLK, a formalism for specifying multi-agent systems. LDLK extends LDL with epistemic modalities, including common knowledge, for reasoning about the evolution of knowledge states of the agents in the system. We study the complexity of verifying a multi-agent system against LDLK specifications and show this to be in PSPACE. We give an algorithm for the practical verification of multi-agent systems specified in LDLK. We show that the model checking algorithm, based on alternating-automata and nFA, is amenable to symbolic implementation on OBDDs. We introduce MCMAS LDLK , an extension of the open-source model checker MCMAS, implementing the algorithm and discuss the experimental results obtained.

scholarly journals Modelling and verification of reconfigurable multi-agent systems

2021 ◽  
Vol 35 (2) ◽  
Author(s):  
Yehia Abd Alrahman ◽  
Nir Piterman
Keyword(s):  
Model Checking ◽  
Communication Protocols ◽  
Local State ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Robot Systems ◽  
Message Exchange ◽  
Multi Agent ◽  
Exchange Data ◽  
Multi Robot

AbstractWe propose a formalism to model and reason about reconfigurable multi-agent systems. In our formalism, agents interact and communicate in different modes so that they can pursue joint tasks; agents may dynamically synchronize, exchange data, adapt their behaviour, and reconfigure their communication interfaces. Inspired by existing multi-robot systems, we represent a system as a set of agents (each with local state), executing independently and only influence each other by means of message exchange. Agents are able to sense their local states and partially their surroundings. We extend ltl to be able to reason explicitly about the intentions of agents in the interaction and their communication protocols. We also study the complexity of satisfiability and model-checking of this extension.

scholarly journals Model Checking Temporal Epistemic Logic under Bounded Recall

2020 ◽  
Vol 34 (05) ◽  
pp. 7071-7078
Author(s):  
Francesco Belardinelli ◽  
Alessio Lomuscio ◽  
Emily Yu
Keyword(s):  
Model Checking ◽  
Incomplete Information ◽  
Epistemic Logic ◽  
Upper Bounds ◽  
Experimental Results ◽  
Model Checker ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Multi Agent ◽  
Bounded Recall

We study the problem of verifying multi-agent systems under the assumption of bounded recall. We introduce the logic CTLKBR, a bounded-recall variant of the temporal-epistemic logic CTLK. We define and study the model checking problem against CTLK specifications under incomplete information and bounded recall and present complexity upper bounds. We present an extension of the BDD-based model checker MCMAS implementing model checking under bounded recall semantics and discuss the experimental results obtained.

scholarly journals A Compositional Automata-based Approach for Model Checking Multi-Agent Systems

2008 ◽  
Vol 195 ◽  
pp. 133-149
Author(s):  
Mario Benevides ◽  
Carla Delgado ◽  
Carlos Pombo ◽  
Luis Lopes ◽  
Ricardo Ribeiro
Keyword(s):  
Model Checking ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Multi Agent

Evolutionary Computation as a Paradigm for Engineering Emergent Behaviour in Multi-Agent Systems

2011 ◽  
pp. 118-136 ◽  
Author(s):  
Robert E. Smith ◽  
Claudio Bonacina
Keyword(s):  
Evolutionary Computation ◽  
Multi Agent System ◽  
Multi Agent Systems ◽  
Agent System ◽  
Future Directions ◽  
Agent Based ◽  
Agent Systems ◽  
Emergent Behaviour ◽  
Shaping System ◽  
Multi Agent

In the multi-agent system (MAS) context, the theories and practices of evolutionary computation (EC) have new implications, particularly with regard to engineering and shaping system behaviors. Thus, it is important that we consider the embodiment of EC in “real” agents, that is, agents that involve the real restrictions of time and space within MASs. In this chapter, we address these issues in three ways. First, we relate the foundations of EC theory to MAS and consider how general interactions among agents fit within this theory. Second, we introduce a platform independent agent system to assure that our EC methods work within the generic, but realistic, constraints of agents. Finally, we introduce an agent-based system of EC objects. Concluding sections discuss implications and future directions.

scholarly journals Quantum Diffie–Hellman Extended to Dynamic Quantum Group Key Agreement for e-Healthcare Multi-Agent Systems in Smart Cities

Sensors ◽  
2020 ◽  
Vol 20 (14) ◽  
pp. 3940
Author(s):  
Vankamamidi S. Naresh ◽  
Moustafa M. Nasralla ◽  
Sivaranjani Reddi ◽  
Iván García-Magariño
Keyword(s):  
System Architecture ◽  
Key Agreement ◽  
Unitary Operation ◽  
Multi Agent System ◽  
Multi Agent Systems ◽  
Group Key ◽  
Group Key Agreement ◽  
Agent Systems ◽  
Diffie Hellman ◽  
Multi Agent

Multi-Agent Systems can support e-Healthcare applications for improving quality of life of citizens. In this direction, we propose a healthcare system architecture named smart healthcare city. First, we divide a given city into various zones and then we propose a zonal level three-layered system architecture. Further, for effectiveness we introduce a Multi-Agent System (MAS) in this three-layered architecture. Protecting sensitive health information of citizens is a major security concern. Group key agreement (GKA) is the corner stone for securely sharing the healthcare data among the healthcare stakeholders of the city. For establishing GKA, many efficient cryptosystems are available in the classical field. However, they are yet dependent on the supposition that some computational problems are infeasible. In light of quantum mechanics, a new field emerges to share a secret key among two or more members. The unbreakable and highly secure features of key agreement based on fundamental laws of physics allow us to propose a Quantum GKA (QGKA) technique based on renowned Quantum Diffie–Hellman (QDH). In this, a node acts as a Group Controller (GC) and forms 2-party groups with remaining nodes, establishing a QDH-style shared key per each two-party. It then joins these keys into a single group key by means of a XOR-operation, acting as a usual group node. Furthermore, we extend the QGKA to Dynamic QGKA (DQGKA) by adding join and leave protocol. Our protocol performance was compared with existing QGKA protocols in terms of Qubit efficiency (QE), unitary operation (UO), unitary operation efficiency (UOE), key consistency check (KCC), security against participants attack (SAP) and satisfactory results were obtained. The security analysis of the proposed technique is based on unconditional security of QDH. Moreover, it is secured against internal and external attack. In this way, e-healthcare Multi-Agent System can be robust against future quantum-based attacks.

Sign in / Sign up

Export Citation Format

Share Document