Incorporating Monitors in Reactive Synthesis Without Paying the Price.
Azzopardi, S., Piterman, N., & Schneider, G.
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
Paper
doi
link
bibtex
2 downloads
@inproceedings{DBLP:conf/atva/AzzopardiPS21,
author = {Shaun Azzopardi and
Nir Piterman and
Gerardo Schneider},
editor = {Zhe Hou and
Vijay Ganesh},
title = {Incorporating Monitors in Reactive Synthesis Without Paying the Price},
booktitle = {Automated Technology for Verification and Analysis - 19th International
Symposium, {ATVA} 2021, Gold Coast, QLD, Australia, October 18-22,
2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12971},
pages = {337--353},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-88885-5\_22},
doi = {10.1007/978-3-030-88885-5\_22},
timestamp = {Wed, 03 Nov 2021 08:28:17 +0100},
biburl = {https://dblp.org/rec/conf/atva/AzzopardiPS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
On the Specification and Monitoring of Timed Normative Systems.
Azzopardi, S., Pace, G., Schapachnik, F., & Schneider, G.
In
Runtime Verification: 21st International Conference, RV 2021, Virtual Event, October 11–14, 2021, Proceedings, pages 81–99, Berlin, Heidelberg, 2021. Springer-Verlag
Paper
doi
link
bibtex
abstract
@inproceedings{10.1007/978-3-030-88494-9_5,
author = {Azzopardi, Shaun and Pace, Gordon and Schapachnik, Fernando and Schneider, Gerardo},
title = {On the Specification and Monitoring of Timed Normative Systems},
year = {2021},
isbn = {978-3-030-88493-2},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
url = {https://doi.org/10.1007/978-3-030-88494-9_5},
doi = {10.1007/978-3-030-88494-9_5},
abstract = {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.},
booktitle = {Runtime Verification: 21st International Conference, RV 2021, Virtual Event, October 11–14, 2021, Proceedings},
pages = {81–99},
numpages = {19},
keywords = {Monitoring, Normative systems, Timed logic, Legal contracts, Deontic logic}
}
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.
A Linear-Time Nominal μ-Calculus with Name Allocation.
Hausmann, D., Milius, S., & Schröder, L.
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
Paper
doi
link
bibtex
@inproceedings{HMS21,
author = {Daniel Hausmann and
Stefan Milius and
Lutz Schr{\"{o}}der},
editor = {Filippo Bonchi and
Simon J. Puglisi},
title = {A Linear-Time Nominal {\(\mu\)}-Calculus with Name Allocation},
booktitle = {46th International Symposium on Mathematical Foundations of Computer
Science, {MFCS} 2021, August 23-27, 2021, Tallinn, Estonia},
series = {LIPIcs},
volume = {202},
pages = {58:1--58:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2021},
url = {https://doi.org/10.4230/LIPIcs.MFCS.2021.58},
doi = {10.4230/LIPIcs.MFCS.2021.58},
timestamp = {Wed, 25 Aug 2021 17:11:18 +0200}
}
Nominal Büchi Automata with Name Allocation.
Urbat, H., Hausmann, D., Milius, S., & Schröder, L.
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
Paper
doi
link
bibtex
@inproceedings{UrbatHMS21,
author = {Henning Urbat and
Daniel Hausmann and
Stefan Milius and
Lutz Schr{\"{o}}der},
editor = {Serge Haddad and
Daniele Varacca},
title = {Nominal B{\"{u}}chi Automata with Name Allocation},
booktitle = {32nd International Conference on Concurrency Theory, {CONCUR} 2021,
August 24-27, 2021, Virtual Conference},
series = {LIPIcs},
volume = {203},
pages = {4:1--4:16},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2021},
url = {https://doi.org/10.4230/LIPIcs.CONCUR.2021.4},
doi = {10.4230/LIPIcs.CONCUR.2021.4},
timestamp = {Fri, 13 Aug 2021 23:45:21 +0200},
}
Modelling and Verification of Reconfigurable Multi-Agent Systems.
Abd Alrahman, Y., & Piterman, N.
Autonomous Agents and Multi-Agent Systems, 35. August 2021.
Paper
doi
link
bibtex
abstract
11 downloads
@article{jamas,
author = {Yehia {Abd Alrahman} and
Nir Piterman},
title = {Modelling and Verification of Reconfigurable Multi-Agent Systems},
volume = {35},
year = {2021},
month = {August},
publisher = {Springer Science},
url = {https://doi.org/10.1007/s10458-021-09521-x},
doi = {10.1007/s10458-021-09521-x},
journal = {Autonomous Agents and Multi-Agent Systems},
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.}
}
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.
Synthesis of Run-To-Completion Controllers for Discrete Event Systems.
Abd Alrahman, Y., Braberman, V. A., D'Ippolito, N., Piterman, N., & Uchitel, S.
In
2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021, pages 4892–4899, 2021. IEEE
Paper
doi
link
bibtex
abstract
11 downloads
@inproceedings{acc21,
author = {Yehia {Abd Alrahman} and
V{\'{\i}}ctor A. Braberman and
Nicol{\'{a}}s D'Ippolito and
Nir Piterman and
Sebasti{\'{a}}n Uchitel},
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.}
}
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.
Control and Discovery of Reactive System Environments.
Keegan, M., Braberman, V. A., D'Ippolito, N., Piterman, N., & Uchitel, S.
IEEE Transactions on Software Engineering. 2021.
To appear
Paper
link
bibtex
4 downloads
@article{KBDPU21,
author = {Maureen Keegan and
V{\'{\i}}ctor A. Braberman and
Nicol{\'{a}}s D'Ippolito and
Nir Piterman and
Sebasti{\'{a}}n Uchitel},
title = {Control and Discovery of Reactive System Environments},
journal = {IEEE Transactions on Software Engineering},
volume = {},
issue = {},
year = {2021},
url = {},
note = {To appear}
}