\n \n \n
\n
\n\n \n \n \n \n \n \n A PO Characterisation of�Reconfiguration.\n \n \n \n \n\n\n \n Abd Alrahman, Y.; Martel, M.; and Piterman, N.\n\n\n \n\n\n\n In Seidl, H.; Liu, Z.; and Pasareanu, C. S., editor(s),
Theoretical Aspects of Computing – ICTAC 2022, pages 42–59, Cham, 2022. Springer International Publishing\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@InProceedings{10.1007/978-3-031-17715-6_5,\nauthor="{Abd Alrahman}, Yehia\nand Martel, Mauricio\nand Piterman, Nir",\neditor="Seidl, Helmut\nand Liu, Zhiming\nand Pasareanu, Corina S.",\ntitle="A PO Characterisation of�Reconfiguration",\nbooktitle="Theoretical Aspects of Computing -- ICTAC 2022",\nyear="2022",\npublisher="Springer International Publishing",\naddress="Cham",\npages="42--59",\nabstract="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.",\nisbn="978-3-031-17715-6",\nurl = {https://link.springer.com/chapter/10.1007/978-3-031-17715-6_5}\n}\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n R-CHECK: A Model Checker for Verifying Reconfigurable MAS.\n \n \n \n \n\n\n \n Abd Alrahman, Y.; Azzopardi, S.; and Piterman, N.\n\n\n \n\n\n\n In Faliszewski, P.; Mascardi, V.; Pelachaud, C.; and Taylor, M. E., editor(s),
21st International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2022, Auckland, New Zewland, May 9-13, 2022, pages 1518–1520, 2022. International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS,ACM)\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/atal/AlrahmanAP22,\n author = {Yehia {Abd Alrahman} and\n Shaun Azzopardi and\n Nir Piterman},\n editor = {Piotr Faliszewski and\n Viviana Mascardi and\n Catherine Pelachaud and\n Matthew E. Taylor},\n title = {{R-CHECK:} {A} Model Checker for Verifying Reconfigurable {MAS}},\n booktitle = {21st International Conference on Autonomous Agents and Multiagent\n Systems, {AAMAS} 2022, Auckland, New Zewland, May 9-13, 2022},\n pages = {1518--1520},\n publisher = {International Foundation for Autonomous Agents and Multiagent Systems\n {(IFAAMAS,ACM)}},\n year = {2022},\n url = {https://dl.acm.org/doi/abs/10.5555/3535850.3536020},\n abstract = {Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature oppor- tunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual in- terests. 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.}\n}\n
\n
\n\n\n
\n Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature oppor- tunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual in- terests. 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.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Model Checking Reconfigurable Interacting Systems.\n \n \n \n \n\n\n \n Abd Alrahman, Y.; Azzopardi, S.; and Piterman, N.\n\n\n \n\n\n\n In Margaria, T.; and Steffen, B., editor(s),
Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning, pages 373–389, Cham, 2022. Springer Nature Switzerland\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@InProceedings{10.1007/978-3-031-19759-8_23,\nauthor="Abd Alrahman, Yehia\nand Azzopardi, Shaun\nand Piterman, Nir",\neditor="Margaria, Tiziana\nand Steffen, Bernhard",\ntitle="Model Checking Reconfigurable Interacting Systems",\nbooktitle="Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning",\nyear="2022",\npublisher="Springer Nature Switzerland",\naddress="Cham",\npages="373--389",\nabstract="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.",\nisbn="978-3-031-19759-8",\nurl={https://link.springer.com/chapter/10.1007/978-3-031-19759-8_23}\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n