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

\n For more details see the documention.\n

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

To the site owner:

\n\n

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

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

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2024\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Symbolic Solution of Emerson-Lei Games for Reactive Synthesis.\n \n \n \n \n\n\n \n Hausmann, D., Lehaut, M., & Piterman, N.\n\n\n \n\n\n\n In Kobayashi, N., & Worrell, J., editor(s), Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14574, of Lecture Notes in Computer Science, pages 55–78, 2024. Springer\n \n\n\n\n
\n\n\n\n \n \n \"SymbolicPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/fossacs/HausmannLP24,\n  author       = {Daniel Hausmann and\n                  Mathieu Lehaut and\n                  Nir Piterman},\n  editor       = {Naoki Kobayashi and\n                  James Worrell},\n  title        = {Symbolic Solution of Emerson-Lei Games for Reactive Synthesis},\n  booktitle    = {Foundations of Software Science and Computation Structures - 27th\n                  International Conference, FoSSaCS 2024, Held as Part of the European\n                  Joint Conferences on Theory and Practice of Software, {ETAPS} 2024,\n                  Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part {I}},\n  series       = {Lecture Notes in Computer Science},\n  volume       = {14574},\n  pages        = {55--78},\n  publisher    = {Springer},\n  year         = {2024},\n  url          = {https://doi.org/10.1007/978-3-031-57228-9\\_4},\n  doi          = {10.1007/978-3-031-57228-9\\_4},\n  timestamp    = {Sun, 14 Apr 2024 18:32:17 +0200},\n  biburl       = {https://dblp.org/rec/conf/fossacs/HausmannLP24.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Fair $ω$-Regular Games.\n \n \n \n \n\n\n \n Hausmann, D., Piterman, N., Saglam, I., & Schmuck, A.\n\n\n \n\n\n\n In Kobayashi, N., & Worrell, J., editor(s), Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14574, of Lecture Notes in Computer Science, pages 13–33, 2024. Springer\n \n\n\n\n
\n\n\n\n \n \n \"FairPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/fossacs/HausmannPSS24,\n  author       = {Daniel Hausmann and\n                  Nir Piterman and\n                  Irmak Saglam and\n                  Anne{-}Kathrin Schmuck},\n  editor       = {Naoki Kobayashi and\n                  James Worrell},\n  title        = {Fair $\\omega$-Regular Games},\n  booktitle    = {Foundations of Software Science and Computation Structures - 27th\n                  International Conference, FoSSaCS 2024, Held as Part of the European\n                  Joint Conferences on Theory and Practice of Software, {ETAPS} 2024,\n                  Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part {I}},\n  series       = {Lecture Notes in Computer Science},\n  volume       = {14574},\n  pages        = {13--33},\n  publisher    = {Springer},\n  year         = {2024},\n  url          = {https://doi.org/10.1007/978-3-031-57228-9\\_2},\n  doi          = {10.1007/978-3-031-57228-9\\_2},\n  timestamp    = {Sun, 14 Apr 2024 18:32:17 +0200},\n  biburl       = {https://dblp.org/rec/conf/fossacs/HausmannPSS24.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2023\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae.\n \n \n \n \n\n\n \n Azzopardi, S., Lidell, D., Piterman, N., & Schneider, G.\n\n\n \n\n\n\n In André, É., & Sun, J., editor(s), Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part II, volume 14216, of Lecture Notes in Computer Science, pages 276–287, 2023. Springer\n \n\n\n\n
\n\n\n\n \n \n \"ppLTLTTPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/atva/AzzopardiLPS23,\n  author       = {Shaun Azzopardi and\n                  David Lidell and\n                  Nir Piterman and\n                  Gerardo Schneider},\n  editor       = {{\\'{E}}tienne Andr{\\'{e}} and\n                  Jun Sun},\n  title        = {ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae},\n  booktitle    = {Automated Technology for Verification and Analysis - 21st International\n                  Symposium, {ATVA} 2023, Singapore, October 24-27, 2023, Proceedings,\n                  Part {II}},\n  series       = {Lecture Notes in Computer Science},\n  volume       = {14216},\n  pages        = {276--287},\n  publisher    = {Springer},\n  year         = {2023},\n  url          = {https://doi.org/10.1007/978-3-031-45332-8\\_15},\n  doi          = {10.1007/978-3-031-45332-8\\_15},\n  timestamp    = {Fri, 27 Oct 2023 20:40:26 +0200},\n  biburl       = {https://dblp.org/rec/conf/atva/AzzopardiLPS23.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Compositional verification of priority systems using sharp bisimulation.\n \n \n \n \n\n\n \n Di Stefano, L., & Lang, F.\n\n\n \n\n\n\n Formal Methods in System Design. 2023.\n \n\n\n\n
\n\n\n\n \n \n \"CompositionalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@Article{DiStefanoL2023,\nauthor={Di Stefano, Luca\nand Lang, Fr{\\'e}d{\\'e}ric},\ntitle={Compositional verification of priority systems using sharp bisimulation},\njournal={Formal Methods in System Design},\nyear={2023},\ndoi={10.1007/s10703-023-00422-1},\nurl={https://doi.org/10.1007/s10703-023-00422-1}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants.\n \n \n \n\n\n \n De Nicola, R., Di Stefano, L., Inverso, O., & Valiani, S.\n\n\n \n\n\n\n In 21st International Conference on Computational Methods in Systems Biology (CMSB), 2023. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{cmsb2023,\n  author = {Rocco {De Nicola} and Luca {Di Stefano} and Omar Inverso and Serenella Valiani},\n  title = {Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants},\n  booktitle = {21st International Conference on Computational Methods in Systems Biology (CMSB)},\n  year = {2023},\n  doi = {10.1007/978-3-031-42697-1\\_4}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Language Support for Verifying Reconfigurable Interacting Systems.\n \n \n \n\n\n \n Abd Alrahman, Y., Azzopardi, S., Di Stefano, L., & Piterman, N.\n\n\n \n\n\n\n International Journal on Software Tools for Technology Transfer. 2023.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{sttt2023a,\n  title = {Language Support for Verifying Reconfigurable Interacting Systems},\n  author = {Abd Alrahman, Yehia and Azzopardi, Shaun and Di Stefano, Luca and Piterman, Nir},\n  journal   = {International Journal on Software Tools for Technology Transfer},\n  year =  {2023},\n  doi = {10.1007/s10009-023-00729-8},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Modelling Flocks of Birds and Colonies of Ants from the Bottom Up.\n \n \n \n\n\n \n De Nicola, R., Di Stefano, L., Inverso, O., & Valiani, S.\n\n\n \n\n\n\n International Journal on Software Tools for Technology Transfer. 2023.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{sttt2023,\n  title = {Modelling Flocks of Birds and Colonies of Ants from the Bottom Up},\n  author = {De Nicola, Rocco and Di Stefano, Luca and Inverso, Omar and Valiani, Serenella},\n  journal   = {International Journal on Software Tools for Technology Transfer},\n  year =  {2023},\n  doi = {10.1007/s10009-023-00731-0},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Games for Efficient Supervisor Synthesis.\n \n \n \n \n\n\n \n Hausmann, D., Jha, P. K., & Piterman, N.\n\n\n \n\n\n\n IEEE Control. Syst. Lett., 7: 2881–2885. 2023.\n \n\n\n\n
\n\n\n\n \n \n \"GamesPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/csysl/HausmannJP23,\n  author       = {Daniel Hausmann and\n                  Prabhat Kumar Jha and\n                  Nir Piterman},\n  title        = {Games for Efficient Supervisor Synthesis},\n  journal      = {{IEEE} Control. Syst. Lett.},\n  volume       = {7},\n  pages        = {2881--2885},\n  year         = {2023},\n  url          = {https://doi.org/10.1109/LCSYS.2023.3290727},\n  doi          = {10.1109/LCSYS.2023.3290727},\n  timestamp    = {Sat, 05 Aug 2023 00:02:02 +0200},\n  biburl       = {https://dblp.org/rec/journals/csysl/HausmannJP23.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Compositional Verification of Stigmergic Collective Systems.\n \n \n \n \n\n\n \n Di Stefano, L., & Lang, F.\n\n\n \n\n\n\n In Dragoi, C., Emmi, M., & Wang, J., editor(s), Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, January 16-17, 2023, Proceedings, volume 13881, of Lecture Notes in Computer Science, pages 155–176, 2023. Springer\n \n\n\n\n
\n\n\n\n \n \n \"CompositionalPaper\n  \n \n \n \"Compositional paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/vmcai/StefanoL23,\n  author    = {Luca {Di Stefano} and\n               Fr{\\'{e}}d{\\'{e}}ric Lang},\n  editor    = {Cezara Dragoi and\n               Michael Emmi and\n               Jingbo Wang},\n  title     = {Compositional Verification of Stigmergic Collective Systems},\n  booktitle = {Verification, Model Checking, and Abstract Interpretation - 24th International\n               Conference, {VMCAI} 2023, Boston, MA, USA, January 16-17, 2023, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {13881},\n  pages     = {155--176},\n  publisher = {Springer},\n  year      = {2023},\n  url       = {https://doi.org/10.1007/978-3-031-24950-1\\_8},\n  doi       = {10.1007/978-3-031-24950-1\\_8},\n  timestamp = {Mon, 30 Jan 2023 14:59:54 +0100},\n  biburl    = {https://dblp.org/rec/conf/vmcai/StefanoL23.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  url_paper = {https://www.cse.chalmers.se/%7Elucad/papers/vmcai2023.pdf}\n}\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (9)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Automated replication of tuple spaces via static analysis.\n \n \n \n \n\n\n \n De Nicola, R., Di Stefano, L., Inverso, O., & Uwimbabazi, A.\n\n\n \n\n\n\n Sci. Comput. Program., 223: 102863. 2022.\n \n\n\n\n
\n\n\n\n \n \n \"AutomatedPaper\n  \n \n \n \"Automated paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/scp/NicolaSIU22,\n  author    = {Rocco {De Nicola} and\n               Luca {Di Stefano} and\n               Omar Inverso and\n               Aline Uwimbabazi},\n  title     = {Automated replication of tuple spaces via static analysis},\n  journal   = {Sci. Comput. Program.},\n  volume    = {223},\n  pages     = {102863},\n  year      = {2022},\n  url       = {https://doi.org/10.1016/j.scico.2022.102863},\n  doi       = {10.1016/j.scico.2022.102863},\n  timestamp = {Tue, 15 Nov 2022 21:42:58 +0100},\n  biburl    = {https://dblp.org/rec/journals/scp/NicolaSIU22.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  url_paper = {https://www.cse.chalmers.se/%7Elucad/papers/scp2022.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Modelling Flocks of Birds from the Bottom Up.\n \n \n \n \n\n\n \n De Nicola, R., Di Stefano, L., Inverso, O., & Valiani, S.\n\n\n \n\n\n\n In Margaria, T., & Steffen, B., editor(s), International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 13703, of Lecture Notes in Computer Science, pages 82–96, 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n \"ModellingPaper\n  \n \n \n \"Modelling paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/isola/NicolaSIV22,\n  author    = {Rocco {De Nicola} and Luca {Di Stefano} and Omar Inverso and Serenella Valiani},\n  editor    = {Tiziana Margaria and Bernhard Steffen},\n  title     = {Modelling Flocks of Birds from the Bottom Up},\n  booktitle = {International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {13703},\n  pages     = {82--96},\n  publisher = {Springer},\n  year      = {2022},\n  url       = {https://doi.org/10.1007/978-3-031-19759-8\\_6},\n  doi       = {10.1007/978-3-031-19759-8\\_6},\n  timestamp = {Fri, 21 Oct 2022 19:54:55 +0200},\n  biburl    = {https://dblp.org/rec/conf/isola/NicolaSIV22.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  url_paper = {https://www.cse.chalmers.se/%7Elucad/papers/isola2022.pdf}\n}\n\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Survey on Satisfiability Checking for the \\(μ\\)-Calculus Through Tree Automata.\n \n \n \n \n\n\n \n Hausmann, D., & Piterman, N.\n\n\n \n\n\n\n In Raskin, J., Chatterjee, K., Doyen, L., & Majumdar, R., editor(s), Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660, of Lecture Notes in Computer Science, pages 228–251, 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{HP22,\n  author       = {Daniel Hausmann and\n                  Nir Piterman},\n  editor       = {Jean{-}Fran{\\c{c}}ois Raskin and\n                  Krishnendu Chatterjee and\n                  Laurent Doyen and\n                  Rupak Majumdar},\n  title        = {A Survey on Satisfiability Checking for the {\\(\\mu\\)}-Calculus Through\n                  Tree Automata},\n  booktitle    = {Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger\n                  on the Occasion of His 60th Birthday},\n  series       = {Lecture Notes in Computer Science},\n  volume       = {13660},\n  pages        = {228--251},\n  publisher    = {Springer},\n  year         = {2022},\n  url          = {https://doi.org/10.1007/978-3-031-22337-2\\_11},\n  doi          = {10.1007/978-3-031-22337-2\\_11},\n  timestamp    = {Fri, 06 Jan 2023 08:07:57 +0100},\n  biburl       = {https://dblp.org/rec/conf/birthday/0001P22.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Model Checking Reconfigurable Interacting Systems.\n \n \n \n\n\n \n Abd Alrahman, Y., Azzopardi, S., & Piterman, N.\n\n\n \n\n\n\n In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2022. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{isola-1,\ntitle={Model Checking Reconfigurable Interacting Systems}, \nauthor={Abd Alrahman, Yehia and Azzopardi, Shaun and Piterman, Nir},\nyear="2022",\nbooktitle="International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)",\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Runtime Verification meets Controller Synthesis.\n \n \n \n\n\n \n Azzopardi, S., Piterman, N., & Schneider, G.\n\n\n \n\n\n\n In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2022. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{isola-2,\ntitle={Runtime Verification meets Controller Synthesis}, \nauthor={Azzopardi, Shaun and Piterman, Nir, and Schneider, Gerardo},\nyear="2022",\nbooktitle="International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)",\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification.\n \n \n \n\n\n \n Azzopardi, S., Ellul, J., Falzon, R., & Pace, G.\n\n\n \n\n\n\n In Runtime Verification (RV), 2022. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{rv20221,\ntitle={AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification}, \nauthor={Azzopardi, Shaun and Ellul, Joshua and Falzon, Ryan and Pace, Gordon},\nyear="2022",\nbooktitle="Runtime Verification (RV)",\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Tainting in Smart Contracts: Combining Static and Runtime Verification.\n \n \n \n\n\n \n Azzopardi, S., Ellul, J., Falzon, R., & Pace, G.\n\n\n \n\n\n\n In Runtime Verification (RV), 2022. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{rv20222,\ntitle={Tainting in Smart Contracts: Combining Static and Runtime Verification}, \nauthor={Azzopardi, Shaun and Ellul, Joshua and Falzon, Ryan and Pace, Gordon},\nyear="2022",\nbooktitle="Runtime Verification (RV)",\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Runtime Verification of Kotlin Coroutines.\n \n \n \n\n\n \n Azzopardi, S., Furian, D., Falcone, Y., & Schneider, G.\n\n\n \n\n\n\n In Runtime Verification (RV), 2022. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{rv20221,\ntitle={Runtime Verification of Kotlin Coroutines}, \nauthor={Azzopardi, Shaun and Furian, Denis and Falcone, Yliès and Schneider, Gerardo},\nyear="2022",\nbooktitle="Runtime Verification (RV)",\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n R-CHECK: A Model Checker for Verifying Reconfigurable MAS.\n \n \n \n\n\n \n Abd Alrahman, Y., Azzopardi, S., & Piterman, N.\n\n\n \n\n\n\n In Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems, of AAMAS '22, pages 1518–1520, Richland, SC, 2022. International Foundation for Autonomous Agents and Multiagent Systems\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{10.5555/3535850.3536020,\n  author = {Abd Alrahman, Yehia and Azzopardi, Shaun and Piterman, Nir},\n  title = {R-CHECK: A Model Checker for Verifying Reconfigurable MAS},\n  year = {2022},\n  isbn = {9781450392136},\n  publisher = {International Foundation for Autonomous Agents and Multiagent Systems},\n  address = {Richland, SC},\n  abstract = {Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK, to allow reasoning about these systems both from an individual- and a system-level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, self-organisation, etc.},\n  booktitle = {Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems},\n  pages = {1518–1520},\n  numpages = {3},\n  keywords = {agent theories and models, verification of multi-agent systems, logics for agent reasoning},\n  location = {Virtual Event, New Zealand},\n  series = {AAMAS '22}\n}\n\n
\n
\n\n\n
\n Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK, to allow reasoning about these systems both from an individual- and a system-level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, self-organisation, etc.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Incorporating Monitors in Reactive Synthesis Without Paying the Price.\n \n \n \n \n\n\n \n Azzopardi, S., Piterman, N., & Schneider, G.\n\n\n \n\n\n\n In Hou, Z., & Ganesh, V., editor(s), Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings, volume 12971, of Lecture Notes in Computer Science, pages 337–353, 2021. Springer\n \n\n\n\n
\n\n\n\n \n \n \"IncorporatingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/atva/AzzopardiPS21,\n  author    = {Shaun Azzopardi and\n               Nir Piterman and\n               Gerardo Schneider},\n  editor    = {Zhe Hou and\n               Vijay Ganesh},\n  title     = {Incorporating Monitors in Reactive Synthesis Without Paying the Price},\n  booktitle = {Automated Technology for Verification and Analysis - 19th International\n               Symposium, {ATVA} 2021, Gold Coast, QLD, Australia, October 18-22,\n               2021, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {12971},\n  pages     = {337--353},\n  publisher = {Springer},\n  year      = {2021},\n  url       = {https://doi.org/10.1007/978-3-030-88885-5\\_22},\n  doi       = {10.1007/978-3-030-88885-5\\_22},\n  timestamp = {Wed, 03 Nov 2021 08:28:17 +0100},\n  biburl    = {https://dblp.org/rec/conf/atva/AzzopardiPS21.bib},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On the Specification and Monitoring of Timed Normative Systems.\n \n \n \n \n\n\n \n Azzopardi, S., Pace, G., Schapachnik, F., & Schneider, G.\n\n\n \n\n\n\n In Runtime Verification: 21st International Conference, RV 2021, Virtual Event, October 11–14, 2021, Proceedings, pages 81–99, Berlin, Heidelberg, 2021. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{10.1007/978-3-030-88494-9_5,\nauthor = {Azzopardi, Shaun and Pace, Gordon and Schapachnik, Fernando and Schneider, Gerardo},\ntitle = {On the Specification and Monitoring of Timed Normative Systems},\nyear = {2021},\nisbn = {978-3-030-88493-2},\npublisher = {Springer-Verlag},\naddress = {Berlin, Heidelberg},\nurl = {https://doi.org/10.1007/978-3-030-88494-9_5},\ndoi = {10.1007/978-3-030-88494-9_5},\nabstract = {In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.},\nbooktitle = {Runtime Verification: 21st International Conference, RV 2021, Virtual Event, October 11–14, 2021, Proceedings},\npages = {81–99},\nnumpages = {19},\nkeywords = {Monitoring, Normative systems, Timed logic, Legal contracts, Deontic logic}\n}\n\n
\n
\n\n\n
\n In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Linear-Time Nominal \\(μ\\)-Calculus with Name Allocation.\n \n \n \n \n\n\n \n Hausmann, D., Milius, S., & Schröder, L.\n\n\n \n\n\n\n In Bonchi, F., & Puglisi, S. J., editor(s), 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia, volume 202, of LIPIcs, pages 58:1–58:18, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{HMS21,\n  author    = {Daniel Hausmann and\n               Stefan Milius and\n               Lutz Schr{\\"{o}}der},\n  editor    = {Filippo Bonchi and\n               Simon J. Puglisi},\n  title     = {A Linear-Time Nominal {\\(\\mu\\)}-Calculus with Name Allocation},\n  booktitle = {46th International Symposium on Mathematical Foundations of Computer\n               Science, {MFCS} 2021, August 23-27, 2021, Tallinn, Estonia},\n  series    = {LIPIcs},\n  volume    = {202},\n  pages     = {58:1--58:18},\n  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\\"{u}}r Informatik},\n  year      = {2021},\n  url       = {https://doi.org/10.4230/LIPIcs.MFCS.2021.58},\n  doi       = {10.4230/LIPIcs.MFCS.2021.58},\n  timestamp = {Wed, 25 Aug 2021 17:11:18 +0200}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Nominal Büchi Automata with Name Allocation.\n \n \n \n \n\n\n \n Urbat, H., Hausmann, D., Milius, S., & Schröder, L.\n\n\n \n\n\n\n In Haddad, S., & Varacca, D., editor(s), 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203, of LIPIcs, pages 4:1–4:16, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik\n \n\n\n\n
\n\n\n\n \n \n \"NominalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{UrbatHMS21,\n  author    = {Henning Urbat and\n               Daniel Hausmann and\n               Stefan Milius and\n               Lutz Schr{\\"{o}}der},\n  editor    = {Serge Haddad and\n               Daniele Varacca},\n  title     = {Nominal B{\\"{u}}chi Automata with Name Allocation},\n  booktitle = {32nd International Conference on Concurrency Theory, {CONCUR} 2021,\n               August 24-27, 2021, Virtual Conference},\n  series    = {LIPIcs},\n  volume    = {203},\n  pages     = {4:1--4:16},\n  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\\"{u}}r Informatik},\n  year      = {2021},\n  url       = {https://doi.org/10.4230/LIPIcs.CONCUR.2021.4},\n  doi       = {10.4230/LIPIcs.CONCUR.2021.4},\n  timestamp = {Fri, 13 Aug 2021 23:45:21 +0200},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Modelling and Verification of Reconfigurable Multi-Agent Systems.\n \n \n \n \n\n\n \n Abd Alrahman, Y., & Piterman, N.\n\n\n \n\n\n\n Autonomous Agents and Multi-Agent Systems, 35. August 2021.\n \n\n\n\n
\n\n\n\n \n \n \"ModellingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{jamas,\n  author    = {Yehia {Abd Alrahman} and\n               Nir Piterman},\n  title     = {Modelling and Verification of Reconfigurable Multi-Agent Systems},\n  volume    = {35},\n  year      = {2021},\n  month     = {August},\n  publisher = {Springer Science},\n  url       = {https://doi.org/10.1007/s10458-021-09521-x},\n  doi       = {10.1007/s10458-021-09521-x},\n  journal   = {Autonomous Agents and Multi-Agent Systems},\n  abstract  = {We propose a formalism to model and reason about reconfigurable multi-agent systems. In our formalism, agents interact and communicate in different modes so that they can pursue joint tasks; agents may dynamically synchronize, exchange data, adapt their behaviour, and reconfigure their communication interfaces. Inspired by existing multi-robot systems, we represent a system as a set of agents (each with local state), executing independently and only influence each other by means of message exchange. Agents are able to sense their local states and partially their surroundings. We extend LTL to be able to reason explicitly about the intentions of agents in the interaction and their communication protocols. We also study the complexity of satisfiability and model-checking of this extension.}\n}\n
\n
\n\n\n
\n We propose a formalism to model and reason about reconfigurable multi-agent systems. In our formalism, agents interact and communicate in different modes so that they can pursue joint tasks; agents may dynamically synchronize, exchange data, adapt their behaviour, and reconfigure their communication interfaces. Inspired by existing multi-robot systems, we represent a system as a set of agents (each with local state), executing independently and only influence each other by means of message exchange. Agents are able to sense their local states and partially their surroundings. We extend LTL to be able to reason explicitly about the intentions of agents in the interaction and their communication protocols. We also study the complexity of satisfiability and model-checking of this extension.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesis of Run-To-Completion Controllers for Discrete Event Systems.\n \n \n \n \n\n\n \n Abd Alrahman, Y., Braberman, V. A., D'Ippolito, N., Piterman, N., & Uchitel, S.\n\n\n \n\n\n\n In 2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021, pages 4892–4899, 2021. IEEE\n \n\n\n\n
\n\n\n\n \n \n \"SynthesisPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{acc21,\n  author    = {Yehia {Abd Alrahman} and\n               V{\\'{\\i}}ctor A. Braberman and\n               Nicol{\\'{a}}s D'Ippolito and\n               Nir Piterman and\n               Sebasti{\\'{a}}n Uchitel},\n  title     = {Synthesis of Run-To-Completion Controllers for Discrete Event Systems},\n  booktitle = {2021 American Control Conference, {ACC} 2021, New Orleans, LA, USA,\n               May 25-28, 2021},\n  pages     = {4892--4899},\n  publisher = {{IEEE}},\n  year      = {2021},\n  url       = {https://doi.org/10.23919/ACC50511.2021.9482704},\n  doi       = {10.23919/ACC50511.2021.9482704},\n abstract  = {A controller for a Discrete Event System must achieve its goals despite that its environment being capable of resolving race conditions between controlled and uncontrolled events.Assuming that the controller loses all races is sometimes unrealistic. In many cases, a realistic assumption is that the controller sometimes wins races and is fast enough to perform multiple actions without being interrupted. However, in order to model this scenario using control of DES requires introducing foreign assumptions about scheduling, that are hard to figure out correctly. We propose a more balanced control problem, named run-to-completion (RTC), to alleviate this issue. RTC naturally supports an execution assumption in which both the controller and the environment are guaranteed to initiate and perform sequences of actions, without flooding or delaying each other indefinitely. We consider control of DES in the context where specifications are given in the form of linear temporal logic. We formalize the RTC control problem and show how it can be reduced to a standard control problem.}\n}\n
\n
\n\n\n
\n A controller for a Discrete Event System must achieve its goals despite that its environment being capable of resolving race conditions between controlled and uncontrolled events.Assuming that the controller loses all races is sometimes unrealistic. In many cases, a realistic assumption is that the controller sometimes wins races and is fast enough to perform multiple actions without being interrupted. However, in order to model this scenario using control of DES requires introducing foreign assumptions about scheduling, that are hard to figure out correctly. We propose a more balanced control problem, named run-to-completion (RTC), to alleviate this issue. RTC naturally supports an execution assumption in which both the controller and the environment are guaranteed to initiate and perform sequences of actions, without flooding or delaying each other indefinitely. We consider control of DES in the context where specifications are given in the form of linear temporal logic. We formalize the RTC control problem and show how it can be reduced to a standard control problem.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Control and Discovery of Reactive System Environments.\n \n \n \n \n\n\n \n Keegan, M., Braberman, V. A., D'Ippolito, N., Piterman, N., & Uchitel, S.\n\n\n \n\n\n\n IEEE Transactions on Software Engineering. 2021.\n To appear\n\n\n\n
\n\n\n\n \n \n \"ControlPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{KBDPU21,\n  author  = {Maureen Keegan 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   = {Control and Discovery of Reactive System Environments},\n  journal = {IEEE Transactions on Software Engineering},\n  volume  = {},\n  issue   = {},\n  year    = {2021},\n  url     = {},\n  note    = {To appear}\n}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Reconfigurable Interaction for MAS Modelling.\n \n \n \n \n\n\n \n Abd Alrahman, Y., Perelli, G., & Piterman, N.\n\n\n \n\n\n\n In Proceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems, of AAMAS '20, pages 7-15, Richland, SC, 2020. International Foundation for Autonomous Agents and Multiagent Systems\n \n\n\n\n
\n\n\n\n \n \n \"ReconfigurablePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 29 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@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
\n
\n\n\n
\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
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A distributed API for coordinating AbC programs.\n \n \n \n \n\n\n \n Abd Alrahman, Y., & Garbi, G.\n\n\n \n\n\n\n International Journal on Software Tools for Technology Transfer. feb 2020.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@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
\n
\n\n\n
\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
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Programming interactions in collective adaptive systems by relying on attribute-based communication.\n \n \n \n \n\n\n \n Abd Alrahman, Y., De Nicola, R., & Loreti, M.\n\n\n \n\n\n\n Sci. Comput. Program., 192: 102428. 2020.\n \n\n\n\n
\n\n\n\n \n \n \"ProgrammingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@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\n\n
\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
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (10)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Equilibrium Design for Concurrent Games.\n \n \n \n \n\n\n \n Gutierrez, J., Najib, M., Perelli, G., & Wooldridge, M.\n\n\n \n\n\n\n In 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands., pages 22:1–22:16, 2019. \n \n\n\n\n
\n\n\n\n \n \n \"EquilibriumPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{C-GNPW19b,\n  author    = {Julian Gutierrez and Muhammad Najib and Giuseppe Perelli and Michael Wooldridge},\n  title     = {Equilibrium Design for Concurrent Games},\n  booktitle = {30th International Conference on Concurrency Theory, {CONCUR} 2019, August 27-30, 2019, Amsterdam, the Netherlands.},\n  pages     = {22:1--22:16},\n  year      = {2019},\n  url       = {https://doi.org/10.4230/LIPIcs.CONCUR.2019.22}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On Computational Tractability for Rational Verification.\n \n \n \n \n\n\n \n Gutierrez, J., Najib, M., Perelli, G., & Wooldridge, M.\n\n\n \n\n\n\n In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 329–335, 2019. \n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{C-GNPW19a,\n  author    = {Julian Gutierrez and Muhammad Najib and Giuseppe Perelli and Michael Wooldridge},\n  title     = {On Computational Tractability for Rational Verification.},\n  booktitle = {Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, {IJCAI} 2019, Macao, China, August 10-16, 2019},\n  pages     = {329--335},\n  year      = {{2019}},\n  url       = {https://www.ijcai.org/Proceedings/2019/47}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Reasoning about Quality and Fuzziness of Strategic Behaviours.\n \n \n \n \n\n\n \n Bouyer, P., Kupferman, O., Markey, N., Maubert, B., Murano, A., & Perelli, G.\n\n\n \n\n\n\n In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 1588–1594, 2019. \n \n\n\n\n
\n\n\n\n \n \n \"ReasoningPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{C-BKMMMP19,\n  author    = {Patricia Bouyer and Orna Kupferman and Nicolas Markey and Bastien Maubert and Aniello Murano and Giuseppe Perelli},\n  title     = {Reasoning about Quality and Fuzziness of Strategic Behaviours.},\n  booktitle = {Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, {IJCAI} 2019, Macao, China, August 10-16, 2019},\n  pages     = {1588--1594},\n  year      = {2019},\n  url       = {https://www.ijcai.org/Proceedings/2019/220}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Enforcing Equilibria in Multi-Agent Systems.\n \n \n \n \n\n\n \n Perelli, G.\n\n\n \n\n\n\n In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS '19, Montreal, QC, Canada, May 13-17, 2019, pages 188–196, 2019. \n \n\n\n\n
\n\n\n\n \n \n \"EnforcingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 6 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{C-Per19,\n  author    = {Giuseppe Perelli},\n  title     = {Enforcing Equilibria in Multi-Agent Systems.},\n  booktitle = {Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, {AAMAS} '19, Montreal, QC, Canada, May 13-17, 2019},\n  pages     = {188--196},\n  year      = {2019},\n  url       = {https://dl.acm.org/doi/10.5555/3306127.3331692}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Nash Equilibrium and Bisimulation Invariance.\n \n \n \n\n\n \n Gutierrez, J., Harrenstein, P., Perelli, G., & Wooldridge, M.\n\n\n \n\n\n\n In Logical Methods in Computer Science, volume 15, issue 3. 2019.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{J-GHPW19,\n  author    = {Julian Gutierrez and Paul Harrenstein and Giuseppe Perelli and Michael Wooldridge},\n  title     = {Nash Equilibrium and Bisimulation Invariance.},\n  booktitle = {Logical Methods in Computer Science},\n  journal   = {Logical Methods in Computer Science},\n  volume    = {15, issue 3},\n  year      = {2019},\n  doi       = {10.23638/LMCS-15(3:32)2019}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A calculus for collective-adaptive systems and its behavioural theory.\n \n \n \n \n\n\n \n Abd Alrahman, Y., De Nicola, R., & Loreti, M.\n\n\n \n\n\n\n Inf. Comput., 268. 2019.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@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
\n
\n\n\n
\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
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A coordination protocol language for power grid operation control.\n \n \n \n \n\n\n \n Abd Alrahman, Y., & Vieira, H. T.\n\n\n \n\n\n\n J. Log. Algebraic Methods Program., 109. 2019.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@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
\n
\n\n\n
\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
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Testing for Coordination Fidelity.\n \n \n \n \n\n\n \n Abd Alrahman, Y., Mezzina, C. A., & Vieira, H. T.\n\n\n \n\n\n\n In Boreale, M., Corradini, F., Loreti, M., & Pugliese, R., editor(s), Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, volume 11665, of Lecture Notes in Computer Science, pages 152-169, 2019. Springer\n \n\n\n\n
\n\n\n\n \n \n \"TestingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@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\n
\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
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Combinations of Qualitative Winning for Stochastic Parity Games.\n \n \n \n\n\n \n Chatterjee, K., & Piterman, N.\n\n\n \n\n\n\n In 30th International Conference on Concurrency Theory, of LIPIcs, pages 229-246, Amsterdam, Netherlands, August 2019. Schloss Dagstuhl\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@inproceedings{CP19,\n  author       = {K. Chatterjee and\n               N. Piterman},\n  title        = {Combinations of Qualitative Winning for Stochastic Parity Games},\n  booktitle    = {30th International Conference on Concurrency Theory},\n  pages        = {229-246},\n  year         = {2019},\n  series       = {LIPIcs},\n  address      = {Amsterdam, Netherlands},\n  month        = {August},\n  publisher    = {Schloss Dagstuhl},\n  opturl_paper = {https://www.cse.chalmers.se/~piterman/publications/2020/2019/CP19.pdf},\n  keywords     = {Games}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Environmentally-Friendly GR(1) Synthesis.\n \n \n \n \n\n\n \n Majumdar, R., Piterman, N., & Schmuck, A.\n\n\n \n\n\n\n In 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 11428, of Lecture Notes in Computer Science, pages 229-246, Prague, Czech Republic, April 2019. \n \n\n\n\n
\n\n\n\n \n \n \"Environmentally-Friendly paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 11 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{MPS19,\n  author    = {R. Majumdar and\n               N. Piterman and\n               A.-K. Schmuck},\n  title     = {Environmentally-Friendly {GR(1)} Synthesis},\n  booktitle = {25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},\n  pages     = {229-246},\n  year      = {2019},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {11428},\n  address   = {Prague, Czech Republic},\n  month     = {April},\n  url_paper = {https://www.cse.chalmers.se/%7Epiterman/publications/2019/MPS19.pdf},\n  keywords  = {Games,Synthesis}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);