var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https%3A%2F%2Flazkany.bitbucket.io%2Fgrants%2Fsyn.bib&jsonp=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https%3A%2F%2Flazkany.bitbucket.io%2Fgrants%2Fsyn.bib&jsonp=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https%3A%2F%2Flazkany.bitbucket.io%2Fgrants%2Fsyn.bib&jsonp=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
    2. \n
  2. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
    3. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2023\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Language Support for Verifying Reconfigurable Interacting Systems.\n \n \n \n\n\n \n Abd Alrahman, Y.; Azzopardi, S.; Di Stefano, L.; and Piterman, N.\n\n\n \n\n\n\n International Journal on Software Tools for Technology Transfer. 2023.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{sttt2023a,\n  title = {Language Support for Verifying Reconfigurable Interacting Systems},\n  author = {Abd Alrahman, Yehia and Azzopardi, Shaun and Di Stefano, Luca and Piterman, Nir},\n  journal   = {International Journal on Software Tools for Technology Transfer},\n  year =  {2023},\n  doi = {10.1007/s10009-023-00729-8},\n}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (3)\n \n \n
\n
\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 \"APaper\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 \"R-CHECK: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 \"ModelPaper\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
\n
\n\n
\n
\n  \n 2021\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Modelling and Verification of Reconfigurable Multi-Agent Systems.\n \n \n \n \n\n\n \n Abd Alrahman, Y.; and Piterman, N.\n\n\n \n\n\n\n Autonomous Agents and Multi-Agent Systems, 35. August 2021.\n \n\n\n\n
\n\n\n\n \n \n \"ModellingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{jmas,\n  author    = {Yehia {Abd Alrahman} and\n               Nir Piterman},\n  title     = {Modelling and Verification of Reconfigurable Multi-Agent Systems},\n  journal   = { In Autonomous Agents and Multi-Agent Systems},\n  volume    = {35},\n  year      = {2021},\n  month     = {August},\n  publisher = {Springer Science},\n  url       = {https://doi.org/10.1007/s10458-021-09521-x},\n  doi       = {10.1007/s10458-021-09521-x},\n  journal   = {Autonomous Agents and Multi-Agent Systems},\n  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.}\n}\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesis of Run-To-Completion Controllers for Discrete Event Systems.\n \n \n \n \n\n\n \n Abd Alrahman, Y.; Braberman, V. A.; D'Ippolito, N.; Piterman, N.; and Uchitel, S.\n\n\n \n\n\n\n In 2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021, pages 4892–4899, 2021. IEEE\n \n\n\n\n
\n\n\n\n \n \n \"SynthesisPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{acc,\n  author    = {Yehia {Abd Alrahman} and\n               V{\\'{\\i}}ctor A. Braberman and\n               Nicol{\\'{a}}s D'Ippolito and\n               Nir Piterman and\n               Sebasti{\\'{a}}n Uchitel},\n  title     = {Synthesis of Run-To-Completion Controllers for Discrete Event Systems},\n  booktitle = {2021 American Control Conference, {ACC} 2021, New Orleans, LA, USA,\n               May 25-28, 2021},\n  pages     = {4892--4899},\n  publisher = {{IEEE}},\n  year      = {2021},\n  url       = {https://doi.org/10.23919/ACC50511.2021.9482704},\n  doi       = {10.23919/ACC50511.2021.9482704},\n abstract  = {A controller for a Discrete Event System must achieve its goals despite that 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.}\n}
\n
\n\n\n
\n A controller for a Discrete Event System must achieve its goals despite that 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);