\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
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 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
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 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
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 \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
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 \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
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 abstract \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
@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
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 abstract \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
@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
Paper\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