| 1. |
- 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.
|
|
| 2. |
- 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.
|
|
| 3. |
- 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.
|
|
| 4. |
- 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.
|
|
| 5. |
- 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.
|
|
| 6. |
- 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.
|
|
| 7. |
- 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.
|
|
| 8. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
Incorporating Monitors in Reactive Synthesis without Paying the Price
- 2021
-
Ingår i: 19th International Symposium on Automated Technology for Verification and Analysis. - Cham : Springer.
-
Konferensbidrag (refereegranskat)abstract
- Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative specifications, and have found languages that combine modelling with declarative specifications more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this paper we explore an approach that combines synthesis of declarative specifications in the presence of an existing behaviour model as a monitor, with the benefit of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeating triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional synthesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we apply it to specifications requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametrisation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.
|
|
| 9. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae
- 2023
-
Ingår i: Automated Technology for Verification and Analysis (ATVA). - Germany : Springer. - 0302-9743 .- 1611-3349. - 9783031453311
-
Konferensbidrag (refereegranskat)abstract
- This paper presents ppLTLTT, a tool for translating pure-past linear temporal logic formulae into temporal testers in the form of automata. We show how ppLTLTT can be used to easily extend existing LTL-based tools, such as LTL-to-automata translators and reactive synthesis tools, to support a richer input language. Namely, with ppLTLTT, tools that accept LTL input are also made to handle pure-past LTL as atomic formulae. While the addition of past operators does not increase the expressive power of LTL, it opens up the possibility of writing more intuitive and succinct specifications. We illustrate this intended use of ppLTLTT for Slugs, Strix, and Spot ’s command line tool LTL2TGBA by describing three corresponding wrapper tools pSlugs, pStrix, and pLTL2TGBA, that all leverage ppLTLTT. All three wrapper tools are designed to seamlessly fit this paradigm, by staying as close to the respective syntax of each underlying tool as possible.
|
|
| 10. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
Runtime Verification Meets Controller Synthesis
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS,volume 13701). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031198489
-
Konferensbidrag (refereegranskat)abstract
- Reactive synthesis guarantees correct-by-construction controllers from logical specifications, but is costly—2EXPTIME-complete in the size of the specification. In a practical setting, the desired controllers need to interact with an environment, but the more precise the model of the environment used for synthesis, the greater the cost of synthesis. This can be avoided by using suitable abstractions of the environment, but this in turn requires appropriate techniques to mediate between controllers and the real environment. Runtime verification can help here, with monitors acting as these mediators, and even as activators or orchestrators of the desired controllers. In this paper we survey literature for combinations of monitors with controller synthesis, and consider other potential combinations as future research directions.
|
|
