Recent Submissions

  • Automata Constructions for LTL with Past 

    Lidell, David (Department of Computer Science and Engineering University of Gothenburg | Chalmers University of Technology, 2024)
    Linear temporal logic (LTL) is a popular language in formal verification, especially in the domains of model checking and reactive synthesis. Because its semantics is defined in terms of infinite sequences of symbols ...
  • Dagligt vattenintag – Rekommendationer och tips för att använda vatten för att gå ner i vikt 

    Bianca, Dupsen (FoodInScope SE, 2024-09-17)
    Pamfletten ger en översikt över de positiva effekterna av att dricka vatten för viktminskning. Den diskuterar hur tillräcklig vätsketillförsel kan bidra till att öka mättnadskänslan, främja ämnesomsättningen och stödja ...
  • Enhancing Requirements Engineering Practices Using Large Language Models 

    Ronanki, Krishna (2024)
    Background: Large Language Models (LLMs) offer users natural language interaction, technical insights and task automation capabilities. However, the systematic integration of LLMs within Requirements Engineering ...
  • Compositional Verification of Stigmergic Collective System 

    Di Stefano, Luca; Lang, Frédéric (2023)
    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 ...
  • Compositional Verification of Priority Systems Using Sharp Bisimulation 

    Di Stefano, Luca; Lang, Frédéric (2023)
    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 ...
  • Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants 

    De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, Serinella (2024)
    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, ...
  • Synthesis for prefix first-order logic on data words 

    Grange, J.; Lehaut, Mathieu (2024)
    We 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 ...
  • Generic Model Checking for Modal Fixpoint Logics in COOL-MC 

    Hausmann, Daniel; Humml, Merlin; Prucker, Simon; Schröder, Lutz; Strahlberger, Aaron (2023)
    We 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 ...
  • Faster Game Solving by Fixpoint Acceleration 

    Hausmann, Daniel (2024)
    We 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 ...
  • THE CONSENSING APPROACH TO STRATEGIZING: The Dynamics of Dialogue in Public Sector Digital Transformation 

    Norling, Kristian (2024-04-10)
    This thesis explores the role of consensing, a process of cognitive consensus-building through the mechanisms of sensing and synthesizing, in digital transformation strategy formulation within the Swedish public sector. ...
  • Unraveling The Black Box - Building Understandable AI Through Strategic Explanation and User-based Design 

    Yu, Shuren (2024)
    The pervasive integration of Artificial Intelligence (AI) in society presents both opportunities and challenges, with the black-box issue emerging as a significant obstacle in realizing the full potential of AI. The ...
  • Fair Omega-regular Games 

    Hausmann, Daniel; Piterman, Nir; Saglam, Irmak; Schmuck, Anne-Kathrin (27th International Conference on Foundations of Software Science and Computation Structures, 2024)
    We 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 ...
  • Symbolic Solution of Emerson-Lei Games for Reactive Synthesis 

    Hausmann, Daniel; Lehaut, Mathieu; Piterman, Nir (2024)
    Emerson-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 ...
  • Synchronous Agents, Verification, and Blame - A Deontic View 

    Kharraz, Karam; Azzopardi, Shaun; Schneider, Gerardo; Leucker, Martin (2023)
    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, ...
  • Modelling Flocks of Birds and Colonies of Ants from the Bottom Up 

    De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, Serenella (2023)
  • Games for Efficient Supervisor Synthesis 

    Hausmann, Daniel; Prabhat, Kumar Jha; Piterman, Nir (2023)
    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 ...
  • COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description) 

    Görlitz, Oliver; Hausmann, Daniel; Humml, Merlin; Pattinson, Dirk; Prucker, Simon; Schröder, Lutz (2023)
    There 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 ...
  • ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae 

    Azzopardi, Shaun; Lidell, David; Piterman, Nir; Schneider, Gerardo (2023)
    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 ...
  • Language Support for Verifying Reconfigurable Interacting Systems 

    Abd Alrahman, Yehia; Azzopardi, Shaun; Di Stefano, Luca; Piterman, Nir (2023)
    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 ...

View more