Articles, chapters, papers, reports Department of Computer Science and Engineering
Permanent URI for this collectionhttps://gupea-staging.ub.gu.se/handle/2077/74181
Browse
Recent Submissions
Item Distribution of Reconfiguration Languages maintaining Tree-like Communication Topology(2024) Hausmann, Daniel; Lehaut, Mathieu; Piterman, NirWe study how to distribute trace languages in a setting where processes communicate via reconfigurable communication channels. That is, the different processes can connect and disconnect from channels at run time. We restrict attention to communication via tree-like communication architectures. These allow channels to connect more than two processes in a way that maintains an underlying spanning tree and keeps communication continuous on the tree. We make the reconfiguration explicit in the language allowing both a centralized automaton as well as the distributed processes to share relevant information about the current communication configuration. We show that Zielonka's seminal result regarding distribution of regular languages for asynchronous automata can be generalized in this setting, incorporating both reconfiguration and more than binary tree architectures.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, NirAutonomous 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.Item Adding Reconfiguration to Zielonka’s Asynchronous Automata(Electronic Proceedings in Theoretical Computer Science, EPTCS, 88-102, 2024) Lehaut, Mathieu; Piterman, NirWe study an extension of Zielonka’s (fixed) asynchronous automata called reconfigurable asynchronous automata where processes can dynamically change who they communicate with. We show that reconfigurable asynchronous automata are not more expressive than fixed asynchronous automata by giving translations from one to the other. However, going from reconfigurable to fixed comes at the cost of disseminating communication (and knowledge) to all processes in the system. We then show that this is unavoidable by describing a language accepted by a reconfigurable automaton such that in every equivalent fixed automaton, every process must either be aware of all communication or be irrelevant.Item Faster and Smaller Solutions of Obliging Games(35th International Conference on Concurrency Theory (CONCUR 2024), 2024) Hausmann, Daniel; Piterman, NirObliging games have been introduced in the context of the game perspective on reactive synthesis in order to enforce a degree of cooperation between the to-be-synthesized system and the environment. Previous approaches to the analysis of obliging games have been small-step in the sense that they have been based on a reduction to standard (non-obliging) games in which single moves correspond to single moves in the original (obliging) game. Here, we propose a novel, large-step view on obliging games, reducing them to standard games in which single moves encode long-term behaviors in the original game. This not only allows us to give a meaningful definition of the environment winning in obliging games, but also leads to significantly improved bounds on both strategy sizes and the solution runtime for obliging games.Item Compositional Verification of Stigmergic Collective System(2023) Di Stefano, Luca; Lang, FrédéricCollective 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.Item Compositional Verification of Priority Systems Using Sharp Bisimulation(2023) Di Stefano, Luca; Lang, FrédéricSharp 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.Item Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants(2024) De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, SerinellaWe 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 wholeItem Synthesis for prefix first-order logic on data words(2024) Grange, J.; Lehaut, MathieuWe study the reactive synthesis problem for distributed systems with an unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modeled by data words, and specifications are given as first-order logic formulas from a fragment we call prefix first-order logic that implements a limited kind of order. We show that this logic has nice properties that enable us to prove decidability of the synthesis problem.Item Generic Model Checking for Modal Fixpoint Logics in COOL-MC(2023) Hausmann, Daniel; Humml, Merlin; Prucker, Simon; Schröder, Lutz; Strahlberger, AaronWe report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (non-deterministic, game-based, probabilistic etc.) and in the next-step modalities used in formulae. The tool implements generic model checking algorithms developed in coalgebraic logic that are easily adapted to concrete instance logics. Apart from the standard modal -calculus, COOL-MC currently supports alternating-time, graded, probabilistic and monotone variants of the -calculus, but is also effortlessly extensible with new instance logics. The model checking process is realized by polynomial reductions to parity game solving, or, alternatively, by a local model checking algorithm that directly computes the extensions of formulae in a lazy fashion, thereby potentially avoiding the construction of the full parity game. We evaluate COOL-MC on informative benchmark sets.Item Faster Game Solving by Fixpoint Acceleration(2024) Hausmann, DanielWe propose a method for solving parity games with acyclic (DAG) sub-structures by computing nested fixpoints of a DAG attractor function that lives over the non-DAG parts of the game, thereby restricting the domain of the involved fixpoint operators. Intuitively, this corresponds to accelerating fixpoint computation by inlining cycle-free parts during the solution of parity games, leading to earlier convergence. We also present an economic later-appearence-record construction that takes Emerson-Lei games to parity games, and show that it preserves DAG sub-structures; it follows that the proposed method can be used also for the accelerated solution of Emerson-Lei games.Item Fair Omega-regular Games(27th International Conference on Foundations of Software Science and Computation Structures, 2024) Hausmann, Daniel; Piterman, Nir; Saglam, Irmak; Schmuck, Anne-KathrinWe consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph G=(V,E) and a set of fair moves E_f a subset of E a player is said to play fair in G if they choose an edge e in E_f infinitely often whenever the source vertex of e is visited infinitely often. Otherwise, they play unfair. We equip such games with two omega-regular winning conditions alpha and beta deciding the winner of mutually fair and mutually unfair plays, respectively. Whenever one player plays fair and the other plays unfair, the fairly playing player wins the game. The resulting games are called fair alpha/beta games. We formalize fair alpha/beta games and show that they are determined. For fair parity/parity games, i.e., fair alpha/beta games where alpha and beta are given each by a parity condition over G, we provide a polynomial reduction to (normal) parity games via a gadget construction inspired by the reduction of stochastic parity games to parity games. We further give a direct symbolic fixpoint algorithm to solve fair parity/parity games. On a conceptual level, we illustrate the translation between the gadget-based reduction and the direct symbolic algorithm which uncovers the underlying similarities of solution algorithms for fair and stochastic parity games, as well as for the recently considered class of fair games in which only one player is restricted by fair moves.Item Symbolic Solution of Emerson-Lei Games for Reactive Synthesis(2024) Hausmann, Daniel; Lehaut, Mathieu; Piterman, NirEmerson-Lei conditions have recently attracted attention due to both their succinctness and their favorable closure properties. In the current work, we show how infinite-duration games with Emerson-Lei objectives can be analyzed in two different ways. First, we show that the Zielonka tree of the Emerson-Lei condition naturally gives rise to a new reduction to parity games. This reduction, however, does not result in optimal analysis. Second, we show based on the first reduction (and the Zielonka tree) how to provide a direct fixpoint-based characterization of the winning region. The fixpoint-based characterization allows for symbolic analysis. It generalizes the solutions of games with known winning conditions such as B\"uchi, GR[1], parity, Streett, Rabin and Muller objectives, and in the case of these conditions reproduces previously known symbolic algorithms and complexity results. We also show how the capabilities of the proposed algorithm can be exploited in reactive synthesis, suggesting a new expressive fragment of LTL that can be handled symbolically. Our fragment combines a safety specification and a liveness part. The safety part is unrestricted and the liveness part allows to define Emerson-Lei conditions on occurrences of letters. The symbolic treatment is enabled due to the simplicity of determinization in the case of safety languages and by using our new algorithm for game solving. This approach maximizes the number of steps solved symbolically in order to maximize the potential for efficient symbolic implementations.Item Synchronous Agents, Verification, and Blame - A Deontic View(2023) Kharraz, Karam; Azzopardi, Shaun; Schneider, Gerardo; Leucker, MartinA 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.Item Modelling Flocks of Birds and Colonies of Ants from the Bottom Up(2023) De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, SerenellaItem Games for Efficient Supervisor Synthesis(2023) Hausmann, Daniel; Prabhat, Kumar Jha; Piterman, Nir; Department of Computer Science and Engineering, Computing Science (GU)In recent years, there has been an increasing interest in the connections between supervisory control theory and reactive synthesis. As the two fields use similar techniques there is great hope that technologies from one field could be used in the other. In this spirit, we provide an alternative reduction from the supervisor synthesis problem to solving Büchi games via games with a non-blocking objective. Our reduction is more compact and uniform than previous reductions. As a consequence, it gives an asymptotically better upper bound on the time complexity of the supervisory control synthesis problem. Our reduction also breaks a widely held belief about the impossibility of reducing the supervisory control synthesis problem to a game with a linear winning condition.Item COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description)(2023) Görlitz, Oliver; Hausmann, Daniel; Humml, Merlin; Pattinson, Dirk; Prucker, Simon; Schröder, LutzThere is a wide range of modal logics whose semantics goes beyond relational structures, and instead involves, e.g., probabilities, multi-player games, weights, or neighbourhood structures. Coalgebraic logic serves as a unifying semantic and algorithmic framework for such logics. It provides uniform reasoning algorithms that are easily instantiated to particular, concretely given logics. The COOL 2 reasoner provides an implementation of such generic algorithms for coalgebraic modal fixpoint logics. As concrete instances, we obtain in particular reasoners for the aconjunctive and alternation-free fragments of the graded μ -calculus and the alternating-time μ -calculus. We evaluate the tool on standard benchmark sets for fixpoint-free graded modal logic and alternating-time temporal logic (ATL), as well as on a dedicated set of benchmarks for the graded μ -calculus.Item ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae(2023) Azzopardi, Shaun; Lidell, David; Piterman, Nir; Schneider, GerardoThis 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.Item Language Support for Verifying Reconfigurable Interacting Systems(2023) Abd Alrahman, Yehia; Azzopardi, Shaun; Di Stefano, Luca; Piterman, NirReconfigurable 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.Item Games for Efficient Supervisor Synthesis(2023) Hausmann, Daniel; Kumar Jha, Prabhat; Piterman, NirIn recent years, there has been an increasing interest in the connections between supervisory control theory and reactive synthesis. As the two fields use similar techniques there is great hope that technologies from one field could be used in the other. In this spirit, we provide an alternative reduction from the supervisor synthesis problem to solving Büchi games via games with a non-blocking objective. Our reduction is more compact and uniform than previous reductions. As a consequence, it gives an asymptotically better upper bound on the time complexity of the supervisory control synthesis problem. Our reduction also breaks a widely held belief about the impossibility of reducing the supervisory control synthesis problem to a game with a linear winning condition.Item A Survey on Satisfiability Checking for the μ -Calculus Through Tree Automata(2022) Hausmann, Daniel; Piterman, NirAlgorithms for model checking and satisfiability of the modal μ -calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more complicated. We review the non-emptiness checking of alternating tree automata by a reduction to solving parity games of a certain structure, so-called emptiness games. Since the emptiness problem for alternating tree automata is EXPTIME -complete, the size of these games is exponential in the number of states of the input automaton. We show how the construction of the emptiness games combines a (fixed) structural part with (history-)determinization of parity word automata. For tree automata with certain syntactic structures, simpler methods may be used to handle the treatment of the word automata, which then may be asymptotically smaller than in the general case. These results have direct consequences in satisfiability and validity checking for (various fragments of) the modal μ -calculus.