| 1. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
A coordination protocol language for power grid operation control
- 2019
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 109
-
Tidskriftsartikel (refereegranskat)abstract
- Future power distribution grids will comprise a large number of components, each potentially able to carry out operations autonomously. Clearly, in order to ensure safe operation of the grid, individual operations must be coordinated among the different components. Since operation safety is a global property, modelling component coordination typically involves reasoning about systems at a global level. In this paper, we propose a language for specifying grid operation control protocols from a global point of view. In our model, operation control is yielded in communications driven by both the grid topology and by state-based information, features captured by novel language principles previously unexplored. We show how the global specifications can be used to automatically generate local controllers of individual components, and that the distributed implementation yielded by such controllers operationally corresponds to the global specification. We showcase our development by modelling a fault management scenario in power grids. (C) 2019 Elsevier Inc. All rights reserved.
|
|
| 2. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
A PO Characterisation ofReconfiguration
- 2022
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349.
-
Konferensbidrag (refereegranskat)abstract
- We consider partial order semantics of concurrent systems in which local reconfigurations may have global side effects. That is, local changes happening to an entity may block or unblock events relating to others, namely, events in which the entity does not participate. We show that partial order computations need to capture additional restrictions about event ordering, i.e., restrictions that arise from such reconfigurations. This introduces ambiguity where different partial orders represent exactly the same events with the same participants happening in different orders, thus defeating the purpose of using partial order semantics. To remove this ambiguity, we suggest an extension of partial orders called glued partial orders. We show that glued partial orders capture all possible forced reordering arising from said reconfigurations. Furthermore, we show that computations belonging to different glued partial orders are only different due to non-determinism. We consider channeled transition systems and Petri-nets with inhibiting arcs as examples.
|
|
| 3. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Language Support for Verifying Reconfigurable Interacting Systems
- 2023
-
Ingår i: International Journal on Software Tools for Technology Transfer (STTT). - 1433-2779 .- 1433-2787.
-
Tidskriftsartikel (refereegranskat)abstract
- Reconfigurable interacting systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. In this article, we provide a modeling and analysis environment for the design of such system. Our tool offers simulation and verification to facilitate native reasoning about the domain concepts of such systems. We present our tool named R-CHECK. R-CHECK supports a high-level input language with matching enumerative and symbolic semantics, and provides a modelling convenience for features such as reconfiguration, coalition formation, self-organisation, etc. For analysis, users can simulate the designed system and explore arising traces. Our included model checker permits reasoning about interaction protocols and joint missions.
|
|
| 4. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Model Checking Reconfigurable Interacting Systems
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS,volume 13703). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031197581
-
Konferensbidrag (refereegranskat)abstract
- Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK (Find the associated toolkit repository here: https://github.com/dsynma/recipe.), to allow reasoning about these systems both from an individual- and a system- level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, and self-organisation.
|
|
| 5. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Modelling and verification of reconfigurable multi-agent systems
- 2021
-
Ingår i: Autonomous Agents and Multi-Agent Systems. - : Springer Science and Business Media LLC. - 1387-2532 .- 1573-7454. ; 35
-
Tidskriftsartikel (refereegranskat)abstract
- We 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.
|
|
| 6. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Programming interactions in collective adaptive systems by relying on attribute-based communication
- 2020
-
Ingår i: Science of Computer Programming. - : Elsevier BV. - 0167-6423. ; 192:June
-
Tidskriftsartikel (refereegranskat)abstract
- © 2020 Elsevier B.V. Collective adaptive systems are new emerging computational systems consisting of a large number of interacting components and featuring complex behaviour. These systems are usually distributed, heterogeneous, decentralised and interdependent, and are operating in dynamic and possibly unpredictable environments. Finding ways to understand and design these systems and, most of all, to model the interactions of their components, is a difficult but important endeavour. In this article we propose a language-based approach for programming the interactions of collective-adaptive systems by relying on attribute-based communication; a paradigm that permits a group of partners to communicate by considering their run-time properties and capabilities. We introduce AbC, a foundational calculus for attribute-based communication and show how its linguistic primitives can be used to program a sophisticated variant of the well-known problem of Stable Allocation in Content Delivery Networks. In our variant, content providers are assigned to clients based on collaboration and by taking into account the preferences of both parties in a fully anonymous and distributed settings. We also illustrate the expressive power of attribute-based communication by showing the natural encoding of group-based, publish/subscribe-based and channel-based communication paradigms into AbC.
|
|
| 7. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
R-CHECK: A Model Checker for Verifying Reconfigurable MAS
- 2022
-
Ingår i: AAMAS 2022. - Virtual : AAMAS '22: Proceedings of the 21st International Conference on Autonomous Agents and Multi agent Systems.
-
Konferensbidrag (refereegranskat)abstract
- Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK, to allow reasoning about these systems both from an individual- and a system-level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, self-organisation, etc.
|
|
| 8. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Reconfigurable Interaction for MAS Modelling
- 2020
-
Ingår i: Proceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems. - Auckland, New Zealand : ACM. - 9781450375184
-
Konferensbidrag (refereegranskat)abstract
- We propose a formalism to model and reason about multi-agent systems. We allow agents to 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. The formalism defines a local behaviour based on shared variables and a global one based on message passing. We extend LTL to be able to reason explicitly about the intentions of the different agents and their interaction protocols. We also study the complexity of satisfiability and model-checking of this extension.
|
|
| 9. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Synthesis of Run-To-Completion Controllers for Discrete Event Systems
- 2021
-
Ingår i: 2021 American Control Conference. - : IEEE.
-
Konferensbidrag (refereegranskat)abstract
- A controller for a Discrete Event System must achieve its goals despite its environment being capable of resolving race conditions between controlled and uncontrolled events. Assuming that the controller loses all races is sometimes unrealistic. In many cases, a realistic assumption is that the controller sometimes wins races and is fast enough to perform multiple actions without being interrupted. However, in order to model this scenario using control of DES requires introducing foreign assumptions about scheduling, that are hard to figure out correctly. We propose a more balanced control problem, named run-to-completion (RTC), to alleviate this issue. RTC naturally supports an execution assumption in which both the controller and the environment are guaranteed to initiate and perform sequences of actions, without flooding or delaying each other indefinitely. We consider control of DES in the context where specifications are given in the form of linear temporal logic. We formalize the RTC control problem and show how it can be reduced to a standard control problem.
|
|
| 10. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Testing for coordination fidelity : Testing for coordination fidelity
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. ; , s. 152-169
-
Bokkapitel (refereegranskat)abstract
- © Springer Nature Switzerland AG 2019. Operation control in modern distributed systems must rely on decentralised coordination among system participants. In particular when the operation control involves critical infrastructures such as power grids, it is vital to ensure correctness properties of such coordination mechanisms. In this paper, we present a verification technique that addresses coordination protocols for power grid operation control. Given a global protocol specification, we show how we can rely on testing semantics for the purpose of ensuring protocol fidelity, i.e., to certify that the interaction among the grid nodes follows the protocol specification.
|
|
