Articles, chapters, papers, reports Department of Computer Science and Engineering

Permanent URI for this collectionhttps://gupea-staging.ub.gu.se/handle/2077/74181

Browse

Browsing Articles, chapters, papers, reports Department of Computer Science and Engineering by Author "Azzopardi, Shaun"

Filter results by typing the first few letters
Now showing 1 - 4 of 4
  • No Thumbnail Available
    Item
    Attributed Point-to-Point Communication in R-CHECK
    (Lecture Notes in Computer Science (LNCS), 2024) Abd Alrahman, Yehia; Azzopardi, Shaun; Di Stefano, Luca; Piterman, Nir
    Autonomous multi-agent, or more generally, collective adaptive systems, use different modes of communication to support their autonomy and ease of interaction. In order to enable modelling and reasoning about such systems, we need frameworks that combine many forms of communication. R-CHECK is a modelling, simulation, and verification environment supporting the development of multi-agent systems, providing attributed channelled broadcast and multicast communication. That is, the communication is not merely derived based on connectivity to channels but in addition based on properties of targeted receiversȦnother common communication mode is point-to-point, wherein agents communicate with each other directly. Capturing point-to-point through R-CHECK’s multicast and broadcast is possible but cumbersome, inefficient, and prone to interference. Here, we extend R-CHECK with attributed point-to-point communication, which can be established based on identity or properties of participants. We also support model-checking of point-to-point by extending linear temporal logic with observation descriptors related to the participants in this communication mode. We argue that these extensions simplify the design of models, and demonstrate their benefits by means of an illustrative case study.
  • No Thumbnail Available
    Item
    Language Support for Verifying Reconfigurable Interacting Systems
    (2023) Abd Alrahman, Yehia; Azzopardi, Shaun; Di Stefano, Luca; Piterman, Nir
    Reconfigurable interacting 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. In this article, we provide a modeling and analysis environment for the design of such system. Our tool offers simulation and verification to facilitate native reasoning about the domain concepts of such systems. We present our tool named R-CHECK. R-CHECK supports a high-level input language with matching enumerative and symbolic semantics, and provides a modelling convenience for features such as reconfiguration, coalition formation, self-organisation, etc. For analysis, users can simulate the designed system and explore arising traces. Our included model checker permits reasoning about interaction protocols and joint missions.
  • 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
    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.