Browsing by Author "Schneider, Gerardo"

Filter results by typing the first few letters
Now showing 1 - 5 of 5
  • No Thumbnail Available
    Item
    Incorporating Monitors in Reactive Synthesis without Paying the Price
    (19th International Symposium on Automated Technology for Verification and Analysis, 2021) Azzopardi, Shaun; Piterman, Nir; Schneider, Gerardo
    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 languages that combine modelling with declarative speci - cations more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this paper we explore an approach that combines synthesis of declarative speci cations in the presence of an existing behaviour model as a monitor, with the bene t of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeat- ing triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional syn- thesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we ap- ply it to speci cations requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametri- sation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.
  • No Thumbnail Available
    Item
    On the Specification and Monitoring of Timed Normative Systems
    (2022) Azzopardi, Shaun; Pace, Gordon J.; Schapachnik, Fernando; Schneider, Gerardo
    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.
  • No Thumbnail Available
    Item
    ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae
    (2023) Azzopardi, Shaun; Lidell, David; Piterman, Nir; Schneider, Gerardo
    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 as LTL-to-automata translators and reactive synthesis tools, to support a richer input language. Namely, with ppLTLTT, tools that accept LTL input are also made to handle pure-past LTL as atomic formulae. While the addition of past operators does not increase the expressive power of LTL, it opens up the possibility of writing more intuitive and succinct specifications. We illustrate this intended use of ppLTLTT for Slugs, Strix, and Spot ’s command line tool LTL2TGBA by describing three corresponding wrapper tools pSlugs, pStrix, and pLTL2TGBA, that all leverage ppLTLTT. All three wrapper tools are designed to seamlessly fit this paradigm, by staying as close to the respective syntax of each underlying tool as possible.
  • No Thumbnail Available
    Item
    Runtime Verification meets Controller Synthesis
    (2022) Azzopardi, Shaun; Piterman, Nir; Schneider, Gerardo
    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 interact with an environment, but the more precise the model of the environment used for synthesis, the greater the cost of synthesis. This can be avoided by using suitable abstractions of the environment, but this in turn requires appropriate techniques to mediate between controllers and the real environment. Runtime verification can help here, with monitors acting as these mediators, and even as activators or orchestrators of the desired controllers. In this paper we survey literature for combinations of monitors with controller synthesis, and consider other potential combinations as future research directions.
  • No Thumbnail Available
    Item
    Synchronous Agents, Verification, and Blame - A Deontic View
    (2023) Kharraz, Karam; Azzopardi, Shaun; Schneider, Gerardo; Leucker, Martin
    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, or a specification is violated, a pertinent question is whether any agent is to blame. This paper considers a two-agent synchronous setting and a formal language to specify when agents’ collaboration is required. We take a deontic approach and use obligations, permissions, and prohibitions to capture notions of non-interference between agents. We also handle reparations, allowing violations to be corrected or compensated. We give trace semantics to our logic, and use it to define blame assignment for violations. We give an automaton construction for the logic, which we use as the base for model checking and blame analysis. We also further provide quantitative semantics that is able to compare different interactions in terms of the required reparations.