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 "Di Stefano, Luca"

Filter results by typing the first few letters
Now showing 1 - 8 of 8
  • 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
    Automated replication of tuple spaces via static analysis
    (2022) De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Uwimbabazi, Aline
    Coordination languages for tuple spaces can offer significant advantages in the specification and implementation of distributed systems, but often do require manual programming effort to ensure consistency. We propose an experimental technique for automated replication of tuple spaces in distributed systems. The system of interest is modelled as a concurrent Go program where different threads represent the behaviour of the separate components, each owning its own local tuple repository. We automatically transform the initial program by combining program transformation and static analysis, so that tuples are replicated depending on the components' read-write access patterns. In this way, we turn the initial system into a replicated one where the replication of tuples is automatically achieved, while avoiding unnecessary replication overhead. Custom static analyses may be plugged in easily in our prototype implementation. We see this as a first step towards developing a fully-fledged framework to support designers to quickly evaluate many classes of replication-based systems under different consistency levels.
  • No Thumbnail Available
    Item
    Compositional Verification of Priority Systems Using Sharp Bisimulation
    (2023) Di Stefano, Luca; Lang, Frédéric
    Sharp bisimulation is a refinement of branching bisimulation, parame terized by a subset of the system’s actions, called strong actions. This parameterization allows the sharp bisimulation to be tailored by the property under verification, whichever property of the modal µ-calculus is considered, while potentially reducing more than strong bisimulation. Sharp bisimulation equivalence is a congruence for process algebraic oper ators such as parallel composition, hide, cut, and rename, and hence can be used in a compositional verification setting. In this paper, we prove that sharp bisimulation equivalence is also a congruence for action priority operators under some conditions on strong actions. We com pare sharp bisimulation with orthogonal bisimulation, whose equivalence is also a congruence for action priority. We show that, if the internal action τ neither gives priority to nor takes priority over other actions, then the quotient of a system with respect to sharp bisimulation equiv alence (called sharp minimization) cannot be larger than the quotient of the same system with respect to orthogonal bisimulation equivalence. We then describe a signature-based partition refinement algorithm for sharp minimization, implemented in the BCG_MIN and BCG_CMP tools of the CADP software toolbox. This algorithm can be adapted to implement orthogonal minimization. We show on a crafted exam ple that using compositional sharp minimization may yield state space reductions that outperform compositional orthogonal minimization by Verification of Priority Systems Using Sharp Bisimulation several orders of magnitude. Finally, we illustrate the use of sharp minimization and priority to verify a bully leader election algorithm.
  • No Thumbnail Available
    Item
    Compositional Verification of Stigmergic Collective System
    (2023) Di Stefano, Luca; Lang, Frédéric
    Collective adaptive systems may be broadly defined as en sembles of autonomous agents, whose interaction may lead to the emer gence of global features and patterns. Formal verification may provide strong guarantees about the emergence of these features, but may suffer from scalability issues caused by state space explosion. Compositional verification techniques, whereby the state space of a system is generated by combining (an abstraction of) those of its components, have shown to be a promising countermeasure to the state space explosion problem. Therefore, in this work we apply these techniques to the problem of verifying collective adaptive systems with stigmergic interaction. Specif ically, we automatically encode these systems into networks of LNT pro cesses, apply a static value analysis to prune the state space of individual agents, and then reuse compositional verification procedures provided by the CADP toolbox. We demonstrate the effectiveness of our approach by verifying a collection of representative systems.
  • No Thumbnail Available
    Item
    Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants
    (2024) De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, Serinella
    We demonstrate a novel methodology that integrates intuitive modelling, simulation, and formal verification of collective behaviour in biological systems. To that end, we consider the case of a colony of foraging ants, where, for the combined effect of known biological mechanisms such as stigmergic interaction, pheromone release, and path integration, the ants will progressively work out the shortest path to move back and forth between their nest and a hypothetical food repository. Starting from an informal description in natural language, we show how to devise intuitive specifications for such scenario in a formal language. We then make use of a prototype software tool to formally assess whether such specifications would indeed replicate the expected collective behaviour of the colony as a whole
  • 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
    Modelling Flocks of Birds and Colonies of Ants from the Bottom Up
    (2023) De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, Serenella
  • No Thumbnail Available
    Item
    Modelling Flocks of Birds from the Bottom Up
    (2022) De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, Serenella
    We argue that compositional specification based on formal languages can facilitate the modelling of, and reasoning about, sophisticated collective behaviour in many natural systems. One defines a system in terms of individual components and local rules, so that collective behaviours emerge naturally from the combined effect of the different actions of the individual components. With appropriate linguistic constructs, this can yield compact and intuitive models that are easy to refine and extend in small incremental steps. In addition, automated workflows implemented on top of this methodology can provide quick feedback, thereby allowing rapid design iterations. To support our argument, we consider flocking, a well-known example of emergent behaviour in collective adaptive systems. We build a minimalistic bottom-up model of a flock of birds incrementally, discussing specific language constructs as we go along. We then describe a prototype simulator, and use it to validate our model in a controlled experiment, where a flock is attacked by a bird of prey. The flock effectively reacts to the attack by splitting into smaller groups and regathering once the threat subsides, consistently with both natural observations and previous models from the literature.