Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative speci cations, and have found ...

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 ...

Reactive synthesis guarantees correct-by-construction controllers from logical specifications, but is costly—2EXPTIME-complete in the size of the specification. In a practical setting, the desired controllers need to ...

This paper presents ppLTLTT, a tool for translating pure-past linear temporal logic formulae into temporal testers in the form of automata. We show how ppLTLTT can be used to easily extend existing LTL-based tools, such ...

A question we can ask of multi-agent systems is whether the agents’ collective interaction satisfies particular goals or specifications, which can be either individual or collective. When a collaborative goal is not reached, ...