var bibbase_data = {"data":"<img src=\"//bibbase.org/img/ajax-loader.gif\" id=\"spinner\"\n  style=\"display: none;\" alt=\"Loading..\" />\n\n<div id=\"bibbase\">\n\n  <script type=\"text/javascript\">\n    var bibbase = {\n      params: {\"bib\":\"https://lazkany.bitbucket.io/publication.bib\",\"jsonp\":\"1\",\"css\":\"assets/css/default.css\",\"host\":\"bibbase.org\"},\n      data: [{\"bibtype\":\"article\",\"type\":\"article\",\"title\":\"Language Support for Verifying Reconfigurable Interacting Systems\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Abd\",\"Alrahman\"],\"firstnames\":[\"Yehia\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Azzopardi\"],\"firstnames\":[\"Shaun\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Di\",\"Stefano\"],\"firstnames\":[\"Luca\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Piterman\"],\"firstnames\":[\"Nir\"],\"suffixes\":[]}],\"journal\":\"International Journal on Software Tools for Technology Transfer\",\"year\":\"2023\",\"doi\":\"10.1007/s10009-023-00729-8\",\"bibtex\":\"@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\",\"author_short\":[\"Abd Alrahman, Y.\",\"Azzopardi, S.\",\"Di Stefano, L.\",\"Piterman, N.\"],\"key\":\"sttt2023a\",\"id\":\"sttt2023a\",\"bibbaseid\":\"abdalrahman-azzopardi-distefano-piterman-languagesupportforverifyingreconfigurableinteractingsystems-2023\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Nir\"],\"propositions\":[],\"lastnames\":[\"Piterman\"],\"suffixes\":[]}],\"title\":\"Correct-by-Design Teamwork Plans for Multi-Agent Systems\",\"journal\":\"CoRR\",\"volume\":\"abs/2301.01257\",\"year\":\"2023\",\"url\":\"https://doi.org/10.48550/arXiv.2301.01257\",\"doi\":\"10.48550/arXiv.2301.01257\",\"eprinttype\":\"arXiv\",\"eprint\":\"2301.01257\",\"bibtex\":\"@article{DBLP:journals/corr/abs-2301-01257,\\n  author    = {Yehia {Abd Alrahman} and\\n               Nir Piterman},\\n  title     = {Correct-by-Design Teamwork Plans for Multi-Agent Systems},\\n  journal   = {CoRR},\\n  volume    = {abs/2301.01257},\\n  year      = {2023},\\n  url       = {https://doi.org/10.48550/arXiv.2301.01257},\\n  doi       = {10.48550/arXiv.2301.01257},\\n  eprinttype = {arXiv},\\n  eprint    = {2301.01257}\\n}\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"Piterman, N.\"],\"key\":\"DBLP:journals/corr/abs-2301-01257\",\"id\":\"DBLP:journals/corr/abs-2301-01257\",\"bibbaseid\":\"abdalrahman-piterman-correctbydesignteamworkplansformultiagentsystems-2023\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.48550/arXiv.2301.01257\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"firstnames\":[\"Yehia\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Martel\"],\"firstnames\":[\"Mauricio\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Piterman\"],\"firstnames\":[\"Nir\"],\"suffixes\":[]}],\"editor\":[{\"propositions\":[],\"lastnames\":[\"Seidl\"],\"firstnames\":[\"Helmut\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Liu\"],\"firstnames\":[\"Zhiming\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Pasareanu\"],\"firstnames\":[\"Corina\",\"S.\"],\"suffixes\":[]}],\"title\":\"A PO Characterisation of Reconfiguration\",\"booktitle\":\"Theoretical Aspects of Computing – ICTAC 2022\",\"year\":\"2022\",\"publisher\":\"Springer International Publishing\",\"address\":\"Cham\",\"pages\":\"42–59\",\"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.\",\"isbn\":\"978-3-031-17715-6\",\"url\":\"https://link.springer.com/chapter/10.1007/978-3-031-17715-6_5\",\"bibtex\":\"@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\",\"author_short\":[\"Abd Alrahman, Y.\",\"Martel, M.\",\"Piterman, N.\"],\"editor_short\":[\"Seidl, H.\",\"Liu, Z.\",\"Pasareanu, C. S.\"],\"key\":\"10.1007/978-3-031-17715-6_5\",\"id\":\"10.1007/978-3-031-17715-6_5\",\"bibbaseid\":\"abdalrahman-martel-piterman-apocharacterisationofreconfiguration-2022\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://link.springer.com/chapter/10.1007/978-3-031-17715-6_5\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"downloads\":1,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Shaun\"],\"propositions\":[],\"lastnames\":[\"Azzopardi\"],\"suffixes\":[]},{\"firstnames\":[\"Nir\"],\"propositions\":[],\"lastnames\":[\"Piterman\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Piotr\"],\"propositions\":[],\"lastnames\":[\"Faliszewski\"],\"suffixes\":[]},{\"firstnames\":[\"Viviana\"],\"propositions\":[],\"lastnames\":[\"Mascardi\"],\"suffixes\":[]},{\"firstnames\":[\"Catherine\"],\"propositions\":[],\"lastnames\":[\"Pelachaud\"],\"suffixes\":[]},{\"firstnames\":[\"Matthew\",\"E.\"],\"propositions\":[],\"lastnames\":[\"Taylor\"],\"suffixes\":[]}],\"title\":\"R-CHECK: A Model Checker for Verifying Reconfigurable MAS\",\"booktitle\":\"21st International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2022, Auckland, New Zewland, May 9-13, 2022\",\"pages\":\"1518–1520\",\"publisher\":\"International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS,ACM)\",\"year\":\"2022\",\"url\":\"https://dl.acm.org/doi/abs/10.5555/3535850.3536020\",\"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.\",\"bibtex\":\"@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\",\"author_short\":[\"Abd Alrahman, Y.\",\"Azzopardi, S.\",\"Piterman, N.\"],\"editor_short\":[\"Faliszewski, P.\",\"Mascardi, V.\",\"Pelachaud, C.\",\"Taylor, M. E.\"],\"key\":\"DBLP:conf/atal/AlrahmanAP22\",\"id\":\"DBLP:conf/atal/AlrahmanAP22\",\"bibbaseid\":\"abdalrahman-azzopardi-piterman-rcheckamodelcheckerforverifyingreconfigurablemas-2022\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://dl.acm.org/doi/abs/10.5555/3535850.3536020\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"downloads\":5,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Abd\",\"Alrahman\"],\"firstnames\":[\"Yehia\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Azzopardi\"],\"firstnames\":[\"Shaun\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Piterman\"],\"firstnames\":[\"Nir\"],\"suffixes\":[]}],\"editor\":[{\"propositions\":[],\"lastnames\":[\"Margaria\"],\"firstnames\":[\"Tiziana\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Steffen\"],\"firstnames\":[\"Bernhard\"],\"suffixes\":[]}],\"title\":\"Model Checking Reconfigurable Interacting Systems\",\"booktitle\":\"Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning\",\"year\":\"2022\",\"publisher\":\"Springer Nature Switzerland\",\"address\":\"Cham\",\"pages\":\"373–389\",\"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.\",\"isbn\":\"978-3-031-19759-8\",\"url\":\"https://link.springer.com/chapter/10.1007/978-3-031-19759-8_23\",\"bibtex\":\"@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\",\"author_short\":[\"Abd Alrahman, Y.\",\"Azzopardi, S.\",\"Piterman, N.\"],\"editor_short\":[\"Margaria, T.\",\"Steffen, B.\"],\"key\":\"10.1007/978-3-031-19759-8_23\",\"id\":\"10.1007/978-3-031-19759-8_23\",\"bibbaseid\":\"abdalrahman-azzopardi-piterman-modelcheckingreconfigurableinteractingsystems-2022\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://link.springer.com/chapter/10.1007/978-3-031-19759-8_23\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Nir\"],\"propositions\":[],\"lastnames\":[\"Piterman\"],\"suffixes\":[]}],\"title\":\"Modelling and verification of reconfigurable multi-agent systems\",\"journal\":\"Autonomous Agents and Multi Agent Systems\",\"volume\":\"35\",\"number\":\"2\",\"pages\":\"47\",\"year\":\"2021\",\"url\":\"https://doi.org/10.1007/s10458-021-09521-x\",\"doi\":\"10.1007/s10458-021-09521-x\",\"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.\",\"bibtex\":\"@article{AlrahmanP21,\\n  author    = {Yehia {Abd Alrahman} and\\n               Nir Piterman},\\n  title     = {Modelling and verification of reconfigurable multi-agent systems},\\n  journal   = {Autonomous Agents and Multi Agent Systems},\\n  volume    = {35},\\n  number    = {2},\\n  pages     = {47},\\n  year      = {2021},\\n  url       = {https://doi.org/10.1007/s10458-021-09521-x},\\n  doi       = {10.1007/s10458-021-09521-x},\\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\",\"author_short\":[\"Abd Alrahman, Y.\",\"Piterman, N.\"],\"key\":\"AlrahmanP21\",\"id\":\"AlrahmanP21\",\"bibbaseid\":\"abdalrahman-piterman-modellingandverificationofreconfigurablemultiagentsystems-2021\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1007/s10458-021-09521-x\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"downloads\":10,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Víctor\",\"A.\"],\"propositions\":[],\"lastnames\":[\"Braberman\"],\"suffixes\":[]},{\"firstnames\":[\"Nicolás\"],\"propositions\":[],\"lastnames\":[\"D'Ippolito\"],\"suffixes\":[]},{\"firstnames\":[\"Nir\"],\"propositions\":[],\"lastnames\":[\"Piterman\"],\"suffixes\":[]},{\"firstnames\":[\"Sebastián\"],\"propositions\":[],\"lastnames\":[\"Uchitel\"],\"suffixes\":[]}],\"title\":\"Synthesis of Run-To-Completion Controllers for Discrete Event Systems\",\"booktitle\":\"2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021\",\"pages\":\"4892–4899\",\"publisher\":\"IEEE\",\"year\":\"2021\",\"url\":\"https://doi.org/10.23919/ACC50511.2021.9482704\",\"doi\":\"10.23919/ACC50511.2021.9482704\",\"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.\",\"bibtex\":\"@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\",\"author_short\":[\"Abd Alrahman, Y.\",\"Braberman, V. A.\",\"D'Ippolito, N.\",\"Piterman, N.\",\"Uchitel, S.\"],\"key\":\"acc\",\"id\":\"acc\",\"bibbaseid\":\"abdalrahman-braberman-dippolito-piterman-uchitel-synthesisofruntocompletioncontrollersfordiscreteeventsystems-2021\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.23919/ACC50511.2021.9482704\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\",\"piterman, n\":\"https://www.cse.chalmers.se/~piterman/publications/index.html\"}},\"downloads\":10,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Abd\",\"Alrahman\"],\"firstnames\":[\"Yehia\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Perelli\"],\"firstnames\":[\"Giuseppe\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Piterman\"],\"firstnames\":[\"Nir\"],\"suffixes\":[]}],\"title\":\"Reconfigurable Interaction for MAS Modelling\",\"year\":\"2020\",\"isbn\":\"9781450375184\",\"publisher\":\"International Foundation for Autonomous Agents and Multiagent Systems\",\"address\":\"Richland, SC\",\"booktitle\":\"Proceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems\",\"pages\":\"7-15\",\"numpages\":\"9\",\"keywords\":\"verification of multi-agent systems, logics for agent reasoning, agent theories and models\",\"location\":\"Auckland, New Zealand\",\"series\":\"AAMAS '20\",\"url\":\"https://dl.acm.org/doi/abs/10.5555/3398761.3398768\",\"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.\",\"bibtex\":\"@inproceedings{rcp,\\n  author    = {Abd Alrahman, Yehia and Perelli, Giuseppe and Piterman, Nir},\\n  title     = {Reconfigurable Interaction for MAS Modelling},\\n  year      = {2020},\\n  isbn      = {9781450375184},\\n  publisher = {International Foundation for Autonomous Agents and Multiagent Systems},\\n  address   = {Richland, SC},\\n  booktitle = {Proceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems},\\n  pages     = {7-15},\\n  numpages  = {9},\\n  keywords  = {verification of multi-agent systems, logics for agent reasoning, agent theories and models},\\n  location  = {Auckland, New Zealand},\\n  series    = {AAMAS '20},\\n  url       = {https://dl.acm.org/doi/abs/10.5555/3398761.3398768},\\n  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.}\\n}\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"Perelli, G.\",\"Piterman, N.\"],\"key\":\"rcp\",\"id\":\"rcp\",\"bibbaseid\":\"abdalrahman-perelli-piterman-reconfigurableinteractionformasmodelling-2020\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://dl.acm.org/doi/abs/10.5555/3398761.3398768\"},\"keyword\":[\"verification of multi-agent systems\",\"logics for agent reasoning\",\"agent theories and models\"],\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\",\"piterman, n\":\"https://www.cse.chalmers.se/~piterman/publications/index.html\",\"perelli, g\":\"https://giuseppeperelli.github.io/oldsite/\"}},\"downloads\":29,\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"doi\":\"10.1007/s10009-020-00553-4\",\"url\":\"https://doi.org/10.1007%2Fs10009-020-00553-4\",\"year\":\"2020\",\"month\":\"feb\",\"publisher\":\"Springer Science and Business Media LLC\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Giulio\"],\"propositions\":[],\"lastnames\":[\"Garbi\"],\"suffixes\":[]}],\"title\":\"A distributed API for coordinating AbC programs\",\"journal\":\"International Journal on Software Tools for Technology Transfer\",\"abstract\":\"Collective-adaptive systems exhibit a particular notion of interaction where environmental conditions largely influence interactions. Previously, we pro- posed a calculus, named AbC, to model and reason about CAS. The calculus proved to be effective by naturally modelling essential CAS features. However, the question on the tradeoff between its expressiveness and its efficiency, when implemented to program CAS applications, is to be answered. In this article, we propose an efficient and distributed coordination infrastructure for AbC. We prove its correctness and we evaluate its performance. The main novelty of our approach is that AbC components are infrastructure agnostic. Thus the code of a component does not specify how messages are routed in the infrastructure but rather what properties a target component must satisfy. We also developed a Go API, named GoAt, and an Eclipse plugin to pro- gram in a high-level syntax which can be automatically used to generate matching Go code. We showcase our development through a non-trivial case study.\",\"bibtex\":\"@article{Abd_Alrahman_2020,\\n  doi       = {10.1007/s10009-020-00553-4},\\n  url       = {https://doi.org/10.1007%2Fs10009-020-00553-4},\\n  year      = {2020},\\n  month     = {feb},\\n  publisher = {Springer Science and Business Media {LLC}},\\n  author    = {Yehia {Abd Alrahman} and Giulio Garbi},\\n  title     = {A distributed {API} for coordinating {AbC} programs},\\n  journal   = {International Journal on Software Tools for Technology Transfer},\\n  abstract  = {Collective-adaptive systems exhibit a particular notion of interaction where environmental conditions largely influence interactions. Previously, we pro- posed a calculus, named AbC, to model and reason about CAS. The calculus proved to be effective by naturally modelling essential CAS features. However, the question on the tradeoff between its expressiveness and its efficiency, when implemented to program CAS applications, is to be answered. In this article, we propose an efficient and distributed coordination infrastructure for AbC. We prove its correctness and we evaluate its performance. The main novelty of our approach is that AbC components are infrastructure agnostic. Thus the code of a component does not specify how messages are routed in the infrastructure but rather what properties a target component must satisfy. We also developed a Go API, named GoAt, and an Eclipse plugin to pro- gram in a high-level syntax which can be automatically used to generate matching Go code. We showcase our development through a non-trivial case study.}\\n}\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"Garbi, G.\"],\"key\":\"Abd_Alrahman_2020\",\"id\":\"Abd_Alrahman_2020\",\"bibbaseid\":\"abdalrahman-garbi-adistributedapiforcoordinatingabcprograms-2020\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1007%2Fs10009-020-00553-4\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"downloads\":2,\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Rocco\"],\"propositions\":[],\"lastnames\":[\"De Nicola\"],\"suffixes\":[]},{\"firstnames\":[\"Michele\"],\"propositions\":[],\"lastnames\":[\"Loreti\"],\"suffixes\":[]}],\"title\":\"Programming interactions in collective adaptive systems by relying on attribute-based communication\",\"journal\":\"Sci. Comput. Program.\",\"volume\":\"192\",\"pages\":\"102428\",\"year\":\"2020\",\"url\":\"https://doi.org/10.1016/j.scico.2020.102428\",\"doi\":\"10.1016/j.scico.2020.102428\",\"abstract\":\"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 complex and sophisticated variant of the well-known problem of Stable Allocation in Content Delivery Networks. Also other interesting case studies, from the realm of collective-adaptive systems, are considered. We also illustrate the expressive power of attribute-based communication by showing the natural encoding of other existing communication paradigms into AbC.\",\"bibtex\":\"@article{DBLP:article/scp/AlrahmanNL20,\\n  author   = {Yehia {Abd Alrahman} and\\n               Rocco {De Nicola} and\\n               Michele Loreti},\\n  title    = {Programming interactions in collective adaptive systems by relying\\n               on attribute-based communication},\\n  journal  = {Sci. Comput. Program.},\\n  volume   = {192},\\n  pages    = {102428},\\n  year     = {2020},\\n  url      = {https://doi.org/10.1016/j.scico.2020.102428},\\n  doi      = {10.1016/j.scico.2020.102428},\\n  abstract = {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 complex and sophisticated variant of the well-known problem of Stable Allocation in Content Delivery Networks. Also other interesting case studies, from the realm of collective-adaptive systems, are considered. We also illustrate the expressive power of attribute-based communication by showing the natural encoding of other existing communication paradigms into AbC.}\\n}\\n\\n\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"De Nicola, R.\",\"Loreti, M.\"],\"key\":\"DBLP:article/scp/AlrahmanNL20\",\"id\":\"DBLP:article/scp/AlrahmanNL20\",\"bibbaseid\":\"abdalrahman-denicola-loreti-programminginteractionsincollectiveadaptivesystemsbyrelyingonattributebasedcommunication-2020\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1016/j.scico.2020.102428\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"downloads\":1,\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Rocco\"],\"propositions\":[],\"lastnames\":[\"De Nicola\"],\"suffixes\":[]},{\"firstnames\":[\"Michele\"],\"propositions\":[],\"lastnames\":[\"Loreti\"],\"suffixes\":[]}],\"title\":\"A calculus for collective-adaptive systems and its behavioural theory\",\"journal\":\"Inf. Comput.\",\"volume\":\"268\",\"year\":\"2019\",\"url\":\"https://doi.org/10.1016/j.ic.2019.104457\",\"doi\":\"10.1016/j.ic.2019.104457\",\"abstract\":\"We propose a process calculus, named AbC, to study the behavioural theory of interactions in collective-adaptive systems by relying on attribute-based communication. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interaction among components is dynamically established by taking into account connections as determined by predicates over their attributes. The structural operational semantics of AbC is based on Labelled Transition Systems that are also used to define bisimilarity between components. Labelled bisimilarity is in full agreement with a barbed congruence, defined by relying on simple basic observables and context closure. The introduced equivalence is used to study the expressiveness of AbC in terms of encoding aspects of broadcast channel-based interactions and to establish formal relationships between system descriptions at different levels of abstraction.\",\"bibtex\":\"@article{DBLP:article/iandc/AlrahmanNL19,\\n  author   = {Yehia {Abd Alrahman} and\\n               Rocco {De Nicola} and\\n               Michele Loreti},\\n  title    = {A calculus for collective-adaptive systems and its behavioural theory},\\n  journal  = {Inf. Comput.},\\n  volume   = {268},\\n  year     = {2019},\\n  url      = {https://doi.org/10.1016/j.ic.2019.104457},\\n  doi      = {10.1016/j.ic.2019.104457},\\n  abstract = {We propose a process calculus, named AbC, to study the behavioural theory of interactions in collective-adaptive systems by relying on attribute-based communication. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interaction among components is dynamically established by taking into account connections as determined by predicates over their attributes. The structural operational semantics of AbC is based on Labelled Transition Systems that are also used to define bisimilarity between components. Labelled bisimilarity is in full agreement with a barbed congruence, defined by relying on simple basic observables and context closure. The introduced equivalence is used to study the expressiveness of AbC in terms of encoding aspects of broadcast channel-based interactions and to establish formal relationships between system descriptions at different levels of abstraction.}\\n}\\n\\n\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"De Nicola, R.\",\"Loreti, M.\"],\"key\":\"DBLP:article/iandc/AlrahmanNL19\",\"id\":\"DBLP:article/iandc/AlrahmanNL19\",\"bibbaseid\":\"abdalrahman-denicola-loreti-acalculusforcollectiveadaptivesystemsanditsbehaviouraltheory-2019\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1016/j.ic.2019.104457\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"downloads\":3,\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Hugo\",\"Torres\"],\"propositions\":[],\"lastnames\":[\"Vieira\"],\"suffixes\":[]}],\"title\":\"A coordination protocol language for power grid operation control\",\"journal\":\"J. Log. Algebraic Methods Program.\",\"volume\":\"109\",\"year\":\"2019\",\"url\":\"https://doi.org/10.1016/j.jlamp.2019.100487\",\"doi\":\"10.1016/j.jlamp.2019.100487\",\"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.\",\"bibtex\":\"@article{DBLP:article/jlap/AlrahmanV19,\\n  author   = {Yehia {Abd Alrahman} and\\n               Hugo Torres Vieira},\\n  title    = {A coordination protocol language for power grid operation control},\\n  journal  = {J. Log. Algebraic Methods Program.},\\n  volume   = {109},\\n  year     = {2019},\\n  url      = {https://doi.org/10.1016/j.jlamp.2019.100487},\\n  doi      = {10.1016/j.jlamp.2019.100487},\\n  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.}\\n}\\n\\n\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"Vieira, H. T.\"],\"key\":\"DBLP:article/jlap/AlrahmanV19\",\"id\":\"DBLP:article/jlap/AlrahmanV19\",\"bibbaseid\":\"abdalrahman-vieira-acoordinationprotocollanguageforpowergridoperationcontrol-2019\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1016/j.jlamp.2019.100487\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"downloads\":4,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Claudio\",\"Antares\"],\"propositions\":[],\"lastnames\":[\"Mezzina\"],\"suffixes\":[]},{\"firstnames\":[\"Hugo\",\"Torres\"],\"propositions\":[],\"lastnames\":[\"Vieira\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Michele\"],\"propositions\":[],\"lastnames\":[\"Boreale\"],\"suffixes\":[]},{\"firstnames\":[\"Flavio\"],\"propositions\":[],\"lastnames\":[\"Corradini\"],\"suffixes\":[]},{\"firstnames\":[\"Michele\"],\"propositions\":[],\"lastnames\":[\"Loreti\"],\"suffixes\":[]},{\"firstnames\":[\"Rosario\"],\"propositions\":[],\"lastnames\":[\"Pugliese\"],\"suffixes\":[]}],\"title\":\"Testing for Coordination Fidelity\",\"booktitle\":\"Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday\",\"series\":\"Lecture Notes in Computer Science\",\"volume\":\"11665\",\"pages\":\"152-169\",\"publisher\":\"Springer\",\"year\":\"2019\",\"url\":\"https://doi.org/10.1007/978-3-030-21485-2\\\\_10\",\"doi\":\"10.1007/978-3-030-21485-2_10\",\"abstract\":\"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.\",\"bibtex\":\"@inproceedings{DBLP:conf/birthday/AlrahmanMV19,\\n  author    = {Yehia {Abd Alrahman} and\\n               Claudio Antares Mezzina and\\n               Hugo Torres Vieira},\\n  editor    = {Michele Boreale and\\n               Flavio Corradini and\\n               Michele Loreti and\\n               Rosario Pugliese},\\n  title     = {Testing for Coordination Fidelity},\\n  booktitle = {Models, Languages, and Tools for Concurrent and Distributed Programming\\n               - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th\\n               Birthday},\\n  series    = {Lecture Notes in Computer Science},\\n  volume    = {11665},\\n  pages     = {152-169},\\n  publisher = {Springer},\\n  year      = {2019},\\n  url       = {https://doi.org/10.1007/978-3-030-21485-2\\\\_10},\\n  doi       = {10.1007/978-3-030-21485-2\\\\_10},\\n  abstract  = {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.}\\n}\\n\\n\\n\\n\\n\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"Mezzina, C. A.\",\"Vieira, H. T.\"],\"editor_short\":[\"Boreale, M.\",\"Corradini, F.\",\"Loreti, M.\",\"Pugliese, R.\"],\"key\":\"DBLP:conf/birthday/AlrahmanMV19\",\"id\":\"DBLP:conf/birthday/AlrahmanMV19\",\"bibbaseid\":\"abdalrahman-mezzina-vieira-testingforcoordinationfidelity-2019\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1007/978-3-030-21485-2\\\\_10\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"downloads\":3,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Rocco\"],\"propositions\":[],\"lastnames\":[\"De Nicola\"],\"suffixes\":[]},{\"firstnames\":[\"Giulio\"],\"propositions\":[],\"lastnames\":[\"Garbi\"],\"suffixes\":[]},{\"firstnames\":[\"Michele\"],\"propositions\":[],\"lastnames\":[\"Loreti\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Christel\"],\"propositions\":[],\"lastnames\":[\"Baier\"],\"suffixes\":[]},{\"firstnames\":[\"Luís\"],\"propositions\":[],\"lastnames\":[\"Caires\"],\"suffixes\":[]}],\"title\":\"A Distributed Coordination Infrastructure for Attribute-Based Interaction\",\"booktitle\":\"Formal Techniques for Distributed Objects, Components, and Systems - 38th IFIP WG 6.1 International Conference, FORTE 2018, Held as Part of the 13th International Federated Conference on Distributed Computing Techniques, DisCoTec 2018, Madrid, Spain, June 18-21, 2018, Proceedings\",\"series\":\"Lecture Notes in Computer Science\",\"volume\":\"10854\",\"pages\":\"1-20\",\"publisher\":\"Springer\",\"year\":\"2018\",\"url\":\"https://doi.org/10.1007/978-3-319-92612-4\\\\_1\",\"doi\":\"10.1007/978-3-319-92612-4_1\",\"abstract\":\"Collective-adaptive systems offer an interesting notion of interaction where run-time contextual data are the driving force for interaction. The attribute-based interaction has been proposed as a foundational theoretical framework to model CAS interactions. The framework permits a group of partners to interact by considering their run-time properties and their environment. In this paper, we lay the basis for an efficient, correct, and distributed implementation of the attribute-based interaction framework. First, we present three coordination infrastructures for message exchange, then we prove their correctness, and finally we model them in terms of stochastic processes to evaluate their performance.\",\"bibtex\":\"@inproceedings{DBLP:conf/forte/AlrahmanNGL18,\\n  author    = {Yehia {Abd Alrahman} and\\n               Rocco {De Nicola} and\\n               Giulio Garbi and\\n               Michele Loreti},\\n  editor    = {Christel Baier and\\n               Lu{\\\\'{\\\\i}}s Caires},\\n  title     = {A Distributed Coordination Infrastructure for Attribute-Based Interaction},\\n  booktitle = {Formal Techniques for Distributed Objects, Components, and Systems\\n               - 38th {IFIP} {WG} 6.1 International Conference, {FORTE} 2018, Held\\n               as Part of the 13th International Federated Conference on Distributed\\n               Computing Techniques, DisCoTec 2018, Madrid, Spain, June 18-21, 2018,\\n               Proceedings},\\n  series    = {Lecture Notes in Computer Science},\\n  volume    = {10854},\\n  pages     = {1-20},\\n  publisher = {Springer},\\n  year      = {2018},\\n  url       = {https://doi.org/10.1007/978-3-319-92612-4\\\\_1},\\n  doi       = {10.1007/978-3-319-92612-4\\\\_1},\\n  abstract  = {Collective-adaptive systems offer an interesting notion of interaction where run-time contextual data are the driving force for interaction. The attribute-based interaction has been proposed as a foundational theoretical framework to model CAS interactions. The framework permits a group of partners to interact by considering their run-time properties and their environment. In this paper, we lay the basis for an efficient, correct, and distributed implementation of the attribute-based interaction framework. First, we present three coordination infrastructures for message exchange, then we prove their correctness, and finally we model them in terms of stochastic processes to evaluate their performance.}\\n}\\n\\n\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"De Nicola, R.\",\"Garbi, G.\",\"Loreti, M.\"],\"editor_short\":[\"Baier, C.\",\"Caires, L.\"],\"key\":\"DBLP:conf/forte/AlrahmanNGL18\",\"id\":\"DBLP:conf/forte/AlrahmanNGL18\",\"bibbaseid\":\"abdalrahman-denicola-garbi-loreti-adistributedcoordinationinfrastructureforattributebasedinteraction-2018\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1007/978-3-319-92612-4\\\\_1\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Rocco\"],\"propositions\":[],\"lastnames\":[\"De Nicola\"],\"suffixes\":[]},{\"firstnames\":[\"Giulio\"],\"propositions\":[],\"lastnames\":[\"Garbi\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Tiziana\"],\"propositions\":[],\"lastnames\":[\"Margaria\"],\"suffixes\":[]},{\"firstnames\":[\"Bernhard\"],\"propositions\":[],\"lastnames\":[\"Steffen\"],\"suffixes\":[]}],\"title\":\"GoAt: Attribute-Based Interaction in Google Go\",\"booktitle\":\"Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III\",\"series\":\"Lecture Notes in Computer Science\",\"volume\":\"11246\",\"pages\":\"288-303\",\"publisher\":\"Springer\",\"year\":\"2018\",\"url\":\"https://doi.org/10.1007/978-3-030-03424-5\\\\_19\",\"doi\":\"10.1007/978-3-030-03424-5_19\",\"abstract\":\"The attribute-based interaction paradigm has been proposed as an appropriate tool to program the interactions of Collective Adaptive Systems where a group of components can interact according to their run-time properties and the environment they operate in. It has been shown that the novel paradigm is very expressive by means of encoding other well-known interaction paradigms. However, the question on the tradeoff between its expressiveness and its efficiency, when implemented to program distributed and collective systems, is still to be answered. In a previous work, we proposed three distributed communication infrastructures to handle message exchange for the attribute-based paradigm and we proved their correctness. In this paper, we describe an actual implementation of these infrastructures in Google Go. We describe an attribute-based programming API, named GoAt , that is parametric with respect to the infrastructure that mediates the interaction between components and an Eclipse plugin for GoAt to program in a high-level syntax which can be automatically used to generate formally verifiable Go code. Finally, we discuss the performance of the API by considering a non-trivial case study.\",\"bibtex\":\"@inproceedings{DBLP:conf/isola/AlrahmanNG18,\\n  author    = {Yehia {Abd Alrahman} and\\n               Rocco {De Nicola} and\\n               Giulio Garbi},\\n  editor    = {Tiziana Margaria and\\n               Bernhard Steffen},\\n  title     = {GoAt: Attribute-Based Interaction in Google Go},\\n  booktitle = {Leveraging Applications of Formal Methods, Verification and Validation.\\n               Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol,\\n               Cyprus, November 5-9, 2018, Proceedings, Part {III}},\\n  series    = {Lecture Notes in Computer Science},\\n  volume    = {11246},\\n  pages     = {288-303},\\n  publisher = {Springer},\\n  year      = {2018},\\n  url       = {https://doi.org/10.1007/978-3-030-03424-5\\\\_19},\\n  doi       = {10.1007/978-3-030-03424-5\\\\_19},\\n  abstract  = {The attribute-based interaction paradigm has been proposed as an appropriate tool to program the interactions of Collective Adaptive Systems where a group of components can interact according to their run-time properties and the environment they operate in. It has been shown that the novel paradigm is very expressive by means of encoding other well-known interaction paradigms. However, the question on the tradeoff between its expressiveness and its efficiency, when implemented to program distributed and collective systems, is still to be answered. In a previous work, we proposed three distributed communication infrastructures to handle message exchange for the attribute-based paradigm and we proved their correctness. In this paper, we describe an actual implementation of these infrastructures in Google Go. We describe an attribute-based programming API, named GoAt , that is parametric with respect to the infrastructure that mediates the interaction between components and an Eclipse plugin for GoAt to program in a high-level syntax which can be automatically used to generate formally verifiable Go code. Finally, we discuss the performance of the API by considering a non-trivial case study.}\\n}\\n\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"De Nicola, R.\",\"Garbi, G.\"],\"editor_short\":[\"Margaria, T.\",\"Steffen, B.\"],\"key\":\"DBLP:conf/isola/AlrahmanNG18\",\"id\":\"DBLP:conf/isola/AlrahmanNG18\",\"bibbaseid\":\"abdalrahman-denicola-garbi-goatattributebasedinteractioningooglego-2018\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1007/978-3-030-03424-5\\\\_19\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Rocco\"],\"propositions\":[],\"lastnames\":[\"De Nicola\"],\"suffixes\":[]},{\"firstnames\":[\"Michele\"],\"propositions\":[],\"lastnames\":[\"Loreti\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Elvira\"],\"propositions\":[],\"lastnames\":[\"Albert\"],\"suffixes\":[]},{\"firstnames\":[\"Ivan\"],\"propositions\":[],\"lastnames\":[\"Lanese\"],\"suffixes\":[]}],\"title\":\"On the Power of Attribute-Based Communication\",\"booktitle\":\"Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings\",\"series\":\"Lecture Notes in Computer Science\",\"volume\":\"9688\",\"pages\":\"1-18\",\"publisher\":\"Springer\",\"year\":\"2016\",\"url\":\"https://doi.org/10.1007/978-3-319-39570-8\\\\_1\",\"doi\":\"10.1007/978-3-319-39570-8_1\",\"abstract\":\"In open systems exhibiting adaptation, behaviors can arise as side effects of intensive components interaction. Finding ways to understand and design these systems, is a difficult but important endeavor. To tackle these issues, we present AbC, a calculus for attribute-based communication. An AbC system consists of a set of parallel agents each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interactions among agents are dynamically established by taking into account \\\"connections\\\" as determined by predicates over the attributes of agents. First, the syntax and the semantics of the calculus are presented, then expressiveness and effectiveness of AbC are demonstrated both in terms of modeling scenarios featuring collaboration, reconfiguration, and adaptation and of the possibility of encoding channel-based interactions and other interaction patterns. Behavioral equivalences for AbC are introduced for establishing formal relationships between different descriptions of the same system.\",\"bibtex\":\"@inproceedings{DBLP:conf/forte/AlrahmanNL16,\\n  author    = {Yehia {Abd Alrahman} and\\n               Rocco {De Nicola} and\\n               Michele Loreti},\\n  editor    = {Elvira Albert and\\n               Ivan Lanese},\\n  title     = {On the Power of Attribute-Based Communication},\\n  booktitle = {Formal Techniques for Distributed Objects, Components, and Systems\\n               - 36th {IFIP} {WG} 6.1 International Conference, {FORTE} 2016, Held\\n               as Part of the 11th International Federated Conference on Distributed\\n               Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June\\n               6-9, 2016, Proceedings},\\n  series    = {Lecture Notes in Computer Science},\\n  volume    = {9688},\\n  pages     = {1-18},\\n  publisher = {Springer},\\n  year      = {2016},\\n  url       = {https://doi.org/10.1007/978-3-319-39570-8\\\\_1},\\n  doi       = {10.1007/978-3-319-39570-8\\\\_1},\\n  abstract  = {In open systems exhibiting adaptation, behaviors can arise as side effects of intensive components interaction. Finding ways to understand and design these systems, is a difficult but important endeavor. To tackle these issues, we present AbC, a calculus for attribute-based communication. An AbC system consists of a set of parallel agents each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interactions among agents are dynamically established by taking into account \\\"connections\\\" as determined by predicates over the attributes of agents. First, the syntax and the semantics of the calculus are presented, then expressiveness and effectiveness of AbC are demonstrated both in terms of modeling scenarios featuring collaboration, reconfiguration, and adaptation and of the possibility of encoding channel-based interactions and other interaction patterns. Behavioral equivalences for AbC are introduced for establishing formal relationships between different descriptions of the same system.}\\n}\\n\\n\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"De Nicola, R.\",\"Loreti, M.\"],\"editor_short\":[\"Albert, E.\",\"Lanese, I.\"],\"key\":\"DBLP:conf/forte/AlrahmanNL16\",\"id\":\"DBLP:conf/forte/AlrahmanNL16\",\"bibbaseid\":\"abdalrahman-denicola-loreti-onthepowerofattributebasedcommunication-2016\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1007/978-3-319-39570-8\\\\_1\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Rocco\"],\"propositions\":[],\"lastnames\":[\"De Nicola\"],\"suffixes\":[]},{\"firstnames\":[\"Michele\"],\"propositions\":[],\"lastnames\":[\"Loreti\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Tiziana\"],\"propositions\":[],\"lastnames\":[\"Margaria\"],\"suffixes\":[]},{\"firstnames\":[\"Bernhard\"],\"propositions\":[],\"lastnames\":[\"Steffen\"],\"suffixes\":[]}],\"title\":\"Programming of CAS Systems by Relying on Attribute-Based Communication\",\"booktitle\":\"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I\",\"series\":\"Lecture Notes in Computer Science\",\"volume\":\"9952\",\"pages\":\"539-553\",\"year\":\"2016\",\"url\":\"https://doi.org/10.1007/978-3-319-47166-2\\\\_38\",\"doi\":\"10.1007/978-3-319-47166-2_38\",\"abstract\":\"In most distributed systems, named connections (i.e., channels) are used as means for programming interaction between communicating partners. These kinds of connections are low level and usually totally independent of the knowledge, the status, the capabilities, ..., in one word, of the attributes of the interacting partners. We have recently introduced a calculus, called AbC, in which interactions among agents are dynamically established by taking into account \\\"connection\\\" as determined by predicates over agent attributes. In this paper, we present Open image in new window , a Java run-time environment that has been developed to support modeling and programming of collective adaptive systems by relying on the communication primitives of the AbC calculus. Systems are described as sets of parallel components, each component is equipped with a set of attributes and communications among components take place in an implicit multicast fashion. By means of a number of examples, we also show how opportunistic behaviors, achieved by run-time attribute updates, can be exploited to express different communication and interaction patterns and to program challenging case studies.\",\"bibtex\":\"@inproceedings{DBLP:conf/isola/AlrahmanNL16,\\n  author    = {Yehia {Abd Alrahman} and\\n               Rocco {De Nicola} and\\n               Michele Loreti},\\n  editor    = {Tiziana Margaria and\\n               Bernhard Steffen},\\n  title     = {Programming of {CAS} Systems by Relying on Attribute-Based Communication},\\n  booktitle = {Leveraging Applications of Formal Methods, Verification and Validation:\\n               Foundational Techniques - 7th International Symposium, ISoLA 2016,\\n               Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part {I}},\\n  series    = {Lecture Notes in Computer Science},\\n  volume    = {9952},\\n  pages     = {539-553},\\n  year      = {2016},\\n  url       = {https://doi.org/10.1007/978-3-319-47166-2\\\\_38},\\n  doi       = {10.1007/978-3-319-47166-2\\\\_38},\\n  abstract  = {In most distributed systems, named connections (i.e., channels) are used as means for programming interaction between communicating partners. These kinds of connections are low level and usually totally independent of the knowledge, the status, the capabilities, ..., in one word, of the attributes of the interacting partners. We have recently introduced a calculus, called AbC, in which interactions among agents are dynamically established by taking into account \\\"connection\\\" as  determined by predicates over agent attributes. In this paper, we present Open image in new window , a Java run-time environment that has been developed to support modeling and programming of collective adaptive systems by relying on the communication primitives of the AbC calculus. Systems are described as sets of parallel components, each component is equipped with a set of attributes and communications among components take place in an implicit multicast fashion. By means of a number of examples, we also show how opportunistic behaviors, achieved by run-time attribute updates, can be exploited to express different communication and interaction patterns and to program challenging case studies.}\\n}\\n\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"De Nicola, R.\",\"Loreti, M.\"],\"editor_short\":[\"Margaria, T.\",\"Steffen, B.\"],\"key\":\"DBLP:conf/isola/AlrahmanNL16\",\"id\":\"DBLP:conf/isola/AlrahmanNL16\",\"bibbaseid\":\"abdalrahman-denicola-loreti-programmingofcassystemsbyrelyingonattributebasedcommunication-2016\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1007/978-3-319-47166-2\\\\_38\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Rocco\"],\"propositions\":[],\"lastnames\":[\"De Nicola\"],\"suffixes\":[]},{\"firstnames\":[\"Michele\"],\"propositions\":[],\"lastnames\":[\"Loreti\"],\"suffixes\":[]},{\"firstnames\":[\"Francesco\"],\"propositions\":[],\"lastnames\":[\"Tiezzi\"],\"suffixes\":[]},{\"firstnames\":[\"Roberto\"],\"propositions\":[],\"lastnames\":[\"Vigo\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Roger\",\"L.\"],\"propositions\":[],\"lastnames\":[\"Wainwright\"],\"suffixes\":[]},{\"firstnames\":[\"Juan\",\"Manuel\"],\"propositions\":[],\"lastnames\":[\"Corchado\"],\"suffixes\":[]},{\"firstnames\":[\"Alessio\"],\"propositions\":[],\"lastnames\":[\"Bechini\"],\"suffixes\":[]},{\"firstnames\":[\"Jiman\"],\"propositions\":[],\"lastnames\":[\"Hong\"],\"suffixes\":[]}],\"title\":\"A calculus for attribute-based communication\",\"booktitle\":\"Proceedings of the 30th Annual ACM Symposium on Applied Computing, Salamanca, Spain, April 13-17, 2015\",\"pages\":\"1840-1845\",\"publisher\":\"ACM\",\"year\":\"2015\",\"url\":\"https://doi.org/10.1145/2695664.2695668\",\"doi\":\"10.1145/2695664.2695668\",\"abstract\":\"The notion of attribute-based communication seems promising to model and analyse systems with huge numbers of interacting components that dynamically adjust and combine their behaviour to achieve specific goals. A basic process calculus, named AbC, is introduced that has as primitive construct exactly attribute-based communication and its impact on the above mentioned kind of systems is considered. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in a broadcast fashion and communication links among components are dynamically established by taking into account interdependences determined by predicates over attributes. First, the syntax and the reduction semantics of AbC are presented, then its expressiveness and effectiveness is demonstrated by modelling two scenarios from the realm of TV streaming channels. An example of how well-established process calculi could be encoded into AbC is given by considering the translation into AbC of a prototypical Ï€-calculus process.\",\"bibtex\":\"@inproceedings{DBLP:conf/sac/AlrahmanNLTV15,\\n  author    = {Yehia {Abd Alrahman} and\\n               Rocco {De Nicola} and\\n               Michele Loreti and\\n               Francesco Tiezzi and\\n               Roberto Vigo},\\n  editor    = {Roger L. Wainwright and\\n               Juan Manuel Corchado and\\n               Alessio Bechini and\\n               Jiman Hong},\\n  title     = {A calculus for attribute-based communication},\\n  booktitle = {Proceedings of the 30th Annual {ACM} Symposium on Applied Computing,\\n               Salamanca, Spain, April 13-17, 2015},\\n  pages     = {1840-1845},\\n  publisher = {{ACM}},\\n  year      = {2015},\\n  url       = {https://doi.org/10.1145/2695664.2695668},\\n  doi       = {10.1145/2695664.2695668},\\n  abstract  = {The notion of attribute-based communication seems promising to model and analyse systems with huge numbers of interacting components that dynamically adjust and combine their behaviour to achieve specific goals. A basic process calculus, named AbC, is introduced that has as primitive construct exactly attribute-based communication and its impact on the above mentioned kind of systems is considered. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in a broadcast fashion and communication links among components are dynamically established by taking into account interdependences determined by predicates over attributes. First, the syntax and the reduction semantics of AbC are presented, then its expressiveness and effectiveness is demonstrated by modelling two scenarios from the realm of TV streaming channels. An example of how well-established process calculi could be encoded into AbC is given by considering the translation into AbC of a prototypical Ï€-calculus process.}\\n}\\n\\n\\n\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"De Nicola, R.\",\"Loreti, M.\",\"Tiezzi, F.\",\"Vigo, R.\"],\"editor_short\":[\"Wainwright, R. L.\",\"Corchado, J. M.\",\"Bechini, A.\",\"Hong, J.\"],\"key\":\"DBLP:conf/sac/AlrahmanNLTV15\",\"id\":\"DBLP:conf/sac/AlrahmanNLTV15\",\"bibbaseid\":\"abdalrahman-denicola-loreti-tiezzi-vigo-acalculusforattributebasedcommunication-2015\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1145/2695664.2695668\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"author\":[{\"firstnames\":[\"Yehia\"],\"propositions\":[],\"lastnames\":[\"Abd Alrahman\"],\"suffixes\":[]},{\"firstnames\":[\"Marina\"],\"propositions\":[],\"lastnames\":[\"Andric\"],\"suffixes\":[]},{\"firstnames\":[\"Alessandro\"],\"propositions\":[],\"lastnames\":[\"Beggiato\"],\"suffixes\":[]},{\"firstnames\":[\"Alberto\"],\"propositions\":[],\"lastnames\":[\"Lluch-Lafuente\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Santiago\"],\"propositions\":[],\"lastnames\":[\"Escobar\"],\"suffixes\":[]}],\"title\":\"Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?\",\"booktitle\":\"Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Revised Selected Papers\",\"series\":\"Lecture Notes in Computer Science\",\"volume\":\"8663\",\"pages\":\"21-41\",\"publisher\":\"Springer\",\"year\":\"2014\",\"url\":\"https://doi.org/10.1007/978-3-319-12904-4\\\\_2\",\"doi\":\"10.1007/978-3-319-12904-4_2\",\"abstract\":\"Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.\",\"bibtex\":\"@inproceedings{DBLP:conf/wrla/AlrahmanABL14,\\n  author    = {Yehia {Abd Alrahman} and\\n               Marina Andric and\\n               Alessandro Beggiato and\\n               Alberto Lluch{-}Lafuente},\\n  editor    = {Santiago Escobar},\\n  title     = {Can We Efficiently Check Concurrent Programs Under Relaxed Memory\\n               Models in Maude?},\\n  booktitle = {Rewriting Logic and Its Applications - 10th International Workshop,\\n               {WRLA} 2014, Held as a Satellite Event of ETAPS, Grenoble, France,\\n               April 5-6, 2014, Revised Selected Papers},\\n  series    = {Lecture Notes in Computer Science},\\n  volume    = {8663},\\n  pages     = {21-41},\\n  publisher = {Springer},\\n  year      = {2014},\\n  url       = {https://doi.org/10.1007/978-3-319-12904-4\\\\_2},\\n  doi       = {10.1007/978-3-319-12904-4\\\\_2},\\n  abstract  = {Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some   of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.}\\n}\\n\",\"author_short\":[\"Abd Alrahman, Y.\",\"Andric, M.\",\"Beggiato, A.\",\"Lluch-Lafuente, A.\"],\"editor_short\":[\"Escobar, S.\"],\"key\":\"DBLP:conf/wrla/AlrahmanABL14\",\"id\":\"DBLP:conf/wrla/AlrahmanABL14\",\"bibbaseid\":\"abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://doi.org/10.1007/978-3-319-12904-4\\\\_2\"},\"metadata\":{\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\"html\":\"\"}],\n      metadata: {\"owner\":\"abd alrahman, y\",\"authorlinks\":{\"abd alrahman, y\":\"https://lazkany.bitbucket.io/\"}},\n      ownerID: \"afaPc76uuap4k53rq\"\n    };\n  </script>\n\n  <script type=\"text/javascript\">\n  var site$;\n  if (typeof $ != 'undefined') {\n    console.log('existing jquery: storing and then restoring');\n    site$ = $;\n    $ = null;\n  }\n  </script>\n\n  <script src=\"https://ajax.googleapis.com/ajax/libs/jquery/2.2.4/jquery.min.js\">\n  </script>\n  <script type=\"text/javascript\">\n  if (site$) {\n    console.log('existing jquery: avoiding conflict and restoring');\n    bb$ = $.noConflict(true);\n    $ = site$;\n  } else {\n    bb$ = $;\n  }\n  </script>\n\n  <script src=\"//bibbase.org/js/bibbase.min.js\"\n          type=\"text/javascript\">\n  </script>\n\n  <script type=\"text/javascript\"\n          src=\"https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML\">\n  </script>\n  <script type=\"text/x-mathjax-config\">\n    MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\\\(','\\\\)']]},\n                        skipTags: [\"body\"],\n                        processClass: \"bibbase_paper\"});\n  </script>\n\n  <style>\n  @media print {\n    .dontprint {\n        display: none !important;\n    }\n\n  .bibbase_group {\n    background-color: #E0E0E0;\n    font-style: italic;\n    font-size: larger;\n    text-shadow: 0px 0px 3px #FFFFFF;\n    border-radius: 4px 4px 4px 4px;\n    -moz-border-radius: 4px 4px 4px 4px;\n    -webkit-border-radius: 4px;\n    padding: 5px 40px 5px;\n    margin-top: 10px;\n    margin-bottom: 5px;\n    cursor: pointer;\n  }\n\n  .bibbase_paper {\n    margin-bottom: 5px;\n  }\n\n  }\n  </style>\n\n  \n  <div style=\"float: right; margin-right: 10px; margin-top: 10px; text-align: right; font-size: 12px\">\n    generated by\n    <a href=\"//bibbase.org\"\n       onclick=\"trackOutboundLink('bibbase', 'logo clicked', window.location.href, '//bibbase.org'); return false;\">\n      <img src=\"//bibbase.org/img/logo.svg\"\n           style=\"vertical-align: middle; margin-left: 3px; height: 16px;\"/\n           alt=\"bibbase.org\"\n           title=\"BibBase – The easiest way to maintain your publications page.\"\n        ></a>\n    \n  </div>\n  \n\n  <div id=\"bibbase_header\" class=\"dontprint\" style=\"\">\n\n    <ul class=\"nav nav-pills\" style=\"margin: 0px;\">\n\n      <li class=\"dropdown\" id=\"groupby_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\">\n          Group by\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li class=\"groupby year\"><a onclick=\"groupby('year')\">\n            Year</a>\n        </li>\n        <li class=\"groupby author\"><a onclick=\"groupby('author_short')\">\n            Author</a>\n        </li>\n        <li class=\"groupby type\"><a onclick=\"groupby('type')\">\n            Type</a>\n        </li>\n        <li class=\"groupby keyword\"><a onclick=\"groupby('keyword')\">\n            Keyword</a>\n        </li>\n        <li class=\"groupby downloads\"><a onclick=\"groupby('downloads')\">\n            Downloads</a>\n        </li>\n      </ul>\n      </li>\n\n\n      <li class=\"dropdown\" id=\"menu_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\" alt=\"controls\">\n          <i class=\"fa fa-reorder\" alt=\"controls\"></i>\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li>\n          <a onclick=\"toggleAll()\">\n            <i class=\"fa fa-chevron-down fa-fw\"></i> Expand/Collapse All\n          </a>\n        </li>\n        <li>\n          <a download=\"publication.bib\" href=\"data:text/bibtex;base64,QGFydGljbGV7c3R0dDIwMjNhLAogIHRpdGxlID0ge0xhbmd1YWdlIFN1cHBvcnQgZm9yIFZlcmlmeWluZyBSZWNvbmZpZ3VyYWJsZSBJbnRlcmFjdGluZyBTeXN0ZW1zfSwKICBhdXRob3IgPSB7QWJkIEFscmFobWFuLCBZZWhpYSBhbmQgQXp6b3BhcmRpLCBTaGF1biBhbmQgRGkgU3RlZmFubywgTHVjYSBhbmQgUGl0ZXJtYW4sIE5pcn0sCiAgam91cm5hbCAgID0ge0ludGVybmF0aW9uYWwgSm91cm5hbCBvbiBTb2Z0d2FyZSBUb29scyBmb3IgVGVjaG5vbG9neSBUcmFuc2Zlcn0sCiAgeWVhciA9ICB7MjAyM30sCiAgZG9pID0gezEwLjEwMDcvczEwMDA5LTAyMy0wMDcyOS04fSwKfQoKCgpAYXJ0aWNsZXtEQkxQOmpvdXJuYWxzL2NvcnIvYWJzLTIzMDEtMDEyNTcsCiAgYXV0aG9yICAgID0ge1llaGlhIHtBYmQgQWxyYWhtYW59IGFuZAogICAgICAgICAgICAgICBOaXIgUGl0ZXJtYW59LAogIHRpdGxlICAgICA9IHtDb3JyZWN0LWJ5LURlc2lnbiBUZWFtd29yayBQbGFucyBmb3IgTXVsdGktQWdlbnQgU3lzdGVtc30sCiAgam91cm5hbCAgID0ge0NvUlJ9LAogIHZvbHVtZSAgICA9IHthYnMvMjMwMS4wMTI1N30sCiAgeWVhciAgICAgID0gezIwMjN9LAogIHVybCAgICAgICA9IHtodHRwczovL2RvaS5vcmcvMTAuNDg1NTAvYXJYaXYuMjMwMS4wMTI1N30sCiAgZG9pICAgICAgID0gezEwLjQ4NTUwL2FyWGl2LjIzMDEuMDEyNTd9LAogIGVwcmludHR5cGUgPSB7YXJYaXZ9LAogIGVwcmludCAgICA9IHsyMzAxLjAxMjU3fQp9CgoKQEluUHJvY2VlZGluZ3N7MTAuMTAwNy85NzgtMy0wMzEtMTc3MTUtNl81LAphdXRob3I9IntBYmQgQWxyYWhtYW59LCBZZWhpYQphbmQgTWFydGVsLCBNYXVyaWNpbwphbmQgUGl0ZXJtYW4sIE5pciIsCmVkaXRvcj0iU2VpZGwsIEhlbG11dAphbmQgTGl1LCBaaGltaW5nCmFuZCBQYXNhcmVhbnUsIENvcmluYSBTLiIsCnRpdGxlPSJBIFBPIENoYXJhY3RlcmlzYXRpb24gb2bCoFJlY29uZmlndXJhdGlvbiIsCmJvb2t0aXRsZT0iVGhlb3JldGljYWwgQXNwZWN0cyBvZiBDb21wdXRpbmcgLS0gSUNUQUMgMjAyMiIsCnllYXI9IjIwMjIiLApwdWJsaXNoZXI9IlNwcmluZ2VyIEludGVybmF0aW9uYWwgUHVibGlzaGluZyIsCmFkZHJlc3M9IkNoYW0iLApwYWdlcz0iNDItLTU5IiwKYWJzdHJhY3Q9IldlIGNvbnNpZGVyIHBhcnRpYWwgb3JkZXIgc2VtYW50aWNzIG9mIGNvbmN1cnJlbnQgc3lzdGVtcyBpbiB3aGljaCBsb2NhbCByZWNvbmZpZ3VyYXRpb25zIG1heSBoYXZlIGdsb2JhbCBzaWRlIGVmZmVjdHMuIFRoYXQgaXMsIGxvY2FsIGNoYW5nZXMgaGFwcGVuaW5nIHRvIGFuIGVudGl0eSBtYXkgYmxvY2sgb3IgdW5ibG9jayBldmVudHMgcmVsYXRpbmcgdG8gb3RoZXJzLCBuYW1lbHksIGV2ZW50cyBpbiB3aGljaCB0aGUgZW50aXR5IGRvZXMgbm90IHBhcnRpY2lwYXRlLiBXZSBzaG93IHRoYXQgcGFydGlhbCBvcmRlciBjb21wdXRhdGlvbnMgbmVlZCB0byBjYXB0dXJlIGFkZGl0aW9uYWwgcmVzdHJpY3Rpb25zIGFib3V0IGV2ZW50IG9yZGVyaW5nLCBpLmUuLCByZXN0cmljdGlvbnMgdGhhdCBhcmlzZSBmcm9tIHN1Y2ggcmVjb25maWd1cmF0aW9ucy4gVGhpcyBpbnRyb2R1Y2VzIGFtYmlndWl0eSB3aGVyZSBkaWZmZXJlbnQgcGFydGlhbCBvcmRlcnMgcmVwcmVzZW50IGV4YWN0bHkgdGhlIHNhbWUgZXZlbnRzIHdpdGggdGhlIHNhbWUgcGFydGljaXBhbnRzIGhhcHBlbmluZyBpbiBkaWZmZXJlbnQgb3JkZXJzLCB0aHVzIGRlZmVhdGluZyB0aGUgcHVycG9zZSBvZiB1c2luZyBwYXJ0aWFsIG9yZGVyIHNlbWFudGljcy4gVG8gcmVtb3ZlIHRoaXMgYW1iaWd1aXR5LCB3ZSBzdWdnZXN0IGFuIGV4dGVuc2lvbiBvZiBwYXJ0aWFsIG9yZGVycyBjYWxsZWQgZ2x1ZWQgcGFydGlhbCBvcmRlcnMuIFdlIHNob3cgdGhhdCBnbHVlZCBwYXJ0aWFsIG9yZGVycyBjYXB0dXJlIGFsbCBwb3NzaWJsZSBmb3JjZWQgcmVvcmRlcmluZyBhcmlzaW5nIGZyb20gc2FpZCByZWNvbmZpZ3VyYXRpb25zLiBGdXJ0aGVybW9yZSwgd2Ugc2hvdyB0aGF0IGNvbXB1dGF0aW9ucyBiZWxvbmdpbmcgdG8gZGlmZmVyZW50IGdsdWVkIHBhcnRpYWwgb3JkZXJzIGFyZSBvbmx5IGRpZmZlcmVudCBkdWUgdG8gbm9uLWRldGVybWluaXNtLiBXZSBjb25zaWRlciBjaGFubmVsZWQgdHJhbnNpdGlvbiBzeXN0ZW1zIGFuZCBQZXRyaS1uZXRzIHdpdGggaW5oaWJpdGluZyBhcmNzIGFzIGV4YW1wbGVzLiIsCmlzYm49Ijk3OC0zLTAzMS0xNzcxNS02IiwKdXJsICAgICAgID0ge2h0dHBzOi8vbGluay5zcHJpbmdlci5jb20vY2hhcHRlci8xMC4xMDA3Lzk3OC0zLTAzMS0xNzcxNS02XzV9Cn0KCgoKCkBpbnByb2NlZWRpbmdze0RCTFA6Y29uZi9hdGFsL0FscmFobWFuQVAyMiwKICBhdXRob3IgICAgPSB7WWVoaWEge0FiZCBBbHJhaG1hbn0gYW5kCiAgICAgICAgICAgICAgIFNoYXVuIEF6em9wYXJkaSBhbmQKICAgICAgICAgICAgICAgTmlyIFBpdGVybWFufSwKICBlZGl0b3IgICAgPSB7UGlvdHIgRmFsaXN6ZXdza2kgYW5kCiAgICAgICAgICAgICAgIFZpdmlhbmEgTWFzY2FyZGkgYW5kCiAgICAgICAgICAgICAgIENhdGhlcmluZSBQZWxhY2hhdWQgYW5kCiAgICAgICAgICAgICAgIE1hdHRoZXcgRS4gVGF5bG9yfSwKICB0aXRsZSAgICAgPSB7e1ItQ0hFQ0s6fSB7QX0gTW9kZWwgQ2hlY2tlciBmb3IgVmVyaWZ5aW5nIFJlY29uZmlndXJhYmxlIHtNQVN9fSwKICBib29rdGl0bGUgPSB7MjFzdCBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2Ugb24gQXV0b25vbW91cyBBZ2VudHMgYW5kIE11bHRpYWdlbnQKICAgICAgICAgICAgICAgU3lzdGVtcywge0FBTUFTfSAyMDIyLCBBdWNrbGFuZCwgTmV3IFpld2xhbmQsIE1heSA5LTEzLCAyMDIyfSwKICBwYWdlcyAgICAgPSB7MTUxOC0tMTUyMH0sCiAgcHVibGlzaGVyID0ge0ludGVybmF0aW9uYWwgRm91bmRhdGlvbiBmb3IgQXV0b25vbW91cyBBZ2VudHMgYW5kIE11bHRpYWdlbnQgU3lzdGVtcwogICAgICAgICAgICAgICB7KElGQUFNQVMsQUNNKX19LAogIHllYXIgICAgICA9IHsyMDIyfSwKICB1cmwgICAgICAgPSB7aHR0cHM6Ly9kbC5hY20ub3JnL2RvaS9hYnMvMTAuNTU1NS8zNTM1ODUwLjM1MzYwMjB9LAogIGFic3RyYWN0ICA9IHtSZWNvbmZpZ3VyYWJsZSBtdWx0aS1hZ2VudCBzeXN0ZW1zIGNvbnNpc3Qgb2YgYSBzZXQgb2YgYXV0b25vbW91cyBhZ2VudHMsIHdpdGggaW50ZWdyYXRlZCBpbnRlcmFjdGlvbiBjYXBhYmlsaXRpZXMgdGhhdCBmZWF0dXJlIG9wcG9yLSB0dW5pc3RpYyBpbnRlcmFjdGlvbi4gQWdlbnRzIHNlZW1pbmdseSByZWNvbmZpZ3VyZSB0aGVpciBpbnRlcmFjdGlvbnMgaW50ZXJmYWNlcyBieSBmb3JtaW5nIGNvbGxlY3RpdmVzLCBhbmQgaW50ZXJhY3QgYmFzZWQgb24gbXV0dWFsIGluLSB0ZXJlc3RzLiBGaW5kaW5nIHdheXMgdG8gZGVzaWduIGFuZCBhbmFseXNlIHRoZSBiZWhhdmlvdXIgb2YgdGhlc2Ugc3lzdGVtcyBpcyBhIHZpZ29yb3VzbHkgcHVyc3VlZCByZXNlYXJjaCBnb2FsLiBXZSBwcm9wb3NlIGEgbW9kZWwgY2hlY2tlciwgbmFtZWQgUi1DSEVDSywgdG8gYWxsb3cgcmVhc29uaW5nIGFib3V0IHRoZXNlIHN5c3RlbXMgYm90aCBmcm9tIGFuIGluZGl2aWR1YWwtIGFuZCBhIHN5c3RlbS0gbGV2ZWwuIFItQ0hFQ0sgYWxzbyBwZXJtaXRzIHJlYXNvbmluZyBhYm91dCBpbnRlcmFjdGlvbiBwcm90b2NvbHMgYW5kIGpvaW50IG1pc3Npb25zLiBSLUNIRUNLIHN1cHBvcnRzIGEgaGlnaC1sZXZlbCBpbnB1dCBsYW5ndWFnZSB3aXRoIHN5bWJvbGljIHNlbWFudGljcywgYW5kIHByb3ZpZGVzIGEgbW9kZWxsaW5nIGNvbnZlbmllbmNlIGZvciBpbnRlcmFjdGlvbiBmZWF0dXJlcyBzdWNoIGFzIHJlY29uZmlndXJhdGlvbiwgY29hbGl0aW9uIGZvcm1hdGlvbiwgc2VsZi1vcmdhbmlzYXRpb24sIGV0Yy59Cn0KCgpASW5Qcm9jZWVkaW5nc3sxMC4xMDA3Lzk3OC0zLTAzMS0xOTc1OS04XzIzLAphdXRob3I9IkFiZCBBbHJhaG1hbiwgWWVoaWEKYW5kIEF6em9wYXJkaSwgU2hhdW4KYW5kIFBpdGVybWFuLCBOaXIiLAplZGl0b3I9Ik1hcmdhcmlhLCBUaXppYW5hCmFuZCBTdGVmZmVuLCBCZXJuaGFyZCIsCnRpdGxlPSJNb2RlbCBDaGVja2luZyBSZWNvbmZpZ3VyYWJsZSBJbnRlcmFjdGluZyBTeXN0ZW1zIiwKYm9va3RpdGxlPSJMZXZlcmFnaW5nIEFwcGxpY2F0aW9ucyBvZiBGb3JtYWwgTWV0aG9kcywgVmVyaWZpY2F0aW9uIGFuZCBWYWxpZGF0aW9uLiBBZGFwdGF0aW9uIGFuZCBMZWFybmluZyIsCnllYXI9IjIwMjIiLApwdWJsaXNoZXI9IlNwcmluZ2VyIE5hdHVyZSBTd2l0emVybGFuZCIsCmFkZHJlc3M9IkNoYW0iLApwYWdlcz0iMzczLS0zODkiLAphYnN0cmFjdD0iUmVjb25maWd1cmFibGUgbXVsdGktYWdlbnQgc3lzdGVtcyBjb25zaXN0IG9mIGEgc2V0IG9mIGF1dG9ub21vdXMgYWdlbnRzLCB3aXRoIGludGVncmF0ZWQgaW50ZXJhY3Rpb24gY2FwYWJpbGl0aWVzIHRoYXQgZmVhdHVyZSBvcHBvcnR1bmlzdGljIGludGVyYWN0aW9uLiBBZ2VudHMgc2VlbWluZ2x5IHJlY29uZmlndXJlIHRoZWlyIGludGVyYWN0aW9ucyBpbnRlcmZhY2VzIGJ5IGZvcm1pbmcgY29sbGVjdGl2ZXMsIGFuZCBpbnRlcmFjdCBiYXNlZCBvbiBtdXR1YWwgaW50ZXJlc3RzLiBGaW5kaW5nIHdheXMgdG8gZGVzaWduIGFuZCBhbmFseXNlIHRoZSBiZWhhdmlvdXIgb2YgdGhlc2Ugc3lzdGVtcyBpcyBhIHZpZ29yb3VzbHkgcHVyc3VlZCByZXNlYXJjaCBnb2FsLiBXZSBwcm9wb3NlIGEgbW9kZWwgY2hlY2tlciwgbmFtZWQgUi1DSEVDSyAoRmluZCB0aGUgYXNzb2NpYXRlZCB0b29sa2l0IHJlcG9zaXRvcnkgaGVyZTogaHR0cHM6Ly9naXRodWIuY29tL2RzeW5tYS9yZWNpcGUuKSwgdG8gYWxsb3cgcmVhc29uaW5nIGFib3V0IHRoZXNlIHN5c3RlbXMgYm90aCBmcm9tIGFuIGluZGl2aWR1YWwtIGFuZCBhIHN5c3RlbS0gbGV2ZWwuIFItQ0hFQ0sgYWxzbyBwZXJtaXRzIHJlYXNvbmluZyBhYm91dCBpbnRlcmFjdGlvbiBwcm90b2NvbHMgYW5kIGpvaW50IG1pc3Npb25zLiBSLUNIRUNLIHN1cHBvcnRzIGEgaGlnaC1sZXZlbCBpbnB1dCBsYW5ndWFnZSB3aXRoIHN5bWJvbGljIHNlbWFudGljcywgYW5kIHByb3ZpZGVzIGEgbW9kZWxsaW5nIGNvbnZlbmllbmNlIGZvciBpbnRlcmFjdGlvbiBmZWF0dXJlcyBzdWNoIGFzIHJlY29uZmlndXJhdGlvbiwgY29hbGl0aW9uIGZvcm1hdGlvbiwgYW5kIHNlbGYtb3JnYW5pc2F0aW9uLiIsCmlzYm49Ijk3OC0zLTAzMS0xOTc1OS04IiwKdXJsPXtodHRwczovL2xpbmsuc3ByaW5nZXIuY29tL2NoYXB0ZXIvMTAuMTAwNy85NzgtMy0wMzEtMTk3NTktOF8yM30KfQoKCgpAYXJ0aWNsZXtBbHJhaG1hblAyMSwKICBhdXRob3IgICAgPSB7WWVoaWEge0FiZCBBbHJhaG1hbn0gYW5kCiAgICAgICAgICAgICAgIE5pciBQaXRlcm1hbn0sCiAgdGl0bGUgICAgID0ge01vZGVsbGluZyBhbmQgdmVyaWZpY2F0aW9uIG9mIHJlY29uZmlndXJhYmxlIG11bHRpLWFnZW50IHN5c3RlbXN9LAogIGpvdXJuYWwgICA9IHtBdXRvbm9tb3VzIEFnZW50cyBhbmQgTXVsdGkgQWdlbnQgU3lzdGVtc30sCiAgdm9sdW1lICAgID0gezM1fSwKICBudW1iZXIgICAgPSB7Mn0sCiAgcGFnZXMgICAgID0gezQ3fSwKICB5ZWFyICAgICAgPSB7MjAyMX0sCiAgdXJsICAgICAgID0ge2h0dHBzOi8vZG9pLm9yZy8xMC4xMDA3L3MxMDQ1OC0wMjEtMDk1MjEteH0sCiAgZG9pICAgICAgID0gezEwLjEwMDcvczEwNDU4LTAyMS0wOTUyMS14fSwKICBhYnN0cmFjdCAgPSB7V2UgcHJvcG9zZSBhIGZvcm1hbGlzbSB0byBtb2RlbCBhbmQgcmVhc29uIGFib3V0IHJlY29uZmlndXJhYmxlIG11bHRpLWFnZW50IHN5c3RlbXMuIEluIG91ciBmb3JtYWxpc20sIGFnZW50cyBpbnRlcmFjdCBhbmQgY29tbXVuaWNhdGUgaW4gZGlmZmVyZW50IG1vZGVzIHNvIHRoYXQgdGhleSBjYW4gcHVyc3VlIGpvaW50IHRhc2tzOyBhZ2VudHMgbWF5IGR5bmFtaWNhbGx5IHN5bmNocm9uaXplLCBleGNoYW5nZSBkYXRhLCBhZGFwdCB0aGVpciBiZWhhdmlvdXIsIGFuZCByZWNvbmZpZ3VyZSB0aGVpciBjb21tdW5pY2F0aW9uIGludGVyZmFjZXMuIEluc3BpcmVkIGJ5IGV4aXN0aW5nIG11bHRpLXJvYm90IHN5c3RlbXMsIHdlIHJlcHJlc2VudCBhIHN5c3RlbSBhcyBhIHNldCBvZiBhZ2VudHMgKGVhY2ggd2l0aCBsb2NhbCBzdGF0ZSksIGV4ZWN1dGluZyBpbmRlcGVuZGVudGx5IGFuZCBvbmx5IGluZmx1ZW5jZSBlYWNoIG90aGVyIGJ5IG1lYW5zIG9mIG1lc3NhZ2UgZXhjaGFuZ2UuIEFnZW50cyBhcmUgYWJsZSB0byBzZW5zZSB0aGVpciBsb2NhbCBzdGF0ZXMgYW5kIHBhcnRpYWxseSB0aGVpciBzdXJyb3VuZGluZ3MuIFdlIGV4dGVuZCBMVEwgdG8gYmUgYWJsZSB0byByZWFzb24gZXhwbGljaXRseSBhYm91dCB0aGUgaW50ZW50aW9ucyBvZiBhZ2VudHMgaW4gdGhlIGludGVyYWN0aW9uIGFuZCB0aGVpciBjb21tdW5pY2F0aW9uIHByb3RvY29scy4gV2UgYWxzbyBzdHVkeSB0aGUgY29tcGxleGl0eSBvZiBzYXRpc2ZpYWJpbGl0eSBhbmQgbW9kZWwtY2hlY2tpbmcgb2YgdGhpcyBleHRlbnNpb24ufQp9CgoKQGlucHJvY2VlZGluZ3N7YWNjLAogIGF1dGhvciAgICA9IHtZZWhpYSB7QWJkIEFscmFobWFufSBhbmQKICAgICAgICAgICAgICAgVntcJ3tcaX19Y3RvciBBLiBCcmFiZXJtYW4gYW5kCiAgICAgICAgICAgICAgIE5pY29se1wne2F9fXMgRCdJcHBvbGl0byBhbmQKICAgICAgICAgICAgICAgTmlyIFBpdGVybWFuIGFuZAogICAgICAgICAgICAgICBTZWJhc3Rpe1wne2F9fW4gVWNoaXRlbH0sCiAgdGl0bGUgICAgID0ge1N5bnRoZXNpcyBvZiBSdW4tVG8tQ29tcGxldGlvbiBDb250cm9sbGVycyBmb3IgRGlzY3JldGUgRXZlbnQgU3lzdGVtc30sCiAgYm9va3RpdGxlID0gezIwMjEgQW1lcmljYW4gQ29udHJvbCBDb25mZXJlbmNlLCB7QUNDfSAyMDIxLCBOZXcgT3JsZWFucywgTEEsIFVTQSwKICAgICAgICAgICAgICAgTWF5IDI1LTI4LCAyMDIxfSwKICBwYWdlcyAgICAgPSB7NDg5Mi0tNDg5OX0sCiAgcHVibGlzaGVyID0ge3tJRUVFfX0sCiAgeWVhciAgICAgID0gezIwMjF9LAogIHVybCAgICAgICA9IHtodHRwczovL2RvaS5vcmcvMTAuMjM5MTkvQUNDNTA1MTEuMjAyMS45NDgyNzA0fSwKICBkb2kgICAgICAgPSB7MTAuMjM5MTkvQUNDNTA1MTEuMjAyMS45NDgyNzA0fSwKIGFic3RyYWN0ICA9IHtBIGNvbnRyb2xsZXIgZm9yIGEgRGlzY3JldGUgRXZlbnQgU3lzdGVtIG11c3QgYWNoaWV2ZSBpdHMgZ29hbHMgZGVzcGl0ZSB0aGF0IGl0cyBlbnZpcm9ubWVudCBiZWluZyBjYXBhYmxlIG9mIHJlc29sdmluZyByYWNlIGNvbmRpdGlvbnMgYmV0d2VlbiBjb250cm9sbGVkIGFuZCB1bmNvbnRyb2xsZWQgZXZlbnRzLkFzc3VtaW5nIHRoYXQgdGhlIGNvbnRyb2xsZXIgbG9zZXMgYWxsIHJhY2VzIGlzIHNvbWV0aW1lcyB1bnJlYWxpc3RpYy4gSW4gbWFueSBjYXNlcywgYSByZWFsaXN0aWMgYXNzdW1wdGlvbiBpcyB0aGF0IHRoZSBjb250cm9sbGVyIHNvbWV0aW1lcyB3aW5zIHJhY2VzIGFuZCBpcyBmYXN0IGVub3VnaCB0byBwZXJmb3JtIG11bHRpcGxlIGFjdGlvbnMgd2l0aG91dCBiZWluZyBpbnRlcnJ1cHRlZC4gSG93ZXZlciwgaW4gb3JkZXIgdG8gbW9kZWwgdGhpcyBzY2VuYXJpbyB1c2luZyBjb250cm9sIG9mIERFUyByZXF1aXJlcyBpbnRyb2R1Y2luZyBmb3JlaWduIGFzc3VtcHRpb25zIGFib3V0IHNjaGVkdWxpbmcsIHRoYXQgYXJlIGhhcmQgdG8gZmlndXJlIG91dCBjb3JyZWN0bHkuIFdlIHByb3Bvc2UgYSBtb3JlIGJhbGFuY2VkIGNvbnRyb2wgcHJvYmxlbSwgbmFtZWQgcnVuLXRvLWNvbXBsZXRpb24gKFJUQyksIHRvIGFsbGV2aWF0ZSB0aGlzIGlzc3VlLiBSVEMgbmF0dXJhbGx5IHN1cHBvcnRzIGFuIGV4ZWN1dGlvbiBhc3N1bXB0aW9uIGluIHdoaWNoIGJvdGggdGhlIGNvbnRyb2xsZXIgYW5kIHRoZSBlbnZpcm9ubWVudCBhcmUgZ3VhcmFudGVlZCB0byBpbml0aWF0ZSBhbmQgcGVyZm9ybSBzZXF1ZW5jZXMgb2YgYWN0aW9ucywgd2l0aG91dCBmbG9vZGluZyBvciBkZWxheWluZyBlYWNoIG90aGVyIGluZGVmaW5pdGVseS4gV2UgY29uc2lkZXIgY29udHJvbCBvZiBERVMgaW4gdGhlIGNvbnRleHQgd2hlcmUgc3BlY2lmaWNhdGlvbnMgYXJlIGdpdmVuIGluIHRoZSBmb3JtIG9mIGxpbmVhciB0ZW1wb3JhbCBsb2dpYy4gV2UgZm9ybWFsaXplIHRoZSBSVEMgY29udHJvbCBwcm9ibGVtIGFuZCBzaG93IGhvdyBpdCBjYW4gYmUgcmVkdWNlZCB0byBhIHN0YW5kYXJkIGNvbnRyb2wgcHJvYmxlbS59Cn0KCgoKQGlucHJvY2VlZGluZ3N7cmNwLAogIGF1dGhvciAgICA9IHtBYmQgQWxyYWhtYW4sIFllaGlhIGFuZCBQZXJlbGxpLCBHaXVzZXBwZSBhbmQgUGl0ZXJtYW4sIE5pcn0sCiAgdGl0bGUgICAgID0ge1JlY29uZmlndXJhYmxlIEludGVyYWN0aW9uIGZvciBNQVMgTW9kZWxsaW5nfSwKICB5ZWFyICAgICAgPSB7MjAyMH0sCiAgaXNibiAgICAgID0gezk3ODE0NTAzNzUxODR9LAogIHB1Ymxpc2hlciA9IHtJbnRlcm5hdGlvbmFsIEZvdW5kYXRpb24gZm9yIEF1dG9ub21vdXMgQWdlbnRzIGFuZCBNdWx0aWFnZW50IFN5c3RlbXN9LAogIGFkZHJlc3MgICA9IHtSaWNobGFuZCwgU0N9LAogIGJvb2t0aXRsZSA9IHtQcm9jZWVkaW5ncyBvZiB0aGUgMTl0aCBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2Ugb24gQXV0b25vbW91cyBBZ2VudHMgYW5kIE11bHRpQWdlbnQgU3lzdGVtc30sCiAgcGFnZXMgICAgID0gezctMTV9LAogIG51bXBhZ2VzICA9IHs5fSwKICBrZXl3b3JkcyAgPSB7dmVyaWZpY2F0aW9uIG9mIG11bHRpLWFnZW50IHN5c3RlbXMsIGxvZ2ljcyBmb3IgYWdlbnQgcmVhc29uaW5nLCBhZ2VudCB0aGVvcmllcyBhbmQgbW9kZWxzfSwKICBsb2NhdGlvbiAgPSB7QXVja2xhbmQsIE5ldyBaZWFsYW5kfSwKICBzZXJpZXMgICAgPSB7QUFNQVMgJzIwfSwKICB1cmwgICAgICAgPSB7aHR0cHM6Ly9kbC5hY20ub3JnL2RvaS9hYnMvMTAuNTU1NS8zMzk4NzYxLjMzOTg3Njh9LAogIGFic3RyYWN0ICA9IHtXZSBwcm9wb3NlIGEgZm9ybWFsaXNtIHRvIG1vZGVsIGFuZCByZWFzb24gYWJvdXQgbXVsdGktIGFnZW50IHN5c3RlbXMuIFdlIGFsbG93IGFnZW50cyB0byBpbnRlcmFjdCBhbmQgY29tbXVuaWNhdGUgaW4gZGlmZmVyZW50IG1vZGVzIHNvIHRoYXQgdGhleSBjYW4gcHVyc3VlIGpvaW50IHRhc2tzOyBhZ2VudHMgbWF5IGR5bmFtaWNhbGx5IHN5bmNocm9uaXplLCBleGNoYW5nZSBkYXRhLCBhZGFwdCB0aGVpciBiZWhhdmlvdXIsIGFuZCByZWNvbmZpZ3VyZSB0aGVpciBjb21tdW5pY2F0aW9uIGludGVyZmFjZXMuIFRoZSBmb3JtYWxpc20gZGVmaW5lcyBhIGxvY2FsIGJlaGF2aW91ciBiYXNlZCBvbiBzaGFyZWQgdmFyaWFibGVzIGFuZCBhIGdsb2JhbCBvbmUgYmFzZWQgb24gbWVzc2FnZSBwYXNzaW5nLiBXZSBleHRlbmQgTFRMIHRvIGJlIGFibGUgdG8gcmVhc29uIGV4cGxpY2l0bHkgYWJvdXQgdGhlIGludGVudGlvbnMgb2YgdGhlIGRpZmZlcmVudCBhZ2VudHMgYW5kIHRoZWlyIGludGVyYWN0aW9uIHByb3RvY29scy4gV2UgYWxzbyBzdHVkeSB0aGUgY29tcGxleGl0eSBvZiBzYXRpc2ZpYWJpbGl0eSBhbmQgbW9kZWwtY2hlY2tpbmcgb2YgdGhpcyBleHRlbnNpb24ufQp9CgoKCkBhcnRpY2xle0FiZF9BbHJhaG1hbl8yMDIwLAogIGRvaSAgICAgICA9IHsxMC4xMDA3L3MxMDAwOS0wMjAtMDA1NTMtNH0sCiAgdXJsICAgICAgID0ge2h0dHBzOi8vZG9pLm9yZy8xMC4xMDA3JTJGczEwMDA5LTAyMC0wMDU1My00fSwKICB5ZWFyICAgICAgPSB7MjAyMH0sCiAgbW9udGggICAgID0ge2ZlYn0sCiAgcHVibGlzaGVyID0ge1NwcmluZ2VyIFNjaWVuY2UgYW5kIEJ1c2luZXNzIE1lZGlhIHtMTEN9fSwKICBhdXRob3IgICAgPSB7WWVoaWEge0FiZCBBbHJhaG1hbn0gYW5kIEdpdWxpbyBHYXJiaX0sCiAgdGl0bGUgICAgID0ge0EgZGlzdHJpYnV0ZWQge0FQSX0gZm9yIGNvb3JkaW5hdGluZyB7QWJDfSBwcm9ncmFtc30sCiAgam91cm5hbCAgID0ge0ludGVybmF0aW9uYWwgSm91cm5hbCBvbiBTb2Z0d2FyZSBUb29scyBmb3IgVGVjaG5vbG9neSBUcmFuc2Zlcn0sCiAgYWJzdHJhY3QgID0ge0NvbGxlY3RpdmUtYWRhcHRpdmUgc3lzdGVtcyBleGhpYml0IGEgcGFydGljdWxhciBub3Rpb24gb2YgaW50ZXJhY3Rpb24gd2hlcmUgZW52aXJvbm1lbnRhbCBjb25kaXRpb25zIGxhcmdlbHkgaW5mbHVlbmNlIGludGVyYWN0aW9ucy4gUHJldmlvdXNseSwgd2UgcHJvLSBwb3NlZCBhIGNhbGN1bHVzLCBuYW1lZCBBYkMsIHRvIG1vZGVsIGFuZCByZWFzb24gYWJvdXQgQ0FTLiBUaGUgY2FsY3VsdXMgcHJvdmVkIHRvIGJlIGVmZmVjdGl2ZSBieSBuYXR1cmFsbHkgbW9kZWxsaW5nIGVzc2VudGlhbCBDQVMgZmVhdHVyZXMuIEhvd2V2ZXIsIHRoZSBxdWVzdGlvbiBvbiB0aGUgdHJhZGVvZmYgYmV0d2VlbiBpdHMgZXhwcmVzc2l2ZW5lc3MgYW5kIGl0cyBlZmZpY2llbmN5LCB3aGVuIGltcGxlbWVudGVkIHRvIHByb2dyYW0gQ0FTIGFwcGxpY2F0aW9ucywgaXMgdG8gYmUgYW5zd2VyZWQuIEluIHRoaXMgYXJ0aWNsZSwgd2UgcHJvcG9zZSBhbiBlZmZpY2llbnQgYW5kIGRpc3RyaWJ1dGVkIGNvb3JkaW5hdGlvbiBpbmZyYXN0cnVjdHVyZSBmb3IgQWJDLiBXZSBwcm92ZSBpdHMgY29ycmVjdG5lc3MgYW5kIHdlIGV2YWx1YXRlIGl0cyBwZXJmb3JtYW5jZS4gVGhlIG1haW4gbm92ZWx0eSBvZiBvdXIgYXBwcm9hY2ggaXMgdGhhdCBBYkMgY29tcG9uZW50cyBhcmUgaW5mcmFzdHJ1Y3R1cmUgYWdub3N0aWMuIFRodXMgdGhlIGNvZGUgb2YgYSBjb21wb25lbnQgZG9lcyBub3Qgc3BlY2lmeSBob3cgbWVzc2FnZXMgYXJlIHJvdXRlZCBpbiB0aGUgaW5mcmFzdHJ1Y3R1cmUgYnV0IHJhdGhlciB3aGF0IHByb3BlcnRpZXMgYSB0YXJnZXQgY29tcG9uZW50IG11c3Qgc2F0aXNmeS4gV2UgYWxzbyBkZXZlbG9wZWQgYSBHbyBBUEksIG5hbWVkIEdvQXQsIGFuZCBhbiBFY2xpcHNlIHBsdWdpbiB0byBwcm8tIGdyYW0gaW4gYSBoaWdoLWxldmVsIHN5bnRheCB3aGljaCBjYW4gYmUgYXV0b21hdGljYWxseSB1c2VkIHRvIGdlbmVyYXRlIG1hdGNoaW5nIEdvIGNvZGUuIFdlIHNob3djYXNlIG91ciBkZXZlbG9wbWVudCB0aHJvdWdoIGEgbm9uLXRyaXZpYWwgY2FzZSBzdHVkeS59Cn0KCgoKQGFydGljbGV7REJMUDphcnRpY2xlL3NjcC9BbHJhaG1hbk5MMjAsCiAgYXV0aG9yICAgPSB7WWVoaWEge0FiZCBBbHJhaG1hbn0gYW5kCiAgICAgICAgICAgICAgIFJvY2NvIHtEZSBOaWNvbGF9IGFuZAogICAgICAgICAgICAgICBNaWNoZWxlIExvcmV0aX0sCiAgdGl0bGUgICAgPSB7UHJvZ3JhbW1pbmcgaW50ZXJhY3Rpb25zIGluIGNvbGxlY3RpdmUgYWRhcHRpdmUgc3lzdGVtcyBieSByZWx5aW5nCiAgICAgICAgICAgICAgIG9uIGF0dHJpYnV0ZS1iYXNlZCBjb21tdW5pY2F0aW9ufSwKICBqb3VybmFsICA9IHtTY2kuIENvbXB1dC4gUHJvZ3JhbS59LAogIHZvbHVtZSAgID0gezE5Mn0sCiAgcGFnZXMgICAgPSB7MTAyNDI4fSwKICB5ZWFyICAgICA9IHsyMDIwfSwKICB1cmwgICAgICA9IHtodHRwczovL2RvaS5vcmcvMTAuMTAxNi9qLnNjaWNvLjIwMjAuMTAyNDI4fSwKICBkb2kgICAgICA9IHsxMC4xMDE2L2ouc2NpY28uMjAyMC4xMDI0Mjh9LAogIGFic3RyYWN0ID0ge0NvbGxlY3RpdmUgYWRhcHRpdmUgc3lzdGVtcyBhcmUgbmV3IGVtZXJnaW5nIGNvbXB1dGF0aW9uYWwgc3lzdGVtcyBjb25zaXN0aW5nIG9mIGEgbGFyZ2UgbnVtYmVyIG9mIGludGVyYWN0aW5nIGNvbXBvbmVudHMgYW5kIGZlYXR1cmluZyBjb21wbGV4IGJlaGF2aW91ci4gVGhlc2Ugc3lzdGVtcyBhcmUgdXN1YWxseSBkaXN0cmlidXRlZCwgaGV0ZXJvZ2VuZW91cywgZGVjZW50cmFsaXNlZCBhbmQgaW50ZXJkZXBlbmRlbnQsIGFuZCBhcmUgb3BlcmF0aW5nIGluIGR5bmFtaWMgYW5kIHBvc3NpYmx5IHVucHJlZGljdGFibGUgZW52aXJvbm1lbnRzLiBGaW5kaW5nIHdheXMgdG8gdW5kZXJzdGFuZCBhbmQgZGVzaWduIHRoZXNlIHN5c3RlbXMgYW5kLCBtb3N0IG9mIGFsbCwgdG8gbW9kZWwgdGhlIGludGVyYWN0aW9ucyBvZiB0aGVpciBjb21wb25lbnRzLCBpcyBhIGRpZmZpY3VsdCBidXQgaW1wb3J0YW50IGVuZGVhdm91ci4gSW4gdGhpcyBhcnRpY2xlIHdlIHByb3Bvc2UgYSBsYW5ndWFnZS1iYXNlZCBhcHByb2FjaCBmb3IgcHJvZ3JhbW1pbmcgdGhlIGludGVyYWN0aW9ucyBvZiBjb2xsZWN0aXZlLWFkYXB0aXZlIHN5c3RlbXMgYnkgcmVseWluZyBvbiBhdHRyaWJ1dGUtYmFzZWQgY29tbXVuaWNhdGlvbjsgYSBwYXJhZGlnbSB0aGF0IHBlcm1pdHMgYSBncm91cCBvZiBwYXJ0bmVycyB0byBjb21tdW5pY2F0ZSBieSBjb25zaWRlcmluZyB0aGVpciBydW4tdGltZSBwcm9wZXJ0aWVzIGFuZCBjYXBhYmlsaXRpZXMuIFdlIGludHJvZHVjZSBBYkMsIGEgZm91bmRhdGlvbmFsIGNhbGN1bHVzIGZvciBhdHRyaWJ1dGUtYmFzZWQgY29tbXVuaWNhdGlvbiBhbmQgc2hvdyBob3cgaXRzIGxpbmd1aXN0aWMgcHJpbWl0aXZlcyBjYW4gYmUgdXNlZCB0byBwcm9ncmFtIGEgY29tcGxleCBhbmQgc29waGlzdGljYXRlZCB2YXJpYW50IG9mIHRoZSB3ZWxsLWtub3duIHByb2JsZW0gb2YgU3RhYmxlIEFsbG9jYXRpb24gaW4gQ29udGVudCBEZWxpdmVyeSBOZXR3b3Jrcy4gQWxzbyBvdGhlciBpbnRlcmVzdGluZyBjYXNlIHN0dWRpZXMsIGZyb20gdGhlIHJlYWxtIG9mIGNvbGxlY3RpdmUtYWRhcHRpdmUgc3lzdGVtcywgYXJlIGNvbnNpZGVyZWQuIFdlIGFsc28gaWxsdXN0cmF0ZSB0aGUgZXhwcmVzc2l2ZSBwb3dlciBvZiBhdHRyaWJ1dGUtYmFzZWQgY29tbXVuaWNhdGlvbiBieSBzaG93aW5nIHRoZSBuYXR1cmFsIGVuY29kaW5nIG9mIG90aGVyIGV4aXN0aW5nIGNvbW11bmljYXRpb24gcGFyYWRpZ21zIGludG8gQWJDLn0KfQoKCgoKCkBhcnRpY2xle0RCTFA6YXJ0aWNsZS9pYW5kYy9BbHJhaG1hbk5MMTksCiAgYXV0aG9yICAgPSB7WWVoaWEge0FiZCBBbHJhaG1hbn0gYW5kCiAgICAgICAgICAgICAgIFJvY2NvIHtEZSBOaWNvbGF9IGFuZAogICAgICAgICAgICAgICBNaWNoZWxlIExvcmV0aX0sCiAgdGl0bGUgICAgPSB7QSBjYWxjdWx1cyBmb3IgY29sbGVjdGl2ZS1hZGFwdGl2ZSBzeXN0ZW1zIGFuZCBpdHMgYmVoYXZpb3VyYWwgdGhlb3J5fSwKICBqb3VybmFsICA9IHtJbmYuIENvbXB1dC59LAogIHZvbHVtZSAgID0gezI2OH0sCiAgeWVhciAgICAgPSB7MjAxOX0sCiAgdXJsICAgICAgPSB7aHR0cHM6Ly9kb2kub3JnLzEwLjEwMTYvai5pYy4yMDE5LjEwNDQ1N30sCiAgZG9pICAgICAgPSB7MTAuMTAxNi9qLmljLjIwMTkuMTA0NDU3fSwKICBhYnN0cmFjdCA9IHtXZSBwcm9wb3NlIGEgcHJvY2VzcyBjYWxjdWx1cywgbmFtZWQgQWJDLCB0byBzdHVkeSB0aGUgYmVoYXZpb3VyYWwgdGhlb3J5IG9mIGludGVyYWN0aW9ucyBpbiBjb2xsZWN0aXZlLWFkYXB0aXZlIHN5c3RlbXMgYnkgcmVseWluZyBvbiBhdHRyaWJ1dGUtYmFzZWQgY29tbXVuaWNhdGlvbi4gQW4gQWJDIHN5c3RlbSBjb25zaXN0cyBvZiBhIHNldCBvZiBwYXJhbGxlbCBjb21wb25lbnRzIGVhY2ggb2Ygd2hpY2ggaXMgZXF1aXBwZWQgd2l0aCBhIHNldCBvZiBhdHRyaWJ1dGVzLiBDb21tdW5pY2F0aW9uIHRha2VzIHBsYWNlIGluIGFuIGltcGxpY2l0IG11bHRpY2FzdCBmYXNoaW9uLCBhbmQgaW50ZXJhY3Rpb24gYW1vbmcgY29tcG9uZW50cyBpcyBkeW5hbWljYWxseSBlc3RhYmxpc2hlZCBieSB0YWtpbmcgaW50byBhY2NvdW50IGNvbm5lY3Rpb25zwp0gYXMgZGV0ZXJtaW5lZCBieSBwcmVkaWNhdGVzIG92ZXIgdGhlaXIgYXR0cmlidXRlcy4gVGhlIHN0cnVjdHVyYWwgb3BlcmF0aW9uYWwgc2VtYW50aWNzIG9mIEFiQyBpcyBiYXNlZCBvbiBMYWJlbGxlZCBUcmFuc2l0aW9uIFN5c3RlbXMgdGhhdCBhcmUgYWxzbyB1c2VkIHRvIGRlZmluZSBiaXNpbWlsYXJpdHkgYmV0d2VlbiBjb21wb25lbnRzLiBMYWJlbGxlZCBiaXNpbWlsYXJpdHkgaXMgaW4gZnVsbCBhZ3JlZW1lbnQgd2l0aCBhIGJhcmJlZCBjb25ncnVlbmNlLCBkZWZpbmVkIGJ5IHJlbHlpbmcgb24gc2ltcGxlIGJhc2ljIG9ic2VydmFibGVzIGFuZCBjb250ZXh0IGNsb3N1cmUuIFRoZSBpbnRyb2R1Y2VkIGVxdWl2YWxlbmNlIGlzIHVzZWQgdG8gc3R1ZHkgdGhlIGV4cHJlc3NpdmVuZXNzIG9mIEFiQyBpbiB0ZXJtcyBvZiBlbmNvZGluZyBhc3BlY3RzIG9mIGJyb2FkY2FzdCBjaGFubmVsLWJhc2VkIGludGVyYWN0aW9ucyBhbmQgdG8gZXN0YWJsaXNoIGZvcm1hbCByZWxhdGlvbnNoaXBzIGJldHdlZW4gc3lzdGVtIGRlc2NyaXB0aW9ucyBhdCBkaWZmZXJlbnQgbGV2ZWxzIG9mIGFic3RyYWN0aW9uLn0KfQoKCgoKCkBhcnRpY2xle0RCTFA6YXJ0aWNsZS9qbGFwL0FscmFobWFuVjE5LAogIGF1dGhvciAgID0ge1llaGlhIHtBYmQgQWxyYWhtYW59IGFuZAogICAgICAgICAgICAgICBIdWdvIFRvcnJlcyBWaWVpcmF9LAogIHRpdGxlICAgID0ge0EgY29vcmRpbmF0aW9uIHByb3RvY29sIGxhbmd1YWdlIGZvciBwb3dlciBncmlkIG9wZXJhdGlvbiBjb250cm9sfSwKICBqb3VybmFsICA9IHtKLiBMb2cuIEFsZ2VicmFpYyBNZXRob2RzIFByb2dyYW0ufSwKICB2b2x1bWUgICA9IHsxMDl9LAogIHllYXIgICAgID0gezIwMTl9LAogIHVybCAgICAgID0ge2h0dHBzOi8vZG9pLm9yZy8xMC4xMDE2L2ouamxhbXAuMjAxOS4xMDA0ODd9LAogIGRvaSAgICAgID0gezEwLjEwMTYvai5qbGFtcC4yMDE5LjEwMDQ4N30sCiAgYWJzdHJhY3QgPSB7RnV0dXJlIHBvd2VyIGRpc3RyaWJ1dGlvbiBncmlkcyB3aWxsIGNvbXByaXNlIGEgbGFyZ2UgbnVtYmVyIG9mIGNvbXBvbmVudHMsIGVhY2ggcG90ZW50aWFsbHkgYWJsZSB0byBjYXJyeSBvdXQgb3BlcmF0aW9ucyBhdXRvbm9tb3VzbHkuIENsZWFybHksIGluIG9yZGVyIHRvIGVuc3VyZSBzYWZlIG9wZXJhdGlvbiBvZiB0aGUgZ3JpZCwgaW5kaXZpZHVhbCBvcGVyYXRpb25zIG11c3QgYmUgY29vcmRpbmF0ZWQgYW1vbmcgdGhlIGRpZmZlcmVudCBjb21wb25lbnRzLiBTaW5jZSBvcGVyYXRpb24gc2FmZXR5IGlzIGEgZ2xvYmFsIHByb3BlcnR5LCBtb2RlbGxpbmcgY29tcG9uZW50IGNvb3JkaW5hdGlvbiB0eXBpY2FsbHkgaW52b2x2ZXMgcmVhc29uaW5nIGFib3V0IHN5c3RlbXMgYXQgYSBnbG9iYWwgbGV2ZWwuIEluIHRoaXMgcGFwZXIsIHdlIHByb3Bvc2UgYSBsYW5ndWFnZSBmb3Igc3BlY2lmeWluZyBncmlkIG9wZXJhdGlvbiBjb250cm9sIHByb3RvY29scyBmcm9tIGEgZ2xvYmFsIHBvaW50IG9mIHZpZXcuIEluIG91ciBtb2RlbCwgb3BlcmF0aW9uIGNvbnRyb2wgaXMgeWllbGRlZCBpbiBjb21tdW5pY2F0aW9ucyBkcml2ZW4gYnkgYm90aCB0aGUgZ3JpZCB0b3BvbG9neSBhbmQgYnkgc3RhdGUtYmFzZWQgaW5mb3JtYXRpb24sIGZlYXR1cmVzIGNhcHR1cmVkIGJ5IG5vdmVsIGxhbmd1YWdlIHByaW5jaXBsZXMgcHJldmlvdXNseSB1bmV4cGxvcmVkLiBXZSBzaG93IGhvdyB0aGUgZ2xvYmFsIHNwZWNpZmljYXRpb25zIGNhbiBiZSB1c2VkIHRvIGF1dG9tYXRpY2FsbHkgZ2VuZXJhdGUgbG9jYWwgY29udHJvbGxlcnMgb2YgaW5kaXZpZHVhbCBjb21wb25lbnRzLCBhbmQgdGhhdCB0aGUgZGlzdHJpYnV0ZWQgaW1wbGVtZW50YXRpb24geWllbGRlZCBieSBzdWNoIGNvbnRyb2xsZXJzIG9wZXJhdGlvbmFsbHkgY29ycmVzcG9uZHMgdG8gdGhlIGdsb2JhbCBzcGVjaWZpY2F0aW9uLiBXZSBzaG93Y2FzZSBvdXIgZGV2ZWxvcG1lbnQgYnkgbW9kZWxsaW5nIGEgZmF1bHQgbWFuYWdlbWVudCBzY2VuYXJpbyBpbiBwb3dlciBncmlkcy59Cn0KCgoKCgpAaW5wcm9jZWVkaW5nc3tEQkxQOmNvbmYvYmlydGhkYXkvQWxyYWhtYW5NVjE5LAogIGF1dGhvciAgICA9IHtZZWhpYSB7QWJkIEFscmFobWFufSBhbmQKICAgICAgICAgICAgICAgQ2xhdWRpbyBBbnRhcmVzIE1lenppbmEgYW5kCiAgICAgICAgICAgICAgIEh1Z28gVG9ycmVzIFZpZWlyYX0sCiAgZWRpdG9yICAgID0ge01pY2hlbGUgQm9yZWFsZSBhbmQKICAgICAgICAgICAgICAgRmxhdmlvIENvcnJhZGluaSBhbmQKICAgICAgICAgICAgICAgTWljaGVsZSBMb3JldGkgYW5kCiAgICAgICAgICAgICAgIFJvc2FyaW8gUHVnbGllc2V9LAogIHRpdGxlICAgICA9IHtUZXN0aW5nIGZvciBDb29yZGluYXRpb24gRmlkZWxpdHl9LAogIGJvb2t0aXRsZSA9IHtNb2RlbHMsIExhbmd1YWdlcywgYW5kIFRvb2xzIGZvciBDb25jdXJyZW50IGFuZCBEaXN0cmlidXRlZCBQcm9ncmFtbWluZwogICAgICAgICAgICAgICAtIEVzc2F5cyBEZWRpY2F0ZWQgdG8gUm9jY28gRGUgTmljb2xhIG9uIHRoZSBPY2Nhc2lvbiBvZiBIaXMgNjV0aAogICAgICAgICAgICAgICBCaXJ0aGRheX0sCiAgc2VyaWVzICAgID0ge0xlY3R1cmUgTm90ZXMgaW4gQ29tcHV0ZXIgU2NpZW5jZX0sCiAgdm9sdW1lICAgID0gezExNjY1fSwKICBwYWdlcyAgICAgPSB7MTUyLTE2OX0sCiAgcHVibGlzaGVyID0ge1NwcmluZ2VyfSwKICB5ZWFyICAgICAgPSB7MjAxOX0sCiAgdXJsICAgICAgID0ge2h0dHBzOi8vZG9pLm9yZy8xMC4xMDA3Lzk3OC0zLTAzMC0yMTQ4NS0yXF8xMH0sCiAgZG9pICAgICAgID0gezEwLjEwMDcvOTc4LTMtMDMwLTIxNDg1LTJcXzEwfSwKICBhYnN0cmFjdCAgPSB7T3BlcmF0aW9uIGNvbnRyb2wgaW4gbW9kZXJuIGRpc3RyaWJ1dGVkIHN5c3RlbXMgbXVzdCByZWx5IG9uIGRlY2VudHJhbGlzZWQgY29vcmRpbmF0aW9uIGFtb25nIHN5c3RlbSBwYXJ0aWNpcGFudHMuIEluIHBhcnRpY3VsYXIgd2hlbiB0aGUgb3BlcmF0aW9uIGNvbnRyb2wgaW52b2x2ZXMgY3JpdGljYWwgaW5mcmFzdHJ1Y3R1cmVzIHN1Y2ggYXMgcG93ZXIgZ3JpZHMsIGl0IGlzIHZpdGFsIHRvIGVuc3VyZSBjb3JyZWN0bmVzcyBwcm9wZXJ0aWVzIG9mIHN1Y2ggY29vcmRpbmF0aW9uIG1lY2hhbmlzbXMuIEluIHRoaXMgcGFwZXIsIHdlIHByZXNlbnQgYSB2ZXJpZmljYXRpb24gdGVjaG5pcXVlIHRoYXQgYWRkcmVzc2VzIGNvb3JkaW5hdGlvbiBwcm90b2NvbHMgZm9yIHBvd2VyIGdyaWQgb3BlcmF0aW9uIGNvbnRyb2wuIEdpdmVuIGEgZ2xvYmFsIHByb3RvY29sIHNwZWNpZmljYXRpb24sIHdlIHNob3cgaG93IHdlIGNhbiByZWx5IG9uIHRlc3Rpbmcgc2VtYW50aWNzIGZvciB0aGUgcHVycG9zZSBvZiBlbnN1cmluZyBwcm90b2NvbCBmaWRlbGl0eSwgaS5lLiwgdG8gY2VydGlmeSB0aGF0IHRoZSBpbnRlcmFjdGlvbiBhbW9uZyB0aGUgZ3JpZCBub2RlcyBmb2xsb3dzIHRoZSBwcm90b2NvbCBzcGVjaWZpY2F0aW9uLn0KfQoKCgoKCgoKCkBpbnByb2NlZWRpbmdze0RCTFA6Y29uZi9mb3J0ZS9BbHJhaG1hbk5HTDE4LAogIGF1dGhvciAgICA9IHtZZWhpYSB7QWJkIEFscmFobWFufSBhbmQKICAgICAgICAgICAgICAgUm9jY28ge0RlIE5pY29sYX0gYW5kCiAgICAgICAgICAgICAgIEdpdWxpbyBHYXJiaSBhbmQKICAgICAgICAgICAgICAgTWljaGVsZSBMb3JldGl9LAogIGVkaXRvciAgICA9IHtDaHJpc3RlbCBCYWllciBhbmQKICAgICAgICAgICAgICAgTHV7XCd7XGl9fXMgQ2FpcmVzfSwKICB0aXRsZSAgICAgPSB7QSBEaXN0cmlidXRlZCBDb29yZGluYXRpb24gSW5mcmFzdHJ1Y3R1cmUgZm9yIEF0dHJpYnV0ZS1CYXNlZCBJbnRlcmFjdGlvbn0sCiAgYm9va3RpdGxlID0ge0Zvcm1hbCBUZWNobmlxdWVzIGZvciBEaXN0cmlidXRlZCBPYmplY3RzLCBDb21wb25lbnRzLCBhbmQgU3lzdGVtcwogICAgICAgICAgICAgICAtIDM4dGgge0lGSVB9IHtXR30gNi4xIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZSwge0ZPUlRFfSAyMDE4LCBIZWxkCiAgICAgICAgICAgICAgIGFzIFBhcnQgb2YgdGhlIDEzdGggSW50ZXJuYXRpb25hbCBGZWRlcmF0ZWQgQ29uZmVyZW5jZSBvbiBEaXN0cmlidXRlZAogICAgICAgICAgICAgICBDb21wdXRpbmcgVGVjaG5pcXVlcywgRGlzQ29UZWMgMjAxOCwgTWFkcmlkLCBTcGFpbiwgSnVuZSAxOC0yMSwgMjAxOCwKICAgICAgICAgICAgICAgUHJvY2VlZGluZ3N9LAogIHNlcmllcyAgICA9IHtMZWN0dXJlIE5vdGVzIGluIENvbXB1dGVyIFNjaWVuY2V9LAogIHZvbHVtZSAgICA9IHsxMDg1NH0sCiAgcGFnZXMgICAgID0gezEtMjB9LAogIHB1Ymxpc2hlciA9IHtTcHJpbmdlcn0sCiAgeWVhciAgICAgID0gezIwMTh9LAogIHVybCAgICAgICA9IHtodHRwczovL2RvaS5vcmcvMTAuMTAwNy85NzgtMy0zMTktOTI2MTItNFxfMX0sCiAgZG9pICAgICAgID0gezEwLjEwMDcvOTc4LTMtMzE5LTkyNjEyLTRcXzF9LAogIGFic3RyYWN0ICA9IHtDb2xsZWN0aXZlLWFkYXB0aXZlIHN5c3RlbXMgb2ZmZXIgYW4gaW50ZXJlc3Rpbmcgbm90aW9uIG9mIGludGVyYWN0aW9uIHdoZXJlIHJ1bi10aW1lIGNvbnRleHR1YWwgZGF0YSBhcmUgdGhlIGRyaXZpbmcgZm9yY2UgZm9yIGludGVyYWN0aW9uLiBUaGUgYXR0cmlidXRlLWJhc2VkIGludGVyYWN0aW9uIGhhcyBiZWVuIHByb3Bvc2VkIGFzIGEgZm91bmRhdGlvbmFsIHRoZW9yZXRpY2FsIGZyYW1ld29yayB0byBtb2RlbCBDQVMgaW50ZXJhY3Rpb25zLiBUaGUgZnJhbWV3b3JrIHBlcm1pdHMgYSBncm91cCBvZiBwYXJ0bmVycyB0byBpbnRlcmFjdCBieSBjb25zaWRlcmluZyB0aGVpciBydW4tdGltZSBwcm9wZXJ0aWVzIGFuZCB0aGVpciBlbnZpcm9ubWVudC4gSW4gdGhpcyBwYXBlciwgd2UgbGF5IHRoZSBiYXNpcyBmb3IgYW4gZWZmaWNpZW50LCBjb3JyZWN0LCBhbmQgZGlzdHJpYnV0ZWQgaW1wbGVtZW50YXRpb24gb2YgdGhlIGF0dHJpYnV0ZS1iYXNlZCBpbnRlcmFjdGlvbiBmcmFtZXdvcmsuIEZpcnN0LCB3ZSBwcmVzZW50IHRocmVlIGNvb3JkaW5hdGlvbiBpbmZyYXN0cnVjdHVyZXMgZm9yIG1lc3NhZ2UgZXhjaGFuZ2UsIHRoZW4gd2UgcHJvdmUgdGhlaXIgY29ycmVjdG5lc3MsIGFuZCBmaW5hbGx5IHdlIG1vZGVsIHRoZW0gaW4gdGVybXMgb2Ygc3RvY2hhc3RpYyBwcm9jZXNzZXMgdG8gZXZhbHVhdGUgdGhlaXIgcGVyZm9ybWFuY2UufQp9CgoKCgoKQGlucHJvY2VlZGluZ3N7REJMUDpjb25mL2lzb2xhL0FscmFobWFuTkcxOCwKICBhdXRob3IgICAgPSB7WWVoaWEge0FiZCBBbHJhaG1hbn0gYW5kCiAgICAgICAgICAgICAgIFJvY2NvIHtEZSBOaWNvbGF9IGFuZAogICAgICAgICAgICAgICBHaXVsaW8gR2FyYml9LAogIGVkaXRvciAgICA9IHtUaXppYW5hIE1hcmdhcmlhIGFuZAogICAgICAgICAgICAgICBCZXJuaGFyZCBTdGVmZmVufSwKICB0aXRsZSAgICAgPSB7R29BdDogQXR0cmlidXRlLUJhc2VkIEludGVyYWN0aW9uIGluIEdvb2dsZSBHb30sCiAgYm9va3RpdGxlID0ge0xldmVyYWdpbmcgQXBwbGljYXRpb25zIG9mIEZvcm1hbCBNZXRob2RzLCBWZXJpZmljYXRpb24gYW5kIFZhbGlkYXRpb24uCiAgICAgICAgICAgICAgIERpc3RyaWJ1dGVkIFN5c3RlbXMgLSA4dGggSW50ZXJuYXRpb25hbCBTeW1wb3NpdW0sIElTb0xBIDIwMTgsIExpbWFzc29sLAogICAgICAgICAgICAgICBDeXBydXMsIE5vdmVtYmVyIDUtOSwgMjAxOCwgUHJvY2VlZGluZ3MsIFBhcnQge0lJSX19LAogIHNlcmllcyAgICA9IHtMZWN0dXJlIE5vdGVzIGluIENvbXB1dGVyIFNjaWVuY2V9LAogIHZvbHVtZSAgICA9IHsxMTI0Nn0sCiAgcGFnZXMgICAgID0gezI4OC0zMDN9LAogIHB1Ymxpc2hlciA9IHtTcHJpbmdlcn0sCiAgeWVhciAgICAgID0gezIwMTh9LAogIHVybCAgICAgICA9IHtodHRwczovL2RvaS5vcmcvMTAuMTAwNy85NzgtMy0wMzAtMDM0MjQtNVxfMTl9LAogIGRvaSAgICAgICA9IHsxMC4xMDA3Lzk3OC0zLTAzMC0wMzQyNC01XF8xOX0sCiAgYWJzdHJhY3QgID0ge1RoZSBhdHRyaWJ1dGUtYmFzZWQgaW50ZXJhY3Rpb24gcGFyYWRpZ20gaGFzIGJlZW4gcHJvcG9zZWQgYXMgYW4gYXBwcm9wcmlhdGUgdG9vbCB0byBwcm9ncmFtIHRoZSBpbnRlcmFjdGlvbnMgb2YgQ29sbGVjdGl2ZSBBZGFwdGl2ZSBTeXN0ZW1zIHdoZXJlIGEgZ3JvdXAgb2YgY29tcG9uZW50cyBjYW4gaW50ZXJhY3QgYWNjb3JkaW5nIHRvIHRoZWlyIHJ1bi10aW1lIHByb3BlcnRpZXMgYW5kIHRoZSBlbnZpcm9ubWVudCB0aGV5IG9wZXJhdGUgaW4uIEl0IGhhcyBiZWVuIHNob3duIHRoYXQgdGhlIG5vdmVsIHBhcmFkaWdtIGlzIHZlcnkgZXhwcmVzc2l2ZSBieSBtZWFucyBvZiBlbmNvZGluZyBvdGhlciB3ZWxsLWtub3duIGludGVyYWN0aW9uIHBhcmFkaWdtcy4gSG93ZXZlciwgdGhlIHF1ZXN0aW9uIG9uIHRoZSB0cmFkZW9mZiBiZXR3ZWVuIGl0cyBleHByZXNzaXZlbmVzcyBhbmQgaXRzIGVmZmljaWVuY3ksIHdoZW4gaW1wbGVtZW50ZWQgdG8gcHJvZ3JhbSBkaXN0cmlidXRlZCBhbmQgY29sbGVjdGl2ZSBzeXN0ZW1zLCBpcyBzdGlsbCB0byBiZSBhbnN3ZXJlZC4gSW4gYSBwcmV2aW91cyB3b3JrLCB3ZSBwcm9wb3NlZCB0aHJlZSBkaXN0cmlidXRlZCBjb21tdW5pY2F0aW9uIGluZnJhc3RydWN0dXJlcyB0byBoYW5kbGUgbWVzc2FnZSBleGNoYW5nZSBmb3IgdGhlIGF0dHJpYnV0ZS1iYXNlZCBwYXJhZGlnbSBhbmQgd2UgcHJvdmVkIHRoZWlyIGNvcnJlY3RuZXNzLiBJbiB0aGlzIHBhcGVyLCB3ZSBkZXNjcmliZSBhbiBhY3R1YWwgaW1wbGVtZW50YXRpb24gb2YgdGhlc2UgaW5mcmFzdHJ1Y3R1cmVzIGluIEdvb2dsZSBHby4gV2UgZGVzY3JpYmUgYW4gYXR0cmlidXRlLWJhc2VkIHByb2dyYW1taW5nIEFQSSwgbmFtZWQgR29BdCAsIHRoYXQgaXMgcGFyYW1ldHJpYyB3aXRoIHJlc3BlY3QgdG8gdGhlIGluZnJhc3RydWN0dXJlIHRoYXQgbWVkaWF0ZXMgdGhlIGludGVyYWN0aW9uIGJldHdlZW4gY29tcG9uZW50cyBhbmQgYW4gRWNsaXBzZSBwbHVnaW4gZm9yIEdvQXQgdG8gcHJvZ3JhbSBpbiBhIGhpZ2gtbGV2ZWwgc3ludGF4IHdoaWNoIGNhbiBiZSBhdXRvbWF0aWNhbGx5IHVzZWQgdG8gZ2VuZXJhdGUgZm9ybWFsbHkgdmVyaWZpYWJsZSBHbyBjb2RlLiBGaW5hbGx5LCB3ZSBkaXNjdXNzIHRoZSBwZXJmb3JtYW5jZSBvZiB0aGUgQVBJIGJ5IGNvbnNpZGVyaW5nIGEgbm9uLXRyaXZpYWwgY2FzZSBzdHVkeS59Cn0KCgoKCkBpbnByb2NlZWRpbmdze0RCTFA6Y29uZi9mb3J0ZS9BbHJhaG1hbk5MMTYsCiAgYXV0aG9yICAgID0ge1llaGlhIHtBYmQgQWxyYWhtYW59IGFuZAogICAgICAgICAgICAgICBSb2NjbyB7RGUgTmljb2xhfSBhbmQKICAgICAgICAgICAgICAgTWljaGVsZSBMb3JldGl9LAogIGVkaXRvciAgICA9IHtFbHZpcmEgQWxiZXJ0IGFuZAogICAgICAgICAgICAgICBJdmFuIExhbmVzZX0sCiAgdGl0bGUgICAgID0ge09uIHRoZSBQb3dlciBvZiBBdHRyaWJ1dGUtQmFzZWQgQ29tbXVuaWNhdGlvbn0sCiAgYm9va3RpdGxlID0ge0Zvcm1hbCBUZWNobmlxdWVzIGZvciBEaXN0cmlidXRlZCBPYmplY3RzLCBDb21wb25lbnRzLCBhbmQgU3lzdGVtcwogICAgICAgICAgICAgICAtIDM2dGgge0lGSVB9IHtXR30gNi4xIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZSwge0ZPUlRFfSAyMDE2LCBIZWxkCiAgICAgICAgICAgICAgIGFzIFBhcnQgb2YgdGhlIDExdGggSW50ZXJuYXRpb25hbCBGZWRlcmF0ZWQgQ29uZmVyZW5jZSBvbiBEaXN0cmlidXRlZAogICAgICAgICAgICAgICBDb21wdXRpbmcgVGVjaG5pcXVlcywgRGlzQ29UZWMgMjAxNiwgSGVyYWtsaW9uLCBDcmV0ZSwgR3JlZWNlLCBKdW5lCiAgICAgICAgICAgICAgIDYtOSwgMjAxNiwgUHJvY2VlZGluZ3N9LAogIHNlcmllcyAgICA9IHtMZWN0dXJlIE5vdGVzIGluIENvbXB1dGVyIFNjaWVuY2V9LAogIHZvbHVtZSAgICA9IHs5Njg4fSwKICBwYWdlcyAgICAgPSB7MS0xOH0sCiAgcHVibGlzaGVyID0ge1NwcmluZ2VyfSwKICB5ZWFyICAgICAgPSB7MjAxNn0sCiAgdXJsICAgICAgID0ge2h0dHBzOi8vZG9pLm9yZy8xMC4xMDA3Lzk3OC0zLTMxOS0zOTU3MC04XF8xfSwKICBkb2kgICAgICAgPSB7MTAuMTAwNy85NzgtMy0zMTktMzk1NzAtOFxfMX0sCiAgYWJzdHJhY3QgID0ge0luIG9wZW4gc3lzdGVtcyBleGhpYml0aW5nIGFkYXB0YXRpb24sIGJlaGF2aW9ycyBjYW4gYXJpc2UgYXMgc2lkZSBlZmZlY3RzIG9mIGludGVuc2l2ZSBjb21wb25lbnRzIGludGVyYWN0aW9uLiBGaW5kaW5nIHdheXMgdG8gdW5kZXJzdGFuZCBhbmQgZGVzaWduIHRoZXNlIHN5c3RlbXMsIGlzIGEgZGlmZmljdWx0IGJ1dCBpbXBvcnRhbnQgZW5kZWF2b3IuIFRvIHRhY2tsZSB0aGVzZSBpc3N1ZXMsIHdlIHByZXNlbnQgQWJDLCBhIGNhbGN1bHVzIGZvciBhdHRyaWJ1dGUtYmFzZWQgY29tbXVuaWNhdGlvbi4gQW4gQWJDIHN5c3RlbSBjb25zaXN0cyBvZiBhIHNldCBvZiBwYXJhbGxlbCBhZ2VudHMgZWFjaCBvZiB3aGljaCBpcyBlcXVpcHBlZCB3aXRoIGEgc2V0IG9mIGF0dHJpYnV0ZXMuIENvbW11bmljYXRpb24gdGFrZXMgcGxhY2UgaW4gYW4gaW1wbGljaXQgbXVsdGljYXN0IGZhc2hpb24sIGFuZCBpbnRlcmFjdGlvbnMgYW1vbmcgYWdlbnRzIGFyZSBkeW5hbWljYWxseSBlc3RhYmxpc2hlZCBieSB0YWtpbmcgaW50byBhY2NvdW50ICJjb25uZWN0aW9ucyIgYXMgZGV0ZXJtaW5lZCBieSBwcmVkaWNhdGVzIG92ZXIgdGhlIGF0dHJpYnV0ZXMgb2YgYWdlbnRzLiBGaXJzdCwgdGhlIHN5bnRheCBhbmQgdGhlIHNlbWFudGljcyBvZiB0aGUgY2FsY3VsdXMgYXJlIHByZXNlbnRlZCwgdGhlbiBleHByZXNzaXZlbmVzcyBhbmQgZWZmZWN0aXZlbmVzcyBvZiBBYkMgYXJlIGRlbW9uc3RyYXRlZCBib3RoIGluIHRlcm1zIG9mIG1vZGVsaW5nIHNjZW5hcmlvcyBmZWF0dXJpbmcgY29sbGFib3JhdGlvbiwgcmVjb25maWd1cmF0aW9uLCBhbmQgYWRhcHRhdGlvbiBhbmQgb2YgdGhlIHBvc3NpYmlsaXR5IG9mIGVuY29kaW5nIGNoYW5uZWwtYmFzZWQgaW50ZXJhY3Rpb25zIGFuZCBvdGhlciBpbnRlcmFjdGlvbiBwYXR0ZXJucy4gQmVoYXZpb3JhbCBlcXVpdmFsZW5jZXMgZm9yIEFiQyBhcmUgaW50cm9kdWNlZCBmb3IgZXN0YWJsaXNoaW5nIGZvcm1hbCByZWxhdGlvbnNoaXBzIGJldHdlZW4gZGlmZmVyZW50IGRlc2NyaXB0aW9ucyBvZiB0aGUgc2FtZSBzeXN0ZW0ufQp9CgoKCgoKQGlucHJvY2VlZGluZ3N7REJMUDpjb25mL2lzb2xhL0FscmFobWFuTkwxNiwKICBhdXRob3IgICAgPSB7WWVoaWEge0FiZCBBbHJhaG1hbn0gYW5kCiAgICAgICAgICAgICAgIFJvY2NvIHtEZSBOaWNvbGF9IGFuZAogICAgICAgICAgICAgICBNaWNoZWxlIExvcmV0aX0sCiAgZWRpdG9yICAgID0ge1RpemlhbmEgTWFyZ2FyaWEgYW5kCiAgICAgICAgICAgICAgIEJlcm5oYXJkIFN0ZWZmZW59LAogIHRpdGxlICAgICA9IHtQcm9ncmFtbWluZyBvZiB7Q0FTfSBTeXN0ZW1zIGJ5IFJlbHlpbmcgb24gQXR0cmlidXRlLUJhc2VkIENvbW11bmljYXRpb259LAogIGJvb2t0aXRsZSA9IHtMZXZlcmFnaW5nIEFwcGxpY2F0aW9ucyBvZiBGb3JtYWwgTWV0aG9kcywgVmVyaWZpY2F0aW9uIGFuZCBWYWxpZGF0aW9uOgogICAgICAgICAgICAgICBGb3VuZGF0aW9uYWwgVGVjaG5pcXVlcyAtIDd0aCBJbnRlcm5hdGlvbmFsIFN5bXBvc2l1bSwgSVNvTEEgMjAxNiwKICAgICAgICAgICAgICAgSW1wZXJpYWwsIENvcmZ1LCBHcmVlY2UsIE9jdG9iZXIgMTAtMTQsIDIwMTYsIFByb2NlZWRpbmdzLCBQYXJ0IHtJfX0sCiAgc2VyaWVzICAgID0ge0xlY3R1cmUgTm90ZXMgaW4gQ29tcHV0ZXIgU2NpZW5jZX0sCiAgdm9sdW1lICAgID0gezk5NTJ9LAogIHBhZ2VzICAgICA9IHs1MzktNTUzfSwKICB5ZWFyICAgICAgPSB7MjAxNn0sCiAgdXJsICAgICAgID0ge2h0dHBzOi8vZG9pLm9yZy8xMC4xMDA3Lzk3OC0zLTMxOS00NzE2Ni0yXF8zOH0sCiAgZG9pICAgICAgID0gezEwLjEwMDcvOTc4LTMtMzE5LTQ3MTY2LTJcXzM4fSwKICBhYnN0cmFjdCAgPSB7SW4gbW9zdCBkaXN0cmlidXRlZCBzeXN0ZW1zLCBuYW1lZCBjb25uZWN0aW9ucyAoaS5lLiwgY2hhbm5lbHMpIGFyZSB1c2VkIGFzIG1lYW5zIGZvciBwcm9ncmFtbWluZyBpbnRlcmFjdGlvbiBiZXR3ZWVuIGNvbW11bmljYXRpbmcgcGFydG5lcnMuIFRoZXNlIGtpbmRzIG9mIGNvbm5lY3Rpb25zIGFyZSBsb3cgbGV2ZWwgYW5kIHVzdWFsbHkgdG90YWxseSBpbmRlcGVuZGVudCBvZiB0aGUga25vd2xlZGdlLCB0aGUgc3RhdHVzLCB0aGUgY2FwYWJpbGl0aWVzLCAuLi4sIGluIG9uZSB3b3JkLCBvZiB0aGUgYXR0cmlidXRlcyBvZiB0aGUgaW50ZXJhY3RpbmcgcGFydG5lcnMuIFdlIGhhdmUgcmVjZW50bHkgaW50cm9kdWNlZCBhIGNhbGN1bHVzLCBjYWxsZWQgQWJDLCBpbiB3aGljaCBpbnRlcmFjdGlvbnMgYW1vbmcgYWdlbnRzIGFyZSBkeW5hbWljYWxseSBlc3RhYmxpc2hlZCBieSB0YWtpbmcgaW50byBhY2NvdW50ICJjb25uZWN0aW9uIiBhcyAgZGV0ZXJtaW5lZCBieSBwcmVkaWNhdGVzIG92ZXIgYWdlbnQgYXR0cmlidXRlcy4gSW4gdGhpcyBwYXBlciwgd2UgcHJlc2VudCBPcGVuIGltYWdlIGluIG5ldyB3aW5kb3cgLCBhIEphdmEgcnVuLXRpbWUgZW52aXJvbm1lbnQgdGhhdCBoYXMgYmVlbiBkZXZlbG9wZWQgdG8gc3VwcG9ydCBtb2RlbGluZyBhbmQgcHJvZ3JhbW1pbmcgb2YgY29sbGVjdGl2ZSBhZGFwdGl2ZSBzeXN0ZW1zIGJ5IHJlbHlpbmcgb24gdGhlIGNvbW11bmljYXRpb24gcHJpbWl0aXZlcyBvZiB0aGUgQWJDIGNhbGN1bHVzLiBTeXN0ZW1zIGFyZSBkZXNjcmliZWQgYXMgc2V0cyBvZiBwYXJhbGxlbCBjb21wb25lbnRzLCBlYWNoIGNvbXBvbmVudCBpcyBlcXVpcHBlZCB3aXRoIGEgc2V0IG9mIGF0dHJpYnV0ZXMgYW5kIGNvbW11bmljYXRpb25zIGFtb25nIGNvbXBvbmVudHMgdGFrZSBwbGFjZSBpbiBhbiBpbXBsaWNpdCBtdWx0aWNhc3QgZmFzaGlvbi4gQnkgbWVhbnMgb2YgYSBudW1iZXIgb2YgZXhhbXBsZXMsIHdlIGFsc28gc2hvdyBob3cgb3Bwb3J0dW5pc3RpYyBiZWhhdmlvcnMsIGFjaGlldmVkIGJ5IHJ1bi10aW1lIGF0dHJpYnV0ZSB1cGRhdGVzLCBjYW4gYmUgZXhwbG9pdGVkIHRvIGV4cHJlc3MgZGlmZmVyZW50IGNvbW11bmljYXRpb24gYW5kIGludGVyYWN0aW9uIHBhdHRlcm5zIGFuZCB0byBwcm9ncmFtIGNoYWxsZW5naW5nIGNhc2Ugc3R1ZGllcy59Cn0KCgoKCkBpbnByb2NlZWRpbmdze0RCTFA6Y29uZi9zYWMvQWxyYWhtYW5OTFRWMTUsCiAgYXV0aG9yICAgID0ge1llaGlhIHtBYmQgQWxyYWhtYW59IGFuZAogICAgICAgICAgICAgICBSb2NjbyB7RGUgTmljb2xhfSBhbmQKICAgICAgICAgICAgICAgTWljaGVsZSBMb3JldGkgYW5kCiAgICAgICAgICAgICAgIEZyYW5jZXNjbyBUaWV6emkgYW5kCiAgICAgICAgICAgICAgIFJvYmVydG8gVmlnb30sCiAgZWRpdG9yICAgID0ge1JvZ2VyIEwuIFdhaW53cmlnaHQgYW5kCiAgICAgICAgICAgICAgIEp1YW4gTWFudWVsIENvcmNoYWRvIGFuZAogICAgICAgICAgICAgICBBbGVzc2lvIEJlY2hpbmkgYW5kCiAgICAgICAgICAgICAgIEppbWFuIEhvbmd9LAogIHRpdGxlICAgICA9IHtBIGNhbGN1bHVzIGZvciBhdHRyaWJ1dGUtYmFzZWQgY29tbXVuaWNhdGlvbn0sCiAgYm9va3RpdGxlID0ge1Byb2NlZWRpbmdzIG9mIHRoZSAzMHRoIEFubnVhbCB7QUNNfSBTeW1wb3NpdW0gb24gQXBwbGllZCBDb21wdXRpbmcsCiAgICAgICAgICAgICAgIFNhbGFtYW5jYSwgU3BhaW4sIEFwcmlsIDEzLTE3LCAyMDE1fSwKICBwYWdlcyAgICAgPSB7MTg0MC0xODQ1fSwKICBwdWJsaXNoZXIgPSB7e0FDTX19LAogIHllYXIgICAgICA9IHsyMDE1fSwKICB1cmwgICAgICAgPSB7aHR0cHM6Ly9kb2kub3JnLzEwLjExNDUvMjY5NTY2NC4yNjk1NjY4fSwKICBkb2kgICAgICAgPSB7MTAuMTE0NS8yNjk1NjY0LjI2OTU2Njh9LAogIGFic3RyYWN0ICA9IHtUaGUgbm90aW9uIG9mIGF0dHJpYnV0ZS1iYXNlZCBjb21tdW5pY2F0aW9uIHNlZW1zIHByb21pc2luZyB0byBtb2RlbCBhbmQgYW5hbHlzZSBzeXN0ZW1zIHdpdGggaHVnZSBudW1iZXJzIG9mIGludGVyYWN0aW5nIGNvbXBvbmVudHMgdGhhdCBkeW5hbWljYWxseSBhZGp1c3QgYW5kIGNvbWJpbmUgdGhlaXIgYmVoYXZpb3VyIHRvIGFjaGlldmUgc3BlY2lmaWMgZ29hbHMuIEEgYmFzaWMgcHJvY2VzcyBjYWxjdWx1cywgbmFtZWQgQWJDLCBpcyBpbnRyb2R1Y2VkIHRoYXQgaGFzIGFzIHByaW1pdGl2ZSBjb25zdHJ1Y3QgZXhhY3RseSBhdHRyaWJ1dGUtYmFzZWQgY29tbXVuaWNhdGlvbiBhbmQgaXRzIGltcGFjdCBvbiB0aGUgYWJvdmUgbWVudGlvbmVkIGtpbmQgb2Ygc3lzdGVtcyBpcyBjb25zaWRlcmVkLiBBbiBBYkMgc3lzdGVtIGNvbnNpc3RzIG9mIGEgc2V0IG9mIHBhcmFsbGVsIGNvbXBvbmVudHMgZWFjaCBvZiB3aGljaCBpcyBlcXVpcHBlZCB3aXRoIGEgc2V0IG9mIGF0dHJpYnV0ZXMuIENvbW11bmljYXRpb24gdGFrZXMgcGxhY2UgaW4gYSBicm9hZGNhc3QgZmFzaGlvbiBhbmQgY29tbXVuaWNhdGlvbiBsaW5rcyBhbW9uZyBjb21wb25lbnRzIGFyZSBkeW5hbWljYWxseSBlc3RhYmxpc2hlZCBieSB0YWtpbmcgaW50byBhY2NvdW50IGludGVyZGVwZW5kZW5jZXMgZGV0ZXJtaW5lZCBieSBwcmVkaWNhdGVzIG92ZXIgYXR0cmlidXRlcy4gRmlyc3QsIHRoZSBzeW50YXggYW5kIHRoZSByZWR1Y3Rpb24gc2VtYW50aWNzIG9mIEFiQyBhcmUgcHJlc2VudGVkLCB0aGVuIGl0cyBleHByZXNzaXZlbmVzcyBhbmQgZWZmZWN0aXZlbmVzcyBpcyBkZW1vbnN0cmF0ZWQgYnkgbW9kZWxsaW5nIHR3byBzY2VuYXJpb3MgZnJvbSB0aGUgcmVhbG0gb2YgVFYgc3RyZWFtaW5nIGNoYW5uZWxzLiBBbiBleGFtcGxlIG9mIGhvdyB3ZWxsLWVzdGFibGlzaGVkIHByb2Nlc3MgY2FsY3VsaSBjb3VsZCBiZSBlbmNvZGVkIGludG8gQWJDIGlzIGdpdmVuIGJ5IGNvbnNpZGVyaW5nIHRoZSB0cmFuc2xhdGlvbiBpbnRvIEFiQyBvZiBhIHByb3RvdHlwaWNhbCDDj+KCrC1jYWxjdWx1cyBwcm9jZXNzLn0KfQoKCgoKCkBpbnByb2NlZWRpbmdze0RCTFA6Y29uZi93cmxhL0FscmFobWFuQUJMMTQsCiAgYXV0aG9yICAgID0ge1llaGlhIHtBYmQgQWxyYWhtYW59IGFuZAogICAgICAgICAgICAgICBNYXJpbmEgQW5kcmljIGFuZAogICAgICAgICAgICAgICBBbGVzc2FuZHJvIEJlZ2dpYXRvIGFuZAogICAgICAgICAgICAgICBBbGJlcnRvIExsdWNoey19TGFmdWVudGV9LAogIGVkaXRvciAgICA9IHtTYW50aWFnbyBFc2NvYmFyfSwKICB0aXRsZSAgICAgPSB7Q2FuIFdlIEVmZmljaWVudGx5IENoZWNrIENvbmN1cnJlbnQgUHJvZ3JhbXMgVW5kZXIgUmVsYXhlZCBNZW1vcnkKICAgICAgICAgICAgICAgTW9kZWxzIGluIE1hdWRlP30sCiAgYm9va3RpdGxlID0ge1Jld3JpdGluZyBMb2dpYyBhbmQgSXRzIEFwcGxpY2F0aW9ucyAtIDEwdGggSW50ZXJuYXRpb25hbCBXb3Jrc2hvcCwKICAgICAgICAgICAgICAge1dSTEF9IDIwMTQsIEhlbGQgYXMgYSBTYXRlbGxpdGUgRXZlbnQgb2YgRVRBUFMsIEdyZW5vYmxlLCBGcmFuY2UsCiAgICAgICAgICAgICAgIEFwcmlsIDUtNiwgMjAxNCwgUmV2aXNlZCBTZWxlY3RlZCBQYXBlcnN9LAogIHNlcmllcyAgICA9IHtMZWN0dXJlIE5vdGVzIGluIENvbXB1dGVyIFNjaWVuY2V9LAogIHZvbHVtZSAgICA9IHs4NjYzfSwKICBwYWdlcyAgICAgPSB7MjEtNDF9LAogIHB1Ymxpc2hlciA9IHtTcHJpbmdlcn0sCiAgeWVhciAgICAgID0gezIwMTR9LAogIHVybCAgICAgICA9IHtodHRwczovL2RvaS5vcmcvMTAuMTAwNy85NzgtMy0zMTktMTI5MDQtNFxfMn0sCiAgZG9pICAgICAgID0gezEwLjEwMDcvOTc4LTMtMzE5LTEyOTA0LTRcXzJ9LAogIGFic3RyYWN0ICA9IHtSZWxheGVkIG1lbW9yeSBtb2RlbHMgb2ZmZXIgc3VpdGFibGUgYWJzdHJhY3Rpb25zIG9mIHRoZSBhY3R1YWwgb3B0aW1pemF0aW9ucyBvZmZlcmVkIGJ5IG11bHRpLWNvcmUgYXJjaGl0ZWN0dXJlcyBhbmQgYnkgY29tcGlsZXJzIG9mIGNvbmN1cnJlbnQgcHJvZ3JhbW1pbmcgbGFuZ3VhZ2VzLiBVc2luZyBzdWNoIGFic3RyYWN0aW9ucyBmb3IgdmVyaWZpY2F0aW9uIHB1cnBvc2VzIGlzIGNoYWxsZW5naW5nIGluIHBhcnQgZHVlIHRvIHRoZWlyIGluaGVyZW50IG5vbi1kZXRlcm1pbmlzbSB3aGljaCBjb250cmlidXRlcyB0byB0aGUgc3RhdGUgc3BhY2UgZXhwbG9zaW9uLiBTZXZlcmFsIHRlY2huaXF1ZXMgaGF2ZSBiZWVuIHByb3Bvc2VkIHRvIG1pdGlnYXRlIHRob3NlIHByb2JsZW1zIHNvIHRvIG1ha2UgdmVyaWZpY2F0aW9uIHVuZGVyIHJlbGF4ZWQgbWVtb3J5IG1vZGVscyBmZWFzaWJsZS4gV2UgZGlzY3VzcyBob3cgdG8gYWRvcHQgc29tZSAgIG9mIHRob3NlIHRlY2huaXF1ZXMgaW4gYSBNYXVkZS1iYXNlZCBhcHByb2FjaCB0byBsYW5ndWFnZSBwcm90b3R5cGluZywgYW5kIHN1Z2dlc3QgdGhlIHVzZSBvZiBvdGhlciB0ZWNobmlxdWVzIHRoYXQgaGF2ZSBiZWVuIHNob3duIHN1Y2Nlc3NmdWwgZm9yIHNpbWlsYXIgdmVyaWZpY2F0aW9uIHB1cnBvc2VzLn0KfQo=\">\n            <i class=\"fa fa-download fa-fw\"></i> Download BibTeX\n          </a>\n        </li>\n        <li>\n          <a href=\"//bibbase.org/rss?bib=https://lazkany.bitbucket.io/publication.bib\">\n            <i class=\"fa fa-rss fa-fw\"></i> RSS Feed\n          </a>\n          </li>\n      </ul>\n      </li>\n\n      \n\n\n      \n    </ul>\n\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_embed\"\n         style=\"display: none;\">\n\n      Excellent! Next you can\n      <a href=\"/network/register?next=/network/newSiteFromTemplate%3Fbiburl=https://lazkany.bitbucket.io/publication.bib\"\n      >create a new website with this list</a>, or\n      embed it in an existing web page by copying &amp; pasting\n      any of the following snippets.\n\n      <div style=\"text-align: left; margin-top: 1em;\">\n        <strong>JavaScript</strong>\n        <span class=\"comment recommended\">(easiest)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;script src=\"https://bibbase.org/show?bib=https%3A%2F%2Flazkany.bitbucket.io%2Fpublication.bib&amp;jsonp=1&amp;css=assets/css/default.css&amp;jsonp=1\"&gt;&lt;/script&gt;\n          </code>\n        </div>\n\n        <strong>PHP</strong>\n        <div class=\"well well-small\">\n          <code>\n            &lt;?php\n            $contents = file_get_contents(\"https://bibbase.org/show?bib=https%3A%2F%2Flazkany.bitbucket.io%2Fpublication.bib&amp;jsonp=1&amp;css=assets/css/default.css\");\n            print_r($contents);\n            ?&gt;\n          </code>\n        </div>\n\n        <strong>iFrame</strong>\n        <span class=\"comment\">(not recommended)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;iframe src=\"https://bibbase.org/show?bib=https%3A%2F%2Flazkany.bitbucket.io%2Fpublication.bib&amp;jsonp=1&amp;css=assets/css/default.css\"&gt;&lt;/iframe&gt;\n          </code>\n        </div>\n\n        <p>\n          For more details see the <a href=\"//bibbase.org/help\">documention</a>.\n        </p>\n      </div>\n    </div>\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_preview\"\n         style=\"display: none;\">\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      <a href=\"/network/register?next=/network/newAccountWithFile%3FfileId=\"\n      >create a free account</a>. 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    </div>\n\n    <div class=\"alert alert-warning bibbase_msg\" id=\"bibbase_msg_mendeley1\"\n         style=\"display: none;\">\n\n      <p>To the site owner:</p>\n\n      <p><strong>Action required!</strong> Mendeley is changing its\n        API. In order to keep using Mendeley with BibBase past April\n        14th, you need to:\n        <ol>\n          <li>renew the authorization for BibBase on Mendeley, and</li>\n          <li>update the BibBase URL\n            in your page the same way you did when you initially set up\n            this page.\n          </li>\n        </ol>\n      </p>\n\n      <p>\n        <a href=\"http://bibbase.org/cgi-bin/mendeley2/get.py\">\n          <i class=\"fa fa-angle-double-right\"></i>\n          Fix it now</a>\n      </p>\n    </div>\n\n  </div>\n\n\n  <div id=\"bibbase_body\">\n    \n  \n  <div class=\"bibbase_group_whole\" id=\"group_2023\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2023')\"\n      onkeypress=\"toggleGroup('group_2023')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2023</span>\n      <span class=\"bibbase_group_count\">\n        \n        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"abdalrahman-azzopardi-distefano-piterman-languagesupportforverifyingreconfigurableinteractingsystems-2023\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Language Support for Verifying Reconfigurable Interacting Systems.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; Azzopardi, S.; Di Stefano, L.;  and Piterman, N.\n</span>\n\n  \n\n</span>\n\n  <i>International Journal on Software Tools for Technology Transfer</i>.  2023.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n  <a href=\"http://doi.org/10.1007/s10009-023-00729-8\"\n     onclick=\"log_download('abdalrahman-azzopardi-distefano-piterman-languagesupportforverifyingreconfigurableinteractingsystems-2023', 'http://doi.org/10.1007/s10009-023-00729-8', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-azzopardi-distefano-piterman-languagesupportforverifyingreconfigurableinteractingsystems-2023\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-azzopardi-distefano-piterman-languagesupportforverifyingreconfigurableinteractingsystems-2023')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@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</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"abdalrahman-piterman-correctbydesignteamworkplansformultiagentsystems-2023\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.48550/arXiv.2301.01257\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-piterman-correctbydesignteamworkplansformultiagentsystems-2023', 'https://doi.org/10.48550/arXiv.2301.01257', event);\">\n    Correct-by-Design Teamwork Plans for Multi-Agent Systems.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>;  and Piterman, N.\n</span>\n\n  \n\n</span>\n\n  <i>CoRR</i>, abs/2301.01257.  2023.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.48550/arXiv.2301.01257\"\n     onclick=\"log_download('abdalrahman-piterman-correctbydesignteamworkplansformultiagentsystems-2023', 'https://doi.org/10.48550/arXiv.2301.01257', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Correct-by-Design Teamwork Plans for Multi-Agent Systems [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.48550/arXiv.2301.01257\"\n     onclick=\"log_download('abdalrahman-piterman-correctbydesignteamworkplansformultiagentsystems-2023', 'http://doi.org/10.48550/arXiv.2301.01257', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-piterman-correctbydesignteamworkplansformultiagentsystems-2023\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-piterman-correctbydesignteamworkplansformultiagentsystems-2023')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{DBLP:journals/corr/abs-2301-01257,\n  author    = {Yehia {Abd Alrahman} and\n               Nir Piterman},\n  title     = {Correct-by-Design Teamwork Plans for Multi-Agent Systems},\n  journal   = {CoRR},\n  volume    = {abs/2301.01257},\n  year      = {2023},\n  url       = {https://doi.org/10.48550/arXiv.2301.01257},\n  doi       = {10.48550/arXiv.2301.01257},\n  eprinttype = {arXiv},\n  eprint    = {2301.01257}\n}\n</pre>\n</div>\n\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2022\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2022')\"\n      onkeypress=\"toggleGroup('group_2022')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2022</span>\n      <span class=\"bibbase_group_count\">\n        \n        (3)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"abdalrahman-martel-piterman-apocharacterisationofreconfiguration-2022\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://link.springer.com/chapter/10.1007/978-3-031-17715-6_5\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-martel-piterman-apocharacterisationofreconfiguration-2022', 'https://link.springer.com/chapter/10.1007/978-3-031-17715-6_5', event);\">\n    A PO Characterisation of Reconfiguration.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; Martel, M.;  and Piterman, N.\n</span>\n\n  \n\n</span>\n\n  In Seidl, H.; Liu, Z.;  and Pasareanu, C. S., editor(s), <i>Theoretical Aspects of Computing – ICTAC 2022</i>, pages 42–59, Cham,  2022. Springer International Publishing\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://link.springer.com/chapter/10.1007/978-3-031-17715-6_5\"\n     onclick=\"log_download('abdalrahman-martel-piterman-apocharacterisationofreconfiguration-2022', 'https://link.springer.com/chapter/10.1007/978-3-031-17715-6_5', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"A PO Characterisation of Reconfiguration [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-martel-piterman-apocharacterisationofreconfiguration-2022\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>1 download</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-martel-piterman-apocharacterisationofreconfiguration-2022')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@InProceedings{10.1007/978-3-031-17715-6_5,\nauthor=&quot;{Abd Alrahman}, Yehia\nand Martel, Mauricio\nand Piterman, Nir&quot;,\neditor=&quot;Seidl, Helmut\nand Liu, Zhiming\nand Pasareanu, Corina S.&quot;,\ntitle=&quot;A PO Characterisation of Reconfiguration&quot;,\nbooktitle=&quot;Theoretical Aspects of Computing -- ICTAC 2022&quot;,\nyear=&quot;2022&quot;,\npublisher=&quot;Springer International Publishing&quot;,\naddress=&quot;Cham&quot;,\npages=&quot;42--59&quot;,\nabstract=&quot;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.&quot;,\nisbn=&quot;978-3-031-17715-6&quot;,\nurl       = {https://link.springer.com/chapter/10.1007/978-3-031-17715-6_5}\n}\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"abdalrahman-azzopardi-piterman-rcheckamodelcheckerforverifyingreconfigurablemas-2022\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://dl.acm.org/doi/abs/10.5555/3535850.3536020\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-azzopardi-piterman-rcheckamodelcheckerforverifyingreconfigurablemas-2022', 'https://dl.acm.org/doi/abs/10.5555/3535850.3536020', event);\">\n    R-CHECK: A Model Checker for Verifying Reconfigurable MAS.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; Azzopardi, S.;  and Piterman, N.\n</span>\n\n  \n\n</span>\n\n  In Faliszewski, P.; Mascardi, V.; Pelachaud, C.;  and Taylor, M. E., editor(s), <i>21st International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2022, Auckland, New Zewland, May 9-13, 2022</i>, pages 1518–1520,  2022. International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS,ACM)\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://dl.acm.org/doi/abs/10.5555/3535850.3536020\"\n     onclick=\"log_download('abdalrahman-azzopardi-piterman-rcheckamodelcheckerforverifyingreconfigurablemas-2022', 'https://dl.acm.org/doi/abs/10.5555/3535850.3536020', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"R-CHECK: A Model Checker for Verifying Reconfigurable MAS [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-azzopardi-piterman-rcheckamodelcheckerforverifyingreconfigurablemas-2022\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>5 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-azzopardi-piterman-rcheckamodelcheckerforverifyingreconfigurablemas-2022')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"abdalrahman-azzopardi-piterman-modelcheckingreconfigurableinteractingsystems-2022\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://link.springer.com/chapter/10.1007/978-3-031-19759-8_23\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-azzopardi-piterman-modelcheckingreconfigurableinteractingsystems-2022', 'https://link.springer.com/chapter/10.1007/978-3-031-19759-8_23', event);\">\n    Model Checking Reconfigurable Interacting Systems.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; Azzopardi, S.;  and Piterman, N.\n</span>\n\n  \n\n</span>\n\n  In Margaria, T.;  and Steffen, B., editor(s), <i>Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning</i>, pages 373–389, Cham,  2022. Springer Nature Switzerland\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://link.springer.com/chapter/10.1007/978-3-031-19759-8_23\"\n     onclick=\"log_download('abdalrahman-azzopardi-piterman-modelcheckingreconfigurableinteractingsystems-2022', 'https://link.springer.com/chapter/10.1007/978-3-031-19759-8_23', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Model Checking Reconfigurable Interacting Systems [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-azzopardi-piterman-modelcheckingreconfigurableinteractingsystems-2022\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-azzopardi-piterman-modelcheckingreconfigurableinteractingsystems-2022')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@InProceedings{10.1007/978-3-031-19759-8_23,\nauthor=&quot;Abd Alrahman, Yehia\nand Azzopardi, Shaun\nand Piterman, Nir&quot;,\neditor=&quot;Margaria, Tiziana\nand Steffen, Bernhard&quot;,\ntitle=&quot;Model Checking Reconfigurable Interacting Systems&quot;,\nbooktitle=&quot;Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning&quot;,\nyear=&quot;2022&quot;,\npublisher=&quot;Springer Nature Switzerland&quot;,\naddress=&quot;Cham&quot;,\npages=&quot;373--389&quot;,\nabstract=&quot;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.&quot;,\nisbn=&quot;978-3-031-19759-8&quot;,\nurl={https://link.springer.com/chapter/10.1007/978-3-031-19759-8_23}\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2021\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2021')\"\n      onkeypress=\"toggleGroup('group_2021')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2021</span>\n      <span class=\"bibbase_group_count\">\n        \n        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"abdalrahman-piterman-modellingandverificationofreconfigurablemultiagentsystems-2021\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1007/s10458-021-09521-x\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-piterman-modellingandverificationofreconfigurablemultiagentsystems-2021', 'https://doi.org/10.1007/s10458-021-09521-x', event);\">\n    Modelling and verification of reconfigurable multi-agent systems.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>;  and Piterman, N.\n</span>\n\n  \n\n</span>\n\n  <i>Autonomous Agents and Multi Agent Systems</i>, 35(2): 47.  2021.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1007/s10458-021-09521-x\"\n     onclick=\"log_download('abdalrahman-piterman-modellingandverificationofreconfigurablemultiagentsystems-2021', 'https://doi.org/10.1007/s10458-021-09521-x', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Modelling and verification of reconfigurable multi-agent systems [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/s10458-021-09521-x\"\n     onclick=\"log_download('abdalrahman-piterman-modellingandverificationofreconfigurablemultiagentsystems-2021', 'http://doi.org/10.1007/s10458-021-09521-x', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-piterman-modellingandverificationofreconfigurablemultiagentsystems-2021\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>10 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-piterman-modellingandverificationofreconfigurablemultiagentsystems-2021')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{AlrahmanP21,\n  author    = {Yehia {Abd Alrahman} and\n               Nir Piterman},\n  title     = {Modelling and verification of reconfigurable multi-agent systems},\n  journal   = {Autonomous Agents and Multi Agent Systems},\n  volume    = {35},\n  number    = {2},\n  pages     = {47},\n  year      = {2021},\n  url       = {https://doi.org/10.1007/s10458-021-09521-x},\n  doi       = {10.1007/s10458-021-09521-x},\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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"abdalrahman-braberman-dippolito-piterman-uchitel-synthesisofruntocompletioncontrollersfordiscreteeventsystems-2021\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.23919/ACC50511.2021.9482704\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-braberman-dippolito-piterman-uchitel-synthesisofruntocompletioncontrollersfordiscreteeventsystems-2021', 'https://doi.org/10.23919/ACC50511.2021.9482704', event);\">\n    Synthesis of Run-To-Completion Controllers for Discrete Event Systems.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; Braberman, V. A.; D'Ippolito, N.; <a class=\"bibbase author link\" href=\"https://www.cse.chalmers.se/~piterman/publications/index.html\">Piterman, N.</a>;  and Uchitel, S.\n</span>\n\n  \n\n</span>\n\n  In <i>2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021</i>, pages 4892–4899,  2021. IEEE\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.23919/ACC50511.2021.9482704\"\n     onclick=\"log_download('abdalrahman-braberman-dippolito-piterman-uchitel-synthesisofruntocompletioncontrollersfordiscreteeventsystems-2021', 'https://doi.org/10.23919/ACC50511.2021.9482704', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Synthesis of Run-To-Completion Controllers for Discrete Event Systems [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.23919/ACC50511.2021.9482704\"\n     onclick=\"log_download('abdalrahman-braberman-dippolito-piterman-uchitel-synthesisofruntocompletioncontrollersfordiscreteeventsystems-2021', 'http://doi.org/10.23919/ACC50511.2021.9482704', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-braberman-dippolito-piterman-uchitel-synthesisofruntocompletioncontrollersfordiscreteeventsystems-2021\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>10 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-braberman-dippolito-piterman-uchitel-synthesisofruntocompletioncontrollersfordiscreteeventsystems-2021')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{acc,\n  author    = {Yehia {Abd Alrahman} and\n               V{\\&#x27;{\\i}}ctor A. Braberman and\n               Nicol{\\&#x27;{a}}s D&#x27;Ippolito and\n               Nir Piterman and\n               Sebasti{\\&#x27;{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</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\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</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2020\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2020')\"\n      onkeypress=\"toggleGroup('group_2020')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2020</span>\n      <span class=\"bibbase_group_count\">\n        \n        (3)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"abdalrahman-perelli-piterman-reconfigurableinteractionformasmodelling-2020\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://dl.acm.org/doi/abs/10.5555/3398761.3398768\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-perelli-piterman-reconfigurableinteractionformasmodelling-2020', 'https://dl.acm.org/doi/abs/10.5555/3398761.3398768', event);\">\n    Reconfigurable Interaction for MAS Modelling.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; <a class=\"bibbase author link\" href=\"https://giuseppeperelli.github.io/oldsite/\">Perelli, G.</a>;  and <a class=\"bibbase author link\" href=\"https://www.cse.chalmers.se/~piterman/publications/index.html\">Piterman, N.</a>\n</span>\n\n  \n\n</span>\n\n  In <i>Proceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems</i>, of <i>AAMAS '20</i>, pages 7-15, Richland, SC,  2020. International Foundation for Autonomous Agents and Multiagent Systems\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://dl.acm.org/doi/abs/10.5555/3398761.3398768\"\n     onclick=\"log_download('abdalrahman-perelli-piterman-reconfigurableinteractionformasmodelling-2020', 'https://dl.acm.org/doi/abs/10.5555/3398761.3398768', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Reconfigurable Interaction for MAS Modelling [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-perelli-piterman-reconfigurableinteractionformasmodelling-2020\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>29 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-perelli-piterman-reconfigurableinteractionformasmodelling-2020')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{rcp,\n  author    = {Abd Alrahman, Yehia and Perelli, Giuseppe and Piterman, Nir},\n  title     = {Reconfigurable Interaction for MAS Modelling},\n  year      = {2020},\n  isbn      = {9781450375184},\n  publisher = {International Foundation for Autonomous Agents and Multiagent Systems},\n  address   = {Richland, SC},\n  booktitle = {Proceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems},\n  pages     = {7-15},\n  numpages  = {9},\n  keywords  = {verification of multi-agent systems, logics for agent reasoning, agent theories and models},\n  location  = {Auckland, New Zealand},\n  series    = {AAMAS &#x27;20},\n  url       = {https://dl.acm.org/doi/abs/10.5555/3398761.3398768},\n  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.}\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  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.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"abdalrahman-garbi-adistributedapiforcoordinatingabcprograms-2020\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1007%2Fs10009-020-00553-4\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-garbi-adistributedapiforcoordinatingabcprograms-2020', 'https://doi.org/10.1007%2Fs10009-020-00553-4', event);\">\n    A distributed API for coordinating AbC programs.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>;  and Garbi, G.\n</span>\n\n  \n\n</span>\n\n  <i>International Journal on Software Tools for Technology Transfer</i>. feb 2020.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1007%2Fs10009-020-00553-4\"\n     onclick=\"log_download('abdalrahman-garbi-adistributedapiforcoordinatingabcprograms-2020', 'https://doi.org/10.1007%2Fs10009-020-00553-4', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"A distributed API for coordinating AbC programs [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/s10009-020-00553-4\"\n     onclick=\"log_download('abdalrahman-garbi-adistributedapiforcoordinatingabcprograms-2020', 'http://doi.org/10.1007/s10009-020-00553-4', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-garbi-adistributedapiforcoordinatingabcprograms-2020\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>2 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-garbi-adistributedapiforcoordinatingabcprograms-2020')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{Abd_Alrahman_2020,\n  doi       = {10.1007/s10009-020-00553-4},\n  url       = {https://doi.org/10.1007%2Fs10009-020-00553-4},\n  year      = {2020},\n  month     = {feb},\n  publisher = {Springer Science and Business Media {LLC}},\n  author    = {Yehia {Abd Alrahman} and Giulio Garbi},\n  title     = {A distributed {API} for coordinating {AbC} programs},\n  journal   = {International Journal on Software Tools for Technology Transfer},\n  abstract  = {Collective-adaptive systems exhibit a particular notion of interaction where environmental conditions largely influence interactions. Previously, we pro- posed a calculus, named AbC, to model and reason about CAS. The calculus proved to be effective by naturally modelling essential CAS features. However, the question on the tradeoff between its expressiveness and its efficiency, when implemented to program CAS applications, is to be answered. In this article, we propose an efficient and distributed coordination infrastructure for AbC. We prove its correctness and we evaluate its performance. The main novelty of our approach is that AbC components are infrastructure agnostic. Thus the code of a component does not specify how messages are routed in the infrastructure but rather what properties a target component must satisfy. We also developed a Go API, named GoAt, and an Eclipse plugin to pro- gram in a high-level syntax which can be automatically used to generate matching Go code. We showcase our development through a non-trivial case study.}\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Collective-adaptive systems exhibit a particular notion of interaction where environmental conditions largely influence interactions. Previously, we pro- posed a calculus, named AbC, to model and reason about CAS. The calculus proved to be effective by naturally modelling essential CAS features. However, the question on the tradeoff between its expressiveness and its efficiency, when implemented to program CAS applications, is to be answered. In this article, we propose an efficient and distributed coordination infrastructure for AbC. We prove its correctness and we evaluate its performance. The main novelty of our approach is that AbC components are infrastructure agnostic. Thus the code of a component does not specify how messages are routed in the infrastructure but rather what properties a target component must satisfy. We also developed a Go API, named GoAt, and an Eclipse plugin to pro- gram in a high-level syntax which can be automatically used to generate matching Go code. We showcase our development through a non-trivial case study.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"abdalrahman-denicola-loreti-programminginteractionsincollectiveadaptivesystemsbyrelyingonattributebasedcommunication-2020\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1016/j.scico.2020.102428\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-denicola-loreti-programminginteractionsincollectiveadaptivesystemsbyrelyingonattributebasedcommunication-2020', 'https://doi.org/10.1016/j.scico.2020.102428', event);\">\n    Programming interactions in collective adaptive systems by relying on attribute-based communication.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; De Nicola, R.;  and Loreti, M.\n</span>\n\n  \n\n</span>\n\n  <i>Sci. Comput. Program.</i>, 192: 102428.  2020.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1016/j.scico.2020.102428\"\n     onclick=\"log_download('abdalrahman-denicola-loreti-programminginteractionsincollectiveadaptivesystemsbyrelyingonattributebasedcommunication-2020', 'https://doi.org/10.1016/j.scico.2020.102428', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Programming interactions in collective adaptive systems by relying on attribute-based communication [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1016/j.scico.2020.102428\"\n     onclick=\"log_download('abdalrahman-denicola-loreti-programminginteractionsincollectiveadaptivesystemsbyrelyingonattributebasedcommunication-2020', 'http://doi.org/10.1016/j.scico.2020.102428', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-denicola-loreti-programminginteractionsincollectiveadaptivesystemsbyrelyingonattributebasedcommunication-2020\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>1 download</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-denicola-loreti-programminginteractionsincollectiveadaptivesystemsbyrelyingonattributebasedcommunication-2020')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{DBLP:article/scp/AlrahmanNL20,\n  author   = {Yehia {Abd Alrahman} and\n               Rocco {De Nicola} and\n               Michele Loreti},\n  title    = {Programming interactions in collective adaptive systems by relying\n               on attribute-based communication},\n  journal  = {Sci. Comput. Program.},\n  volume   = {192},\n  pages    = {102428},\n  year     = {2020},\n  url      = {https://doi.org/10.1016/j.scico.2020.102428},\n  doi      = {10.1016/j.scico.2020.102428},\n  abstract = {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 complex and sophisticated variant of the well-known problem of Stable Allocation in Content Delivery Networks. Also other interesting case studies, from the realm of collective-adaptive systems, are considered. We also illustrate the expressive power of attribute-based communication by showing the natural encoding of other existing communication paradigms into AbC.}\n}\n\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  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 complex and sophisticated variant of the well-known problem of Stable Allocation in Content Delivery Networks. Also other interesting case studies, from the realm of collective-adaptive systems, are considered. We also illustrate the expressive power of attribute-based communication by showing the natural encoding of other existing communication paradigms into AbC.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2019\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2019')\"\n      onkeypress=\"toggleGroup('group_2019')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2019</span>\n      <span class=\"bibbase_group_count\">\n        \n        (3)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"abdalrahman-denicola-loreti-acalculusforcollectiveadaptivesystemsanditsbehaviouraltheory-2019\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1016/j.ic.2019.104457\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-denicola-loreti-acalculusforcollectiveadaptivesystemsanditsbehaviouraltheory-2019', 'https://doi.org/10.1016/j.ic.2019.104457', event);\">\n    A calculus for collective-adaptive systems and its behavioural theory.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; De Nicola, R.;  and Loreti, M.\n</span>\n\n  \n\n</span>\n\n  <i>Inf. Comput.</i>, 268.  2019.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1016/j.ic.2019.104457\"\n     onclick=\"log_download('abdalrahman-denicola-loreti-acalculusforcollectiveadaptivesystemsanditsbehaviouraltheory-2019', 'https://doi.org/10.1016/j.ic.2019.104457', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"A calculus for collective-adaptive systems and its behavioural theory [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1016/j.ic.2019.104457\"\n     onclick=\"log_download('abdalrahman-denicola-loreti-acalculusforcollectiveadaptivesystemsanditsbehaviouraltheory-2019', 'http://doi.org/10.1016/j.ic.2019.104457', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-denicola-loreti-acalculusforcollectiveadaptivesystemsanditsbehaviouraltheory-2019\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>3 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-denicola-loreti-acalculusforcollectiveadaptivesystemsanditsbehaviouraltheory-2019')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{DBLP:article/iandc/AlrahmanNL19,\n  author   = {Yehia {Abd Alrahman} and\n               Rocco {De Nicola} and\n               Michele Loreti},\n  title    = {A calculus for collective-adaptive systems and its behavioural theory},\n  journal  = {Inf. Comput.},\n  volume   = {268},\n  year     = {2019},\n  url      = {https://doi.org/10.1016/j.ic.2019.104457},\n  doi      = {10.1016/j.ic.2019.104457},\n  abstract = {We propose a process calculus, named AbC, to study the behavioural theory of interactions in collective-adaptive systems by relying on attribute-based communication. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interaction among components is dynamically established by taking into account connections as determined by predicates over their attributes. The structural operational semantics of AbC is based on Labelled Transition Systems that are also used to define bisimilarity between components. Labelled bisimilarity is in full agreement with a barbed congruence, defined by relying on simple basic observables and context closure. The introduced equivalence is used to study the expressiveness of AbC in terms of encoding aspects of broadcast channel-based interactions and to establish formal relationships between system descriptions at different levels of abstraction.}\n}\n\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  We propose a process calculus, named AbC, to study the behavioural theory of interactions in collective-adaptive systems by relying on attribute-based communication. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interaction among components is dynamically established by taking into account connections as determined by predicates over their attributes. The structural operational semantics of AbC is based on Labelled Transition Systems that are also used to define bisimilarity between components. Labelled bisimilarity is in full agreement with a barbed congruence, defined by relying on simple basic observables and context closure. The introduced equivalence is used to study the expressiveness of AbC in terms of encoding aspects of broadcast channel-based interactions and to establish formal relationships between system descriptions at different levels of abstraction.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"abdalrahman-vieira-acoordinationprotocollanguageforpowergridoperationcontrol-2019\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1016/j.jlamp.2019.100487\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-vieira-acoordinationprotocollanguageforpowergridoperationcontrol-2019', 'https://doi.org/10.1016/j.jlamp.2019.100487', event);\">\n    A coordination protocol language for power grid operation control.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>;  and Vieira, H. T.\n</span>\n\n  \n\n</span>\n\n  <i>J. Log. Algebraic Methods Program.</i>, 109.  2019.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1016/j.jlamp.2019.100487\"\n     onclick=\"log_download('abdalrahman-vieira-acoordinationprotocollanguageforpowergridoperationcontrol-2019', 'https://doi.org/10.1016/j.jlamp.2019.100487', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"A coordination protocol language for power grid operation control [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1016/j.jlamp.2019.100487\"\n     onclick=\"log_download('abdalrahman-vieira-acoordinationprotocollanguageforpowergridoperationcontrol-2019', 'http://doi.org/10.1016/j.jlamp.2019.100487', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-vieira-acoordinationprotocollanguageforpowergridoperationcontrol-2019\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>4 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-vieira-acoordinationprotocollanguageforpowergridoperationcontrol-2019')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{DBLP:article/jlap/AlrahmanV19,\n  author   = {Yehia {Abd Alrahman} and\n               Hugo Torres Vieira},\n  title    = {A coordination protocol language for power grid operation control},\n  journal  = {J. Log. Algebraic Methods Program.},\n  volume   = {109},\n  year     = {2019},\n  url      = {https://doi.org/10.1016/j.jlamp.2019.100487},\n  doi      = {10.1016/j.jlamp.2019.100487},\n  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.}\n}\n\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  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.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"abdalrahman-mezzina-vieira-testingforcoordinationfidelity-2019\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1007/978-3-030-21485-2\\_10\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-mezzina-vieira-testingforcoordinationfidelity-2019', 'https://doi.org/10.1007/978-3-030-21485-2\\_10', event);\">\n    Testing for Coordination Fidelity.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; Mezzina, C. A.;  and Vieira, H. T.\n</span>\n\n  \n\n</span>\n\n  In Boreale, M.; Corradini, F.; Loreti, M.;  and Pugliese, R., editor(s), <i>Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday</i>, volume 11665, of <i>Lecture Notes in Computer Science</i>, pages 152-169,  2019. Springer\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1007/978-3-030-21485-2\\_10\"\n     onclick=\"log_download('abdalrahman-mezzina-vieira-testingforcoordinationfidelity-2019', 'https://doi.org/10.1007/978-3-030-21485-2\\_10', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Testing for Coordination Fidelity [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-030-21485-2_10\"\n     onclick=\"log_download('abdalrahman-mezzina-vieira-testingforcoordinationfidelity-2019', 'http://doi.org/10.1007/978-3-030-21485-2_10', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-mezzina-vieira-testingforcoordinationfidelity-2019\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>3 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-mezzina-vieira-testingforcoordinationfidelity-2019')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{DBLP:conf/birthday/AlrahmanMV19,\n  author    = {Yehia {Abd Alrahman} and\n               Claudio Antares Mezzina and\n               Hugo Torres Vieira},\n  editor    = {Michele Boreale and\n               Flavio Corradini and\n               Michele Loreti and\n               Rosario Pugliese},\n  title     = {Testing for Coordination Fidelity},\n  booktitle = {Models, Languages, and Tools for Concurrent and Distributed Programming\n               - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th\n               Birthday},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {11665},\n  pages     = {152-169},\n  publisher = {Springer},\n  year      = {2019},\n  url       = {https://doi.org/10.1007/978-3-030-21485-2\\_10},\n  doi       = {10.1007/978-3-030-21485-2\\_10},\n  abstract  = {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.}\n}\n\n\n\n\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  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.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2018\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2018')\"\n      onkeypress=\"toggleGroup('group_2018')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2018</span>\n      <span class=\"bibbase_group_count\">\n        \n        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"abdalrahman-denicola-garbi-loreti-adistributedcoordinationinfrastructureforattributebasedinteraction-2018\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1007/978-3-319-92612-4\\_1\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-denicola-garbi-loreti-adistributedcoordinationinfrastructureforattributebasedinteraction-2018', 'https://doi.org/10.1007/978-3-319-92612-4\\_1', event);\">\n    A Distributed Coordination Infrastructure for Attribute-Based Interaction.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; De Nicola, R.; Garbi, G.;  and Loreti, M.\n</span>\n\n  \n\n</span>\n\n  In Baier, C.;  and Caires, L., editor(s), <i>Formal Techniques for Distributed Objects, Components, and Systems - 38th IFIP WG 6.1 International Conference, FORTE 2018, Held as Part of the 13th International Federated Conference on Distributed Computing Techniques, DisCoTec 2018, Madrid, Spain, June 18-21, 2018, Proceedings</i>, volume 10854, of <i>Lecture Notes in Computer Science</i>, pages 1-20,  2018. Springer\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1007/978-3-319-92612-4\\_1\"\n     onclick=\"log_download('abdalrahman-denicola-garbi-loreti-adistributedcoordinationinfrastructureforattributebasedinteraction-2018', 'https://doi.org/10.1007/978-3-319-92612-4\\_1', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"A Distributed Coordination Infrastructure for Attribute-Based Interaction [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-319-92612-4_1\"\n     onclick=\"log_download('abdalrahman-denicola-garbi-loreti-adistributedcoordinationinfrastructureforattributebasedinteraction-2018', 'http://doi.org/10.1007/978-3-319-92612-4_1', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-denicola-garbi-loreti-adistributedcoordinationinfrastructureforattributebasedinteraction-2018\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-denicola-garbi-loreti-adistributedcoordinationinfrastructureforattributebasedinteraction-2018')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{DBLP:conf/forte/AlrahmanNGL18,\n  author    = {Yehia {Abd Alrahman} and\n               Rocco {De Nicola} and\n               Giulio Garbi and\n               Michele Loreti},\n  editor    = {Christel Baier and\n               Lu{\\&#x27;{\\i}}s Caires},\n  title     = {A Distributed Coordination Infrastructure for Attribute-Based Interaction},\n  booktitle = {Formal Techniques for Distributed Objects, Components, and Systems\n               - 38th {IFIP} {WG} 6.1 International Conference, {FORTE} 2018, Held\n               as Part of the 13th International Federated Conference on Distributed\n               Computing Techniques, DisCoTec 2018, Madrid, Spain, June 18-21, 2018,\n               Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {10854},\n  pages     = {1-20},\n  publisher = {Springer},\n  year      = {2018},\n  url       = {https://doi.org/10.1007/978-3-319-92612-4\\_1},\n  doi       = {10.1007/978-3-319-92612-4\\_1},\n  abstract  = {Collective-adaptive systems offer an interesting notion of interaction where run-time contextual data are the driving force for interaction. The attribute-based interaction has been proposed as a foundational theoretical framework to model CAS interactions. The framework permits a group of partners to interact by considering their run-time properties and their environment. In this paper, we lay the basis for an efficient, correct, and distributed implementation of the attribute-based interaction framework. First, we present three coordination infrastructures for message exchange, then we prove their correctness, and finally we model them in terms of stochastic processes to evaluate their performance.}\n}\n\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Collective-adaptive systems offer an interesting notion of interaction where run-time contextual data are the driving force for interaction. The attribute-based interaction has been proposed as a foundational theoretical framework to model CAS interactions. The framework permits a group of partners to interact by considering their run-time properties and their environment. In this paper, we lay the basis for an efficient, correct, and distributed implementation of the attribute-based interaction framework. First, we present three coordination infrastructures for message exchange, then we prove their correctness, and finally we model them in terms of stochastic processes to evaluate their performance.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"abdalrahman-denicola-garbi-goatattributebasedinteractioningooglego-2018\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1007/978-3-030-03424-5\\_19\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-denicola-garbi-goatattributebasedinteractioningooglego-2018', 'https://doi.org/10.1007/978-3-030-03424-5\\_19', event);\">\n    GoAt: Attribute-Based Interaction in Google Go.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; De Nicola, R.;  and Garbi, G.\n</span>\n\n  \n\n</span>\n\n  In Margaria, T.;  and Steffen, B., editor(s), <i>Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III</i>, volume 11246, of <i>Lecture Notes in Computer Science</i>, pages 288-303,  2018. Springer\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1007/978-3-030-03424-5\\_19\"\n     onclick=\"log_download('abdalrahman-denicola-garbi-goatattributebasedinteractioningooglego-2018', 'https://doi.org/10.1007/978-3-030-03424-5\\_19', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"GoAt: Attribute-Based Interaction in Google Go [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-030-03424-5_19\"\n     onclick=\"log_download('abdalrahman-denicola-garbi-goatattributebasedinteractioningooglego-2018', 'http://doi.org/10.1007/978-3-030-03424-5_19', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-denicola-garbi-goatattributebasedinteractioningooglego-2018\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-denicola-garbi-goatattributebasedinteractioningooglego-2018')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{DBLP:conf/isola/AlrahmanNG18,\n  author    = {Yehia {Abd Alrahman} and\n               Rocco {De Nicola} and\n               Giulio Garbi},\n  editor    = {Tiziana Margaria and\n               Bernhard Steffen},\n  title     = {GoAt: Attribute-Based Interaction in Google Go},\n  booktitle = {Leveraging Applications of Formal Methods, Verification and Validation.\n               Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol,\n               Cyprus, November 5-9, 2018, Proceedings, Part {III}},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {11246},\n  pages     = {288-303},\n  publisher = {Springer},\n  year      = {2018},\n  url       = {https://doi.org/10.1007/978-3-030-03424-5\\_19},\n  doi       = {10.1007/978-3-030-03424-5\\_19},\n  abstract  = {The attribute-based interaction paradigm has been proposed as an appropriate tool to program the interactions of Collective Adaptive Systems where a group of components can interact according to their run-time properties and the environment they operate in. It has been shown that the novel paradigm is very expressive by means of encoding other well-known interaction paradigms. However, the question on the tradeoff between its expressiveness and its efficiency, when implemented to program distributed and collective systems, is still to be answered. In a previous work, we proposed three distributed communication infrastructures to handle message exchange for the attribute-based paradigm and we proved their correctness. In this paper, we describe an actual implementation of these infrastructures in Google Go. We describe an attribute-based programming API, named GoAt , that is parametric with respect to the infrastructure that mediates the interaction between components and an Eclipse plugin for GoAt to program in a high-level syntax which can be automatically used to generate formally verifiable Go code. Finally, we discuss the performance of the API by considering a non-trivial case study.}\n}\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  The attribute-based interaction paradigm has been proposed as an appropriate tool to program the interactions of Collective Adaptive Systems where a group of components can interact according to their run-time properties and the environment they operate in. It has been shown that the novel paradigm is very expressive by means of encoding other well-known interaction paradigms. However, the question on the tradeoff between its expressiveness and its efficiency, when implemented to program distributed and collective systems, is still to be answered. In a previous work, we proposed three distributed communication infrastructures to handle message exchange for the attribute-based paradigm and we proved their correctness. In this paper, we describe an actual implementation of these infrastructures in Google Go. We describe an attribute-based programming API, named GoAt , that is parametric with respect to the infrastructure that mediates the interaction between components and an Eclipse plugin for GoAt to program in a high-level syntax which can be automatically used to generate formally verifiable Go code. Finally, we discuss the performance of the API by considering a non-trivial case study.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2016\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2016')\"\n      onkeypress=\"toggleGroup('group_2016')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2016</span>\n      <span class=\"bibbase_group_count\">\n        \n        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"abdalrahman-denicola-loreti-onthepowerofattributebasedcommunication-2016\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1007/978-3-319-39570-8\\_1\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-denicola-loreti-onthepowerofattributebasedcommunication-2016', 'https://doi.org/10.1007/978-3-319-39570-8\\_1', event);\">\n    On the Power of Attribute-Based Communication.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; De Nicola, R.;  and Loreti, M.\n</span>\n\n  \n\n</span>\n\n  In Albert, E.;  and Lanese, I., editor(s), <i>Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings</i>, volume 9688, of <i>Lecture Notes in Computer Science</i>, pages 1-18,  2016. Springer\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1007/978-3-319-39570-8\\_1\"\n     onclick=\"log_download('abdalrahman-denicola-loreti-onthepowerofattributebasedcommunication-2016', 'https://doi.org/10.1007/978-3-319-39570-8\\_1', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"On the Power of Attribute-Based Communication [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-319-39570-8_1\"\n     onclick=\"log_download('abdalrahman-denicola-loreti-onthepowerofattributebasedcommunication-2016', 'http://doi.org/10.1007/978-3-319-39570-8_1', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-denicola-loreti-onthepowerofattributebasedcommunication-2016\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-denicola-loreti-onthepowerofattributebasedcommunication-2016')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{DBLP:conf/forte/AlrahmanNL16,\n  author    = {Yehia {Abd Alrahman} and\n               Rocco {De Nicola} and\n               Michele Loreti},\n  editor    = {Elvira Albert and\n               Ivan Lanese},\n  title     = {On the Power of Attribute-Based Communication},\n  booktitle = {Formal Techniques for Distributed Objects, Components, and Systems\n               - 36th {IFIP} {WG} 6.1 International Conference, {FORTE} 2016, Held\n               as Part of the 11th International Federated Conference on Distributed\n               Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June\n               6-9, 2016, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {9688},\n  pages     = {1-18},\n  publisher = {Springer},\n  year      = {2016},\n  url       = {https://doi.org/10.1007/978-3-319-39570-8\\_1},\n  doi       = {10.1007/978-3-319-39570-8\\_1},\n  abstract  = {In open systems exhibiting adaptation, behaviors can arise as side effects of intensive components interaction. Finding ways to understand and design these systems, is a difficult but important endeavor. To tackle these issues, we present AbC, a calculus for attribute-based communication. An AbC system consists of a set of parallel agents each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interactions among agents are dynamically established by taking into account &quot;connections&quot; as determined by predicates over the attributes of agents. First, the syntax and the semantics of the calculus are presented, then expressiveness and effectiveness of AbC are demonstrated both in terms of modeling scenarios featuring collaboration, reconfiguration, and adaptation and of the possibility of encoding channel-based interactions and other interaction patterns. Behavioral equivalences for AbC are introduced for establishing formal relationships between different descriptions of the same system.}\n}\n\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  In open systems exhibiting adaptation, behaviors can arise as side effects of intensive components interaction. Finding ways to understand and design these systems, is a difficult but important endeavor. To tackle these issues, we present AbC, a calculus for attribute-based communication. An AbC system consists of a set of parallel agents each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interactions among agents are dynamically established by taking into account \"connections\" as determined by predicates over the attributes of agents. First, the syntax and the semantics of the calculus are presented, then expressiveness and effectiveness of AbC are demonstrated both in terms of modeling scenarios featuring collaboration, reconfiguration, and adaptation and of the possibility of encoding channel-based interactions and other interaction patterns. Behavioral equivalences for AbC are introduced for establishing formal relationships between different descriptions of the same system.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"abdalrahman-denicola-loreti-programmingofcassystemsbyrelyingonattributebasedcommunication-2016\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1007/978-3-319-47166-2\\_38\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-denicola-loreti-programmingofcassystemsbyrelyingonattributebasedcommunication-2016', 'https://doi.org/10.1007/978-3-319-47166-2\\_38', event);\">\n    Programming of CAS Systems by Relying on Attribute-Based Communication.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; De Nicola, R.;  and Loreti, M.\n</span>\n\n  \n\n</span>\n\n  In Margaria, T.;  and Steffen, B., editor(s), <i>Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I</i>, volume 9952, of <i>Lecture Notes in Computer Science</i>, pages 539-553,  2016. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1007/978-3-319-47166-2\\_38\"\n     onclick=\"log_download('abdalrahman-denicola-loreti-programmingofcassystemsbyrelyingonattributebasedcommunication-2016', 'https://doi.org/10.1007/978-3-319-47166-2\\_38', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Programming of CAS Systems by Relying on Attribute-Based Communication [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-319-47166-2_38\"\n     onclick=\"log_download('abdalrahman-denicola-loreti-programmingofcassystemsbyrelyingonattributebasedcommunication-2016', 'http://doi.org/10.1007/978-3-319-47166-2_38', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-denicola-loreti-programmingofcassystemsbyrelyingonattributebasedcommunication-2016\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-denicola-loreti-programmingofcassystemsbyrelyingonattributebasedcommunication-2016')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{DBLP:conf/isola/AlrahmanNL16,\n  author    = {Yehia {Abd Alrahman} and\n               Rocco {De Nicola} and\n               Michele Loreti},\n  editor    = {Tiziana Margaria and\n               Bernhard Steffen},\n  title     = {Programming of {CAS} Systems by Relying on Attribute-Based Communication},\n  booktitle = {Leveraging Applications of Formal Methods, Verification and Validation:\n               Foundational Techniques - 7th International Symposium, ISoLA 2016,\n               Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part {I}},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {9952},\n  pages     = {539-553},\n  year      = {2016},\n  url       = {https://doi.org/10.1007/978-3-319-47166-2\\_38},\n  doi       = {10.1007/978-3-319-47166-2\\_38},\n  abstract  = {In most distributed systems, named connections (i.e., channels) are used as means for programming interaction between communicating partners. These kinds of connections are low level and usually totally independent of the knowledge, the status, the capabilities, ..., in one word, of the attributes of the interacting partners. We have recently introduced a calculus, called AbC, in which interactions among agents are dynamically established by taking into account &quot;connection&quot; as  determined by predicates over agent attributes. In this paper, we present Open image in new window , a Java run-time environment that has been developed to support modeling and programming of collective adaptive systems by relying on the communication primitives of the AbC calculus. Systems are described as sets of parallel components, each component is equipped with a set of attributes and communications among components take place in an implicit multicast fashion. By means of a number of examples, we also show how opportunistic behaviors, achieved by run-time attribute updates, can be exploited to express different communication and interaction patterns and to program challenging case studies.}\n}\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  In most distributed systems, named connections (i.e., channels) are used as means for programming interaction between communicating partners. These kinds of connections are low level and usually totally independent of the knowledge, the status, the capabilities, ..., in one word, of the attributes of the interacting partners. We have recently introduced a calculus, called AbC, in which interactions among agents are dynamically established by taking into account \"connection\" as determined by predicates over agent attributes. In this paper, we present Open image in new window , a Java run-time environment that has been developed to support modeling and programming of collective adaptive systems by relying on the communication primitives of the AbC calculus. Systems are described as sets of parallel components, each component is equipped with a set of attributes and communications among components take place in an implicit multicast fashion. By means of a number of examples, we also show how opportunistic behaviors, achieved by run-time attribute updates, can be exploited to express different communication and interaction patterns and to program challenging case studies.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2015\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2015')\"\n      onkeypress=\"toggleGroup('group_2015')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2015</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"abdalrahman-denicola-loreti-tiezzi-vigo-acalculusforattributebasedcommunication-2015\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1145/2695664.2695668\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-denicola-loreti-tiezzi-vigo-acalculusforattributebasedcommunication-2015', 'https://doi.org/10.1145/2695664.2695668', event);\">\n    A calculus for attribute-based communication.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; De Nicola, R.; Loreti, M.; Tiezzi, F.;  and Vigo, R.\n</span>\n\n  \n\n</span>\n\n  In Wainwright, R. L.; Corchado, J. M.; Bechini, A.;  and Hong, J., editor(s), <i>Proceedings of the 30th Annual ACM Symposium on Applied Computing, Salamanca, Spain, April 13-17, 2015</i>, pages 1840-1845,  2015. ACM\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1145/2695664.2695668\"\n     onclick=\"log_download('abdalrahman-denicola-loreti-tiezzi-vigo-acalculusforattributebasedcommunication-2015', 'https://doi.org/10.1145/2695664.2695668', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"A calculus for attribute-based communication [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1145/2695664.2695668\"\n     onclick=\"log_download('abdalrahman-denicola-loreti-tiezzi-vigo-acalculusforattributebasedcommunication-2015', 'http://doi.org/10.1145/2695664.2695668', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-denicola-loreti-tiezzi-vigo-acalculusforattributebasedcommunication-2015\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-denicola-loreti-tiezzi-vigo-acalculusforattributebasedcommunication-2015')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{DBLP:conf/sac/AlrahmanNLTV15,\n  author    = {Yehia {Abd Alrahman} and\n               Rocco {De Nicola} and\n               Michele Loreti and\n               Francesco Tiezzi and\n               Roberto Vigo},\n  editor    = {Roger L. Wainwright and\n               Juan Manuel Corchado and\n               Alessio Bechini and\n               Jiman Hong},\n  title     = {A calculus for attribute-based communication},\n  booktitle = {Proceedings of the 30th Annual {ACM} Symposium on Applied Computing,\n               Salamanca, Spain, April 13-17, 2015},\n  pages     = {1840-1845},\n  publisher = {{ACM}},\n  year      = {2015},\n  url       = {https://doi.org/10.1145/2695664.2695668},\n  doi       = {10.1145/2695664.2695668},\n  abstract  = {The notion of attribute-based communication seems promising to model and analyse systems with huge numbers of interacting components that dynamically adjust and combine their behaviour to achieve specific goals. A basic process calculus, named AbC, is introduced that has as primitive construct exactly attribute-based communication and its impact on the above mentioned kind of systems is considered. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in a broadcast fashion and communication links among components are dynamically established by taking into account interdependences determined by predicates over attributes. First, the syntax and the reduction semantics of AbC are presented, then its expressiveness and effectiveness is demonstrated by modelling two scenarios from the realm of TV streaming channels. An example of how well-established process calculi could be encoded into AbC is given by considering the translation into AbC of a prototypical Ï€-calculus process.}\n}\n\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  The notion of attribute-based communication seems promising to model and analyse systems with huge numbers of interacting components that dynamically adjust and combine their behaviour to achieve specific goals. A basic process calculus, named AbC, is introduced that has as primitive construct exactly attribute-based communication and its impact on the above mentioned kind of systems is considered. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in a broadcast fashion and communication links among components are dynamically established by taking into account interdependences determined by predicates over attributes. First, the syntax and the reduction semantics of AbC are presented, then its expressiveness and effectiveness is demonstrated by modelling two scenarios from the realm of TV streaming channels. An example of how well-established process calculi could be encoded into AbC is given by considering the translation into AbC of a prototypical Ï€-calculus process.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2014\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2014')\"\n      onkeypress=\"toggleGroup('group_2014')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2014</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://doi.org/10.1007/978-3-319-12904-4\\_2\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014', 'https://doi.org/10.1007/978-3-319-12904-4\\_2', event);\">\n    Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://lazkany.bitbucket.io/\">Abd Alrahman, Y.</a>; Andric, M.; Beggiato, A.;  and Lluch-Lafuente, A.\n</span>\n\n  \n\n</span>\n\n  In Escobar, S., editor(s), <i>Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Revised Selected Papers</i>, volume 8663, of <i>Lecture Notes in Computer Science</i>, pages 21-41,  2014. Springer\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://doi.org/10.1007/978-3-319-12904-4\\_2\"\n     onclick=\"log_download('abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014', 'https://doi.org/10.1007/978-3-319-12904-4\\_2', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude? [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-319-12904-4_2\"\n     onclick=\"log_download('abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014', 'http://doi.org/10.1007/978-3-319-12904-4_2', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{DBLP:conf/wrla/AlrahmanABL14,\n  author    = {Yehia {Abd Alrahman} and\n               Marina Andric and\n               Alessandro Beggiato and\n               Alberto Lluch{-}Lafuente},\n  editor    = {Santiago Escobar},\n  title     = {Can We Efficiently Check Concurrent Programs Under Relaxed Memory\n               Models in Maude?},\n  booktitle = {Rewriting Logic and Its Applications - 10th International Workshop,\n               {WRLA} 2014, Held as a Satellite Event of ETAPS, Grenoble, France,\n               April 5-6, 2014, Revised Selected Papers},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {8663},\n  pages     = {21-41},\n  publisher = {Springer},\n  year      = {2014},\n  url       = {https://doi.org/10.1007/978-3-319-12904-4\\_2},\n  doi       = {10.1007/978-3-319-12904-4\\_2},\n  abstract  = {Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some   of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.}\n}\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n\n\n\n  </div>\n\n\n  <!-- Modal -->\n\n  <!-- <iframe id=\"bibbase_network_frame\" -->\n  <!--         src=\"//bibbase.org/network/control\" -->\n  <!--         style=\"display: none;\"> -->\n  <!-- </iframe> -->\n\n</div>\n"}; document.write(bibbase_data.data);