Browsing Articles, chapters, papers, reports Department of Computer Science and Engineering by Issue Date
Now showing items 1-20 of 23
-
Automated replication of tuple spaces via static analysis
(2022)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 ... -
A PO Characterisation of Reconfiguration
(2022)We consider partial order semantics of concurrent systems in which local reconfigurations may have global side effects. That is, local changes happening to an entity may block or unblock events relating to others, namely, ... -
Modelling Flocks of Birds from the Bottom Up
(2022)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 ... -
A Survey on Satisfiability Checking for the μ -Calculus Through Tree Automata
(2022)Algorithms 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 ... -
Games for Efficient Supervisor Synthesis
(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)
(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 ... -
Games for Efficient Supervisor Synthesis
(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 ... -
Language Support for Verifying Reconfigurable Interacting Systems
(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 ... -
ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae
(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 ... -
Synchronous Agents, Verification, and Blame - A Deontic View
(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, ... -
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
(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 ... -
Compositional Verification of Priority Systems Using Sharp Bisimulation
(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 ... -
Compositional Verification of Stigmergic Collective System
(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 ... -
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
(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 ... -
Fair Omega-regular Games
(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 ... -
Faster Game Solving by Fixpoint Acceleration
(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 ... -
Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants
(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
(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 ... -
Attributed Point-to-Point Communication in R-CHECK
(Lecture Notes in Computer Science (LNCS), 2024)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, ...