Volume
LIPIcs, Volume 311
35th International Conference on Concurrency Theory (CONCUR 2024)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR)
Event
CONCUR 2024, September 9-13, 2024, Calgary, CanadaEditors
Publication Details
- published at: 2024-08-29
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-339-3
- DBLP: db/conf/concur/concur2024
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 311, CONCUR 2024, Complete Volume
Abstract
LIPIcs, Volume 311, CONCUR 2024, Complete Volume
Cite as
35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 1-752, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Proceedings{majumdar_et_al:LIPIcs.CONCUR.2024,
title = {{LIPIcs, Volume 311, CONCUR 2024, Complete Volume}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {1--752},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024},
URN = {urn:nbn:de:0030-drops-207714},
doi = {10.4230/LIPIcs.CONCUR.2024},
annote = {Keywords: LIPIcs, Volume 311, CONCUR 2024, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{majumdar_et_al:LIPIcs.CONCUR.2024.0,
author = {Majumdar, Rupak and Silva, Alexandra},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {0:i--0:xii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.0},
URN = {urn:nbn:de:0030-drops-207724},
doi = {10.4230/LIPIcs.CONCUR.2024.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk)
Abstract
First Order Logic (FOL) is a powerful formalism that naturally captures many interesting decision and optimization problems. In recent years, there has been a tremendous progress in automated logic reasoning tools, such as Boolean SATisfiability Solvers and Satisfiability Modulo Theory solvers. This enabled the use of logic and logic solvers as a universal solution to many problems in Computer Science, in general, and in Program Analysis, in particular. Most new program analysis techniques formalize the desired analysis task in a fragment of FOL, and delegate the analysis to a SAT or an SMT solver.
In this talk, we focus on a fragment of FOL called Constrained Horn Clauses (CHC) and the CHC solver SPACER. CHCs arise in many applications of automated verification. They naturally capture such problems as discovery and verification of inductive invariants; Model Checking of safety properties of finite- and infinite-state systems; safety verification of push-down systems (and their extensions); modular verification of distributed and parameterized systems; type inference, and many others.
Using CHC separates the process of developing a proof methodology (also known as generation of Verification Condition (VC)) from the algorithmic details of deciding whether the VC is correct. Such a flexible design simplifies supporting multiple proof methodologies, multiple languages, and multiple verification tasks with a single framework, without sacrificing performance and scalability.
Cite as
Arie Gurfinkel. Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk). In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{gurfinkel:LIPIcs.CONCUR.2024.1,
author = {Gurfinkel, Arie},
title = {{Constrained Horn Clauses for Program Verification and Synthesis}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {1:1--1:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.1},
URN = {urn:nbn:de:0030-drops-207734},
doi = {10.4230/LIPIcs.CONCUR.2024.1},
annote = {Keywords: Constrained Horn Clauses}
}
Document
Invited Talk
Principles of Persistent Programming (Invited Talk)
Abstract
Persistent programming is the art of developing programs that operate on persistent (non-volatile) states that survive program termination, be it planned or abrupt (e.g. due to a power failure). Persistent programming poses several important challenges: 1) persistent systems have complex - and often unspecified - semantics in that operations do not generally persist in their execution order; 2) software bugs in persistent settings can lead to permanent data corruption; and 3) traditional testing techniques are inapplicable in persistent settings. Can formal methods come to the rescue?
Cite as
Azalea Raad. Principles of Persistent Programming (Invited Talk). In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{raad:LIPIcs.CONCUR.2024.2,
author = {Raad, Azalea},
title = {{Principles of Persistent Programming}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.2},
URN = {urn:nbn:de:0030-drops-207742},
doi = {10.4230/LIPIcs.CONCUR.2024.2},
annote = {Keywords: Persistent Programming}
}
Document
Invited Talk
Verifying Concurrent Search Structures (Invited Talk)
Abstract
Search structures support the fundamental data storage primitives on key-value pairs: insert a pair, delete by key, search by key, and update the value associated with a key. Concurrent search structures are parallel algorithms to speed access to search structures on multicore and distributed servers. For these data structures to be efficient, the underlying parallel algorithms need to perform fine-grained synchronization between threads. This makes them notoriously difficult to design and implement correctly. Indeed, bugs are routinely found both in actual implementations and in the designs proposed by experts in peer-reviewed publications. Often, these bugs elude testing-based quality control due to complex thread interactions that only manifest after deployment, and under conditions that are difficult to replicate. Given the critical role that concurrent search structures play in today’s software infrastructure, it is therefore highly desirable to verify their correctness using formal methods, preferably in an automated fashion.
In this talk, I will present a framework for obtaining linearizability proofs for concurrent search structures that are modular, reusable, and amenable to automation. The framework takes advantage of recent advances in local reasoning techniques based on concurrent separation logic. I will provide an overview of these techniques and discuss there use for verifying both lock-based and lock-free concurrent search structures such as concurrent (skip)lists, hash structures, binary search trees, B trees, and log-structured merge trees.
Cite as
Thomas Wies. Verifying Concurrent Search Structures (Invited Talk). In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{wies:LIPIcs.CONCUR.2024.3,
author = {Wies, Thomas},
title = {{Verifying Concurrent Search Structures}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {3:1--3:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.3},
URN = {urn:nbn:de:0030-drops-207754},
doi = {10.4230/LIPIcs.CONCUR.2024.3},
annote = {Keywords: Concurrent search structures}
}
Document
Centralized vs Decentralized Monitors for Hyperproperties
Abstract
This paper focuses on the runtime verification of hyperproperties expressed in Hyper-recHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-recHML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralised monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation.
Cite as
Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Daniele Gorla, and Jana Wagemaker. Centralized vs Decentralized Monitors for Hyperproperties. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{aceto_et_al:LIPIcs.CONCUR.2024.4,
author = {Aceto, Luca and Achilleos, Antonis and Anastasiadi, Elli and Francalanza, Adrian and Gorla, Daniele and Wagemaker, Jana},
title = {{Centralized vs Decentralized Monitors for Hyperproperties}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {4:1--4:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.4},
URN = {urn:nbn:de:0030-drops-207763},
doi = {10.4230/LIPIcs.CONCUR.2024.4},
annote = {Keywords: Runtime Verification, hyperlogics, decentralization}
}
Document
MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm
Abstract
The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities into equivalent automata. Typical conversions equip the automata with a guess-and-check mechanism to ascertain the truth of future modalities. Guess-and-check can be naturally implemented via alternation. However, since timed automata tools do not handle alternation, existing methods perform an additional step of converting the alternating timed automata into timed automata. This "de-alternation" step proceeds by an intricate finite abstraction of the space of configurations of the alternating automaton.
Recently, a model of generalized timed automata (GTA) has been proposed. The model comes with several powerful additional features, and yet, the best known zone-based reachability algorithms for timed automata have been extended to the GTA model, with the same complexity for all the zone operations. An attractive feature of GTAs is the presence of future clocks which act like timers that guess a time to an event and stay alive until a timeout. Future clocks seem to provide another natural way to implement the guess-and-check: start the future clock with a guessed time to an event and check its occurrence using a timeout. Indeed, using this feature, we provide a new concise translation from MITL to GTA. In particular, for the timed until modality, our translation offers an exponential improvement w.r.t. the state-of-the-art.
Thanks to this conversion, MITL model checking reduces to checking liveness for GTAs. However, no liveness algorithm is known for GTAs. Due to the presence of future clocks, there is no finite time-abstract bisimulation (region equivalence) for GTAs, whereas liveness algorithms for timed automata crucially rely on the presence of the finite region equivalence. As our second contribution, we provide a new zone-based algorithm for checking Büchi non-emptiness in GTAs, which circumvents this fundamental challenge.
Cite as
S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{akshay_et_al:LIPIcs.CONCUR.2024.5,
author = {Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.},
title = {{MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {5:1--5:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.5},
URN = {urn:nbn:de:0030-drops-207774},
doi = {10.4230/LIPIcs.CONCUR.2024.5},
annote = {Keywords: MITL model checking, timed automata, zones, liveness}
}
Document
Causally Deterministic Markov Decision Processes
Abstract
Probabilistic systems are often modeled using factored versions of Markov decision processes (MDPs), where the states are composed out of the local states of components and each transition involves only a small subset of the components. Concurrency arises naturally in such systems. Our goal is to exploit concurrency when analyzing factored MDPs (FMDPs). To do so, we first formulate FMDPs in a way that aids this goal and port several notions from concurrency theory to the probabilistic setting of MDPs. In particular, we provide a concurrent semantics for FMDPs based on the classical notion of event structures, thereby cleanly separating causality, concurrency, and conflicts that arise from stochastic choices. We further identify the subclass of causally deterministic FMDPs (CMDPs), where non-determinism arises solely due to concurrency. Using our event structure semantics, we show that in CMDPs, local reachability properties can be computed using a "greedy" strategy. Finally, we implement our ideas in a prototype and apply it to four models, confirming the potential for substantial improvements over state-of-the-art methods.
Cite as
S. Akshay, Tobias Meggendorfer, and P. S. Thiagarajan. Causally Deterministic Markov Decision Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{akshay_et_al:LIPIcs.CONCUR.2024.6,
author = {Akshay, S. and Meggendorfer, Tobias and Thiagarajan, P. S.},
title = {{Causally Deterministic Markov Decision Processes}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {6:1--6:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.6},
URN = {urn:nbn:de:0030-drops-207781},
doi = {10.4230/LIPIcs.CONCUR.2024.6},
annote = {Keywords: MDPs, distribution, causal determinism}
}
Document
Fairness and Consensus in an Asynchronous Opinion Model for Social Networks
Abstract
We introduce a DeGroot-based model for opinion dynamics in social networks. A community of agents is represented as a weighted directed graph whose edges indicate how much agents influence one another. The model is formalized using labeled transition systems, henceforth called opinion transition systems (OTS), whose states represent the agents' opinions and whose actions are the edges of the influence graph. If a transition labeled (i,j) is performed, agent j updates their opinion taking into account the opinion of agent i and the influence i has over j. We study (convergence to) opinion consensus among the agents of strongly-connected graphs with influence values in the interval (0,1). We show that consensus cannot be guaranteed under the standard strong fairness assumption on transition systems. We derive that consensus is guaranteed under a stronger notion from the literature of concurrent systems; bounded fairness. We argue that bounded-fairness is too strong of a notion for consensus as it almost surely rules out random runs and it is not a constructive liveness property. We introduce a weaker fairness notion, called m-bounded fairness, and show that it guarantees consensus. The new notion includes almost surely all random runs and it is a constructive liveness property. Finally, we consider OTS with dynamic influence and show convergence to consensus holds under m-bounded fairness if the influence changes within a fixed interval [L,U] with 0 < L < U < 1. We illustrate OTS with examples and simulations, offering insights into opinion formation under fairness and dynamic influence.
Cite as
Jesús Aranda, Sebastián Betancourt, Juan Fco. Díaz, and Frank Valencia. Fairness and Consensus in an Asynchronous Opinion Model for Social Networks. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{aranda_et_al:LIPIcs.CONCUR.2024.7,
author = {Aranda, Jes\'{u}s and Betancourt, Sebasti\'{a}n and D{\'\i}az, Juan Fco. and Valencia, Frank},
title = {{Fairness and Consensus in an Asynchronous Opinion Model for Social Networks}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {7:1--7:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.7},
URN = {urn:nbn:de:0030-drops-207794},
doi = {10.4230/LIPIcs.CONCUR.2024.7},
annote = {Keywords: Social networks, fairness, DeGroot, consensus, asynchrony}
}
Document
Bidding Games with Charging
Abstract
Graph games lie at the algorithmic core of many automated design problems in computer science. These are games usually played between two players on a given graph, where the players keep moving a token along the edges according to pre-determined rules (turn-based, concurrent, etc.), and the winner is decided based on the infinite path (aka play) traversed by the token from a given initial position. In bidding games, the players initially get some monetary budgets which they need to use to bid for the privilege of moving the token at each step. Each round of bidding affects the players' available budgets, which is the only form of update that the budgets experience. We introduce bidding games with charging where the players can additionally improve their budgets during the game by collecting vertex-dependent monetary rewards, aka the "charges." Unlike traditional bidding games (where all charges are zero), bidding games with charging allow non-trivial recurrent behaviors. For example, a reachability objective may require multiple detours to vertices with high charges to earn additional budget. We show that, nonetheless, the central property of traditional bidding games generalizes to bidding games with charging: For each vertex there exists a threshold ratio, which is the necessary and sufficient fraction of the total budget for winning the game from that vertex. While the thresholds of traditional bidding games correspond to unique fixed points of linear systems of equations, in games with charging, these fixed points are no longer unique. This significantly complicates the proof of existence and the algorithmic computation of thresholds for infinite-duration objectives. We also provide the lower complexity bounds for computing thresholds for Rabin and Streett objectives, which are the first known lower bounds in any form of bidding games (with or without charging), and we solve the following repair problem for safety and reachability games that have unsatisfiable objectives: Can we distribute a given amount of charge to the players in a way such that the objective can be satisfied?
Cite as
Guy Avni, Ehsan Kafshdar Goharshady, Thomas A. Henzinger, and Kaushik Mallik. Bidding Games with Charging. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{avni_et_al:LIPIcs.CONCUR.2024.8,
author = {Avni, Guy and Kafshdar Goharshady, Ehsan and Henzinger, Thomas A. and Mallik, Kaushik},
title = {{Bidding Games with Charging}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {8:1--8:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.8},
URN = {urn:nbn:de:0030-drops-207807},
doi = {10.4230/LIPIcs.CONCUR.2024.8},
annote = {Keywords: Bidding games on graphs, \omega-regular objectives}
}
Document
Risk-Averse Optimization of Total Rewards in Markovian Models Using Deviation Measures
Abstract
This paper addresses objectives tailored to the risk-averse optimization of accumulated rewards in Markov decision processes (MDPs). The studied objectives require maximizing the expected value of the accumulated rewards minus a penalty factor times a deviation measure of the resulting distribution of rewards. Using the variance in this penalty mechanism leads to the variance-penalized expectation (VPE) for which it is known that optimal schedulers have to minimize future expected rewards when a high amount of rewards has been accumulated. This behavior is undesirable as risk-averse behavior should keep the probability of particularly low outcomes low, but not discourage the accumulation of additional rewards on already good executions.
The paper investigates the semi-variance, which only takes outcomes below the expected value into account, the mean absolute deviation (MAD), and the semi-MAD as alternative deviation measures. Furthermore, a penalty mechanism that penalizes outcomes below a fixed threshold is studied. For all of these objectives, the properties of optimal schedulers are specified and in particular the question whether these objectives overcome the problem observed for the VPE is answered. Further, the resulting algorithmic problems on MDPs and Markov chains are investigated.
Cite as
Christel Baier, Jakob Piribauer, and Maximilian Starke. Risk-Averse Optimization of Total Rewards in Markovian Models Using Deviation Measures. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{baier_et_al:LIPIcs.CONCUR.2024.9,
author = {Baier, Christel and Piribauer, Jakob and Starke, Maximilian},
title = {{Risk-Averse Optimization of Total Rewards in Markovian Models Using Deviation Measures}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {9:1--9:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.9},
URN = {urn:nbn:de:0030-drops-207816},
doi = {10.4230/LIPIcs.CONCUR.2024.9},
annote = {Keywords: Markov decision processes, risk-aversion, deviation measures, total reward}
}
Document
Passive Learning of Regular Data Languages in Polynomial Time and Data
Abstract
A regular data language is a language over an infinite alphabet recognized by a deterministic register automaton (DRA), as defined by Benedikt, Ley and Puppis. The later model, which is expressively equivalent to the deterministic finite-memory automata introduced earlier by Francez and Kaminsky, enjoys unique minimal automata (up to isomorphism), based on a Myhill-Nerode theorem.
In this paper, we introduce a polynomial time passive learning algorithm for regular data languages from positive and negative samples. Following Gold’s model for learning languages, we prove that our algorithm can identify in the limit any regular data language L, i.e. it returns a minimal DRA recognizing L if a characteristic sample set for L is provided as input. We prove that there exist characteristic sample sets of polynomial size with respect to the size of the minimal DRA recognizing L. To the best of our knowledge, it is the first passive learning algorithm for data languages, and the first learning algorithm which is fully polynomial, both with respect to time complexity and size of the characteristic sample set.
Cite as
Mrudula Balachander, Emmanuel Filiot, and Raffaella Gentilini. Passive Learning of Regular Data Languages in Polynomial Time and Data. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{balachander_et_al:LIPIcs.CONCUR.2024.10,
author = {Balachander, Mrudula and Filiot, Emmanuel and Gentilini, Raffaella},
title = {{Passive Learning of Regular Data Languages in Polynomial Time and Data}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {10:1--10:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.10},
URN = {urn:nbn:de:0030-drops-207829},
doi = {10.4230/LIPIcs.CONCUR.2024.10},
annote = {Keywords: Register automata, passive learning, automata over infinite alphabets}
}
Document
Left-Linear Rewriting in Adhesive Categories
Abstract
When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since independence means that they could be executed in any order, and potentially in parallel. Equivalences identifying rewriting sequences which differ only for independent steps are at the core of the theory of concurrency of many formalisms. We investigate the issue in the context of the double pushout approach to rewriting in the general setting of adhesive categories. While a consolidated theory exists for linear rules, which can consume, preserve and generate entities, this paper focuses on left-linear rules which may also "merge" parts of the state. This is an apparently minimal, yet technically hard enhancement, since a standard characterisation of independence that - in the linear case - allows one to derive a number of properties, essential in the development of a theory of concurrency, no longer holds. The paper performs an in-depth study of the notion of independence for left-linear rules: it introduces a novel characterisation of independence, identifies well-behaved classes of left-linear rewriting systems, and provides some fundamental results including a Church-Rosser property and the existence of canonical equivalence proofs for concurrent computations. These results properly extends the class of formalisms that can be modelled in the adhesive framework.
Cite as
Paolo Baldan, Davide Castelnovo, Andrea Corradini, and Fabio Gadducci. Left-Linear Rewriting in Adhesive Categories. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{baldan_et_al:LIPIcs.CONCUR.2024.11,
author = {Baldan, Paolo and Castelnovo, Davide and Corradini, Andrea and Gadducci, Fabio},
title = {{Left-Linear Rewriting in Adhesive Categories}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {11:1--11:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.11},
URN = {urn:nbn:de:0030-drops-207835},
doi = {10.4230/LIPIcs.CONCUR.2024.11},
annote = {Keywords: Adhesive categories, double-pushout rewriting, left-linear rules, switch equivalence, local Church-Rosser property}
}
Document
History-Determinism vs Fair Simulation
Abstract
An automaton 𝒜 is history-deterministic if its nondeterminism can be resolved on the fly, only using the prefix of the word read so far. This mild form of nondeterminism has attracted particular attention for its applications in synthesis problems. An automaton 𝒜 is guidable with respect to a class C of automata if it can fairly simulate every automaton in C, whose language is contained in that of 𝒜. In other words, guidable automata are those for which inclusion and simulation coincide, making them particularly interesting for model-checking.
We study the connection between these two notions, and specifically the question of when they coincide. For classes of automata on which they do, deciding guidability, an otherwise challenging decision problem, reduces to deciding history-determinism, a problem that is starting to be well-understood for many classes.
We provide a selection of sufficient criteria for a class of automata to guarantee the coincidence of the notions, and use them to show that the notions coincide for the most common automata classes, among which are ω-regular automata and many infinite-state automata with safety and reachability acceptance conditions, including vector addition systems with states, one-counter nets, pushdown-, Parikh-, and timed-automata.
We also demonstrate that history-determinism and guidability do not always coincide, for example, for the classes of timed automata with a fixed number of clocks.
Cite as
Udi Boker, Thomas A. Henzinger, Karoliina Lehtinen, and Aditya Prakash. History-Determinism vs Fair Simulation. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{boker_et_al:LIPIcs.CONCUR.2024.12,
author = {Boker, Udi and Henzinger, Thomas A. and Lehtinen, Karoliina and Prakash, Aditya},
title = {{History-Determinism vs Fair Simulation}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {12:1--12:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.12},
URN = {urn:nbn:de:0030-drops-207841},
doi = {10.4230/LIPIcs.CONCUR.2024.12},
annote = {Keywords: History-Determinism}
}
Document
The Power of Counting Steps in Quantitative Games
Abstract
We study deterministic games of infinite duration played on graphs and focus on the strategy complexity of quantitative objectives. Such games are known to admit optimal memoryless strategies over finite graphs, but require infinite-memory strategies in general over infinite graphs.
We provide new lower and upper bounds for the strategy complexity of mean-payoff and total-payoff objectives over infinite graphs, focusing on whether step-counter strategies (sometimes called Markov strategies) suffice to implement winning strategies. In particular, we show that over finitely branching arenas, three variants of limsup mean-payoff and total-payoff objectives admit winning strategies that are based either on a step counter or on a step counter and an additional bit of memory. Conversely, we show that for certain liminf total-payoff objectives, strategies resorting to a step counter and finite memory are not sufficient. For step-counter strategies, this settles the case of all classical quantitative objectives up to the second level of the Borel hierarchy.
Cite as
Sougata Bose, Rasmus Ibsen-Jensen, David Purser, Patrick Totzke, and Pierre Vandenhove. The Power of Counting Steps in Quantitative Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{bose_et_al:LIPIcs.CONCUR.2024.13,
author = {Bose, Sougata and Ibsen-Jensen, Rasmus and Purser, David and Totzke, Patrick and Vandenhove, Pierre},
title = {{The Power of Counting Steps in Quantitative Games}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.13},
URN = {urn:nbn:de:0030-drops-207852},
doi = {10.4230/LIPIcs.CONCUR.2024.13},
annote = {Keywords: Games on graphs, Markov strategies, quantitative objectives, infinite-state systems}
}
Document
As Soon as Possible but Rationally
Abstract
This paper addresses complexity problems in rational verification and synthesis for multi-player games played on weighted graphs, where the objective of each player is to minimize the cost of reaching a specific set of target vertices. In these games, one player, referred to as the system, declares his strategy upfront. The other players, composing the environment, then rationally make their moves according to their objectives. The rational behavior of these responding players is captured through two models: they opt for strategies that either represent a Nash equilibrium or lead to a play with a Pareto-optimal cost tuple.
Cite as
Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin. As Soon as Possible but Rationally. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2024.14,
author = {Bruy\`{e}re, V\'{e}ronique and Grandmont, Christophe and Raskin, Jean-Fran\c{c}ois},
title = {{As Soon as Possible but Rationally}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {14:1--14:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.14},
URN = {urn:nbn:de:0030-drops-207869},
doi = {10.4230/LIPIcs.CONCUR.2024.14},
annote = {Keywords: Games played on graphs, rational verification, rational synthesis, Nash equilibrium, Pareto-optimality, quantitative reachability objectives}
}
Document
RobTL: Robustness Temporal Logic for CPS
Abstract
We propose Robustness Temporal Logic (RobTL), a novel temporal logic for the specification and analysis of distances between the behaviours of Cyber-Physical Systems (CPS) over a finite time horizon. RobTL specifications allow us to measure the differences in the behaviours of systems with respect to various objectives and temporal constraints, and to study how those differences evolve in time. Specifically, the unique features of RobTL allow us to specify robustness properties of CPS against uncertainty and perturbations. As an example, we use RobTL to analyse the robustness of an engine system that is subject to attacks aimed at inflicting overstress of equipment.
Cite as
Valentina Castiglioni, Michele Loreti, and Simone Tini. RobTL: Robustness Temporal Logic for CPS. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{castiglioni_et_al:LIPIcs.CONCUR.2024.15,
author = {Castiglioni, Valentina and Loreti, Michele and Tini, Simone},
title = {{RobTL: Robustness Temporal Logic for CPS}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {15:1--15:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.15},
URN = {urn:nbn:de:0030-drops-207870},
doi = {10.4230/LIPIcs.CONCUR.2024.15},
annote = {Keywords: Cyber-physical systems, robustness, temporal logic, uncertainty}
}
Document
Effect Semantics for Quantum Process Calculi
Abstract
The development of quantum communication protocols sparked the interest in quantum extensions of process calculi and behavioural equivalences, but defining a bisimilarity that matches the observational properties of a quantum-capable system is a surprisingly difficult task. The two proposals explicitly addressing this issue, qCCS and lqCCS, do not define an algorithmic verification scheme: the bisimilarity of two processes is proven by comparing their behaviour under all input states. We introduce a new semantic model based on effects, i.e. probabilistic predicates on quantum states that represent their observable properties. We define and investigate the properties of effect distributions and effect labelled transition systems (eLTSs), generalizing probability distributions and probabilistic labelled transition systems (pLTSs), respectively. As a proof of concept, we provide an eLTS-based semantics for a minimal quantum process algebra, which we prove sound and complete with respect to the observable probabilistic behaviour of quantum processes. To the best of our knowledge, ours is the first algorithmically verifiable proposal that abides to the properties of quantum theory.
Cite as
Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Effect Semantics for Quantum Process Calculi. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{ceragioli_et_al:LIPIcs.CONCUR.2024.16,
author = {Ceragioli, Lorenzo and Gadducci, Fabio and Lomurno, Giuseppe and Tedeschi, Gabriele},
title = {{Effect Semantics for Quantum Process Calculi}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {16:1--16:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.16},
URN = {urn:nbn:de:0030-drops-207886},
doi = {10.4230/LIPIcs.CONCUR.2024.16},
annote = {Keywords: Quantum process calculi, probabilistic LTSs, effect LTSs}
}
Document
Invariants for One-Counter Automata with Disequality Tests
Abstract
We study the reachability problem for one-counter automata in which transitions can carry disequality tests. A disequality test is a guard that prohibits a specified counter value. This reachability problem has been known to be NP-hard and in PSPACE, and characterising its computational complexity has been left as a challenging open question by Almagor, Cohen, Pérez, Shirmohammadi, and Worrell (2020). We reduce the complexity gap, placing the problem into the second level of the polynomial hierarchy, namely into the class coNP^NP. In the presence of both equality and disequality tests, our upper bound is at the third level, P^NP^NP.
To prove this result, we show that non-reachability can be witnessed by a pair of invariants (forward and backward). These invariants are almost inductive. They aim to over-approximate only a "core" of the reachability set instead of the entire set. The invariants are also leaky: it is possible to escape the set. We complement this with separate checks as the leaks can only occur in a controlled way.
Cite as
Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks, and Nicolas Waldburger. Invariants for One-Counter Automata with Disequality Tests. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2024.17,
author = {Chistikov, Dmitry and Leroux, J\'{e}r\^{o}me and Sinclair-Banks, Henry and Waldburger, Nicolas},
title = {{Invariants for One-Counter Automata with Disequality Tests}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {17:1--17:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.17},
URN = {urn:nbn:de:0030-drops-207898},
doi = {10.4230/LIPIcs.CONCUR.2024.17},
annote = {Keywords: Inductive invariant, Vector addition system, One-counter automaton}
}
Document
Weighted Basic Parallel Processes and Combinatorial Enumeration
Abstract
We study weighted basic parallel processes (WBPP), a nonlinear recursive generalisation of weighted finite automata inspired from process algebra and Petri net theory. Our main result is an algorithm of 2-EXPSPACE complexity for the WBPP equivalence problem. While (unweighted) BPP language equivalence is undecidable, we can use this algorithm to decide multiplicity equivalence of BPP and language equivalence of unambiguous BPP, with the same complexity. These are long-standing open problems for the related model of weighted context-free grammars.
Our second contribution is a connection between WBPP, power series solutions of systems of polynomial differential equations, and combinatorial enumeration. To this end we consider constructible differentially finite power series (CDF), a class of multivariate differentially algebraic series introduced by Bergeron and Reutenauer in order to provide a combinatorial interpretation to differential equations. CDF series generalise rational, algebraic, and a large class of D-finite (holonomic) series, for which no complexity upper bound for equivalence was known. We show that CDF series correspond to commutative WBPP series. As a consequence of our result on WBPP and commutativity, we show that equivalence of CDF power series can be decided with 2-EXPTIME complexity.
In order to showcase the CDF equivalence algorithm, we show that CDF power series naturally arise from combinatorial enumeration, namely as the exponential generating series of constructible species of structures. Examples of such species include sequences, binary trees, ordered trees, Cayley trees, set partitions, series-parallel graphs, and many others. As a consequence of this connection, we obtain an algorithm to decide multiplicity equivalence of constructible species, decidability of which was not known before.
The complexity analysis is based on effective bounds from algebraic geometry, namely on the length of chains of polynomial ideals constructed by repeated application of finitely many, not necessarily commuting derivations of a multivariate polynomial ring. This is obtained by generalising a result of Novikov and Yakovenko in the case of a single derivation, which is noteworthy since generic bounds on ideal chains are non-primitive recursive in general. On the way, we develop the theory of WBPP series and CDF power series, exposing several of their appealing properties.
Cite as
Lorenzo Clemente. Weighted Basic Parallel Processes and Combinatorial Enumeration. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{clemente:LIPIcs.CONCUR.2024.18,
author = {Clemente, Lorenzo},
title = {{Weighted Basic Parallel Processes and Combinatorial Enumeration}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {18:1--18:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.18},
URN = {urn:nbn:de:0030-drops-207903},
doi = {10.4230/LIPIcs.CONCUR.2024.18},
annote = {Keywords: weighted automata, combinatorial enumeration, shuffle, algebraic differential equations, process algebra, basic parallel processes, species of structures}
}
Document
Computing Inductive Invariants of Regular Abstraction Frameworks
Abstract
Regular transition systems (RTS) are a popular formalism for modeling infinite-state systems in general, and parameterised systems in particular. In a CONCUR 22 paper, Esparza et al. introduce a novel approach to the verification of RTS, based on inductive invariants. The approach computes the intersection of all inductive invariants of a given RTS that can be expressed as CNF formulas with a bounded number of clauses, and uses it to construct an automaton recognising an overapproximation of the reachable configurations. The paper shows that the problem of deciding if the language of this automaton intersects a given regular set of unsafe configurations is in EXPSPACE and PSPACE-hard.
We introduce regular abstraction frameworks, a generalisation of the approach of Esparza et al., very similar to the regular abstractions of Hong and Lin. A framework consists of a regular language of constraints, and a transducer, called the interpretation, that assigns to each constraint the set of configurations of the RTS satisfying it. Examples of regular abstraction frameworks include the formulas of Esparza et al., octagons, bounded difference matrices, and views. We show that the generalisation of the decision problem above to regular abstraction frameworks remains in EXPSPACE, and prove a matching (non-trivial) EXPSPACE-hardness bound.
EXPSPACE-hardness implies that, in the worst case, the automaton recognising the overapproximation of the reachable configurations has a double-exponential number of states. We introduce a learning algorithm that computes this automaton in a lazy manner, stopping whenever the current hypothesis is already strong enough to prove safety. We report on an implementation and show that our experimental results improve on those of Esparza et al.
Cite as
Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr. Computing Inductive Invariants of Regular Abstraction Frameworks. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{czerner_et_al:LIPIcs.CONCUR.2024.19,
author = {Czerner, Philipp and Esparza, Javier and Krasotin, Valentin and Welzel-Mohr, Christoph},
title = {{Computing Inductive Invariants of Regular Abstraction Frameworks}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {19:1--19:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.19},
URN = {urn:nbn:de:0030-drops-207919},
doi = {10.4230/LIPIcs.CONCUR.2024.19},
annote = {Keywords: Regular model checking, abstraction, inductive invariants}
}
Document
Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques
Abstract
Behavioural distances of transition systems modelled via coalgebras for endofunctors generalize traditional notions of behavioural equivalence to a quantitative setting, in which states are equipped with a measure of how (dis)similar they are. Endowing transition systems with such distances essentially relies on the ability to lift functors describing the one-step behavior of the transition systems to the category of pseudometric spaces. We consider the category theoretic generalization of the Kantorovich lifting from transportation theory to the case of lifting functors to quantale-valued relations, which subsumes equivalences, preorders and (directed) metrics. We use tools from fibred category theory, which allow one to see the Kantorovich lifting as arising from an appropriate fibred adjunction. Our main contributions are compositionality results for the Kantorovich lifting, where we show that that the lifting of a composed functor coincides with the composition of the liftings. In addition, we describe how to lift distributive laws in the case where one of the two functors is polynomial (with finite coproducts). These results are essential ingredients for adapting up-to-techniques to the case of quantale-valued behavioural distances. Up-to techniques are a well-known coinductive technique for efficiently showing lower bounds for behavioural distances. We illustrate the results of our paper in two case studies.
Cite as
Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, and Paul Wild. Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{dangelo_et_al:LIPIcs.CONCUR.2024.20,
author = {D'Angelo, Keri and Gurke, Sebastian and Kirss, Johanna Maria and K\"{o}nig, Barbara and Najafi, Matina and R\'{o}\.{z}owski, Wojciech and Wild, Paul},
title = {{Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {20:1--20:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.20},
URN = {urn:nbn:de:0030-drops-207921},
doi = {10.4230/LIPIcs.CONCUR.2024.20},
annote = {Keywords: behavioural metrics, coalgebra, Galois connections, quantales, Kantorovich lifting, up-to techniques}
}
Document
Reversible Transducers over Infinite Words
Abstract
Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specification. An important result by Dartois et al. [Luc Dartois et al., 2017] shows that composition of two-way transducers enjoy a polynomial composition when the underlying transducer is reversible, that is, if they are both deterministic and co-deterministic. This is a major improvement over general deterministic two-way transducers, for which composition causes a doubly exponential blow-up in the size of the inputs in general. Moreover, they show that reversible two-way transducers have the same expressiveness as deterministic two-way transducers. However, the notion of reversible two-way transducers over infinite words as well as the question of their expressiveness were not studied yet.
In this article, we introduce the class of reversible two-way transducers over infinite words and show that they enjoy the same expressive power as deterministic two-way transducers over infinite words. This is done through a non-trivial, effective construction inducing a single exponential blow-up in the set of states. Further, we also prove that composing two reversible two-way transducers over infinite words incurs only a polynomial complexity, thereby providing an efficient procedure for composition of transducers over infinite words.
Cite as
Luc Dartois, Paul Gastin, Loïc Germerie Guizouarn, R. Govind, and Shankaranarayanan Krishna. Reversible Transducers over Infinite Words. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{dartois_et_al:LIPIcs.CONCUR.2024.21,
author = {Dartois, Luc and Gastin, Paul and Germerie Guizouarn, Lo\"{i}c and Govind, R. and Krishna, Shankaranarayanan},
title = {{Reversible Transducers over Infinite Words}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {21:1--21:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.21},
URN = {urn:nbn:de:0030-drops-207932},
doi = {10.4230/LIPIcs.CONCUR.2024.21},
annote = {Keywords: Transducers, Regular functions, Reversibility, Composition, SSTs}
}
Document
An Automata-Based Approach for Synchronizable Mailbox Communication
Abstract
We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends). A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. Previous work mostly considered the setting where rounds have fixed size. Our main contribution shows that the problem whether a mailbox communication system complies with the round-based policy, with no size limitation on rounds, is PSPACE-complete. For this we use a novel automata-based approach, that also allows to determine the precise complexity (PSPACE) of several questions considered in previous literature.
Cite as
Romain Delpy, Anca Muscholl, and Grégoire Sutre. An Automata-Based Approach for Synchronizable Mailbox Communication. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{delpy_et_al:LIPIcs.CONCUR.2024.22,
author = {Delpy, Romain and Muscholl, Anca and Sutre, Gr\'{e}goire},
title = {{An Automata-Based Approach for Synchronizable Mailbox Communication}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {22:1--22:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.22},
URN = {urn:nbn:de:0030-drops-207947},
doi = {10.4230/LIPIcs.CONCUR.2024.22},
annote = {Keywords: Concurrent programming, Mailbox communication, Verification}
}
Document
Regular Games with Imperfect Information Are Not That Regular
Abstract
We consider two-player games with imperfect information and the synthesis of a randomized strategy for one player that ensures the objective is satisfied almost-surely (i.e., with probability 1), regardless of the strategy of the other player. Imperfect information is modeled by an indistinguishability relation describing the pairs of histories that the first player cannot distinguish, a generalization of the traditional model with partial observations. The game is regular if it admits a regular function whose kernel commutes with the indistinguishability relation.
The synthesis of pure strategies that ensure all possible outcomes satisfy the objective is possible in regular games, by a generic reduction that holds for all objectives. While the solution for pure strategies extends to randomized strategies in the traditional model with partial observations (which is always regular), a similar reduction does not exist in the more general model. Despite that, we show that in regular games with Büchi objectives the synthesis problem is decidable for randomized strategies that ensure the outcome satisfies the objective almost-surely.
Cite as
Laurent Doyen and Thomas Soullard. Regular Games with Imperfect Information Are Not That Regular. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{doyen_et_al:LIPIcs.CONCUR.2024.23,
author = {Doyen, Laurent and Soullard, Thomas},
title = {{Regular Games with Imperfect Information Are Not That Regular}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {23:1--23:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.23},
URN = {urn:nbn:de:0030-drops-207953},
doi = {10.4230/LIPIcs.CONCUR.2024.23},
annote = {Keywords: Imperfect-information games, randomized strategies, synthesis}
}
Document
Validity of Contextual Formulas
Abstract
Many well-known logical identities are naturally written as equivalences between contextual formulas. A simple example is the Boole-Shannon expansion c[p] ≡ (p ∧ c[true]) ∨ (¬ p ∧ c[false]), where c denotes an arbitrary formula with possibly multiple occurrences of a "hole", called a context, and c[φ] denotes the result of "filling" all holes of c with the formula φ. Another example is the unfolding rule μX.c[X] ≡ c[μX.c[X]] of the modal μ-calculus.
We consider the modal μ-calculus as overarching temporal logic and, as usual, reduce the problem whether φ₁ ≡ φ₂ holds for contextual formulas φ₁, φ₂ to the problem whether φ₁ ↔ φ₂ is valid. We show that the problem whether a contextual formula of the μ-calculus is valid for all contexts can be reduced to validity of ordinary formulas. Our first result constructs a canonical context such that a formula is valid for all contexts iff it is valid for this particular one. However, the ordinary formula is exponential in the nesting-depth of the context variables. In a second result we solve this problem, thus proving that validity of contextual formulas is EXP-complete, as for ordinary equivalences. We also prove that both results hold for CTL and LTL as well. We conclude the paper with some experimental results. In particular, we use our implementation to automatically prove the correctness of a set of six contextual equivalences of LTL recently introduced by Esparza et al. for the normalization of LTL formulas. While Esparza et al. need several pages of manual proof, our tool only needs milliseconds to do the job and to compute counterexamples for incorrect variants of the equivalences.
Cite as
Javier Esparza and Rubén Rubio. Validity of Contextual Formulas. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{esparza_et_al:LIPIcs.CONCUR.2024.24,
author = {Esparza, Javier and Rubio, Rub\'{e}n},
title = {{Validity of Contextual Formulas}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {24:1--24:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.24},
URN = {urn:nbn:de:0030-drops-207965},
doi = {10.4230/LIPIcs.CONCUR.2024.24},
annote = {Keywords: \mu-calculus, temporal logic, contextual rules}
}
Document
A Unifying Categorical View of Nondeterministic Iteration and Tests
Abstract
We study Kleene iteration in the categorical context. A celebrated completeness result by Kozen introduced Kleene algebra (with tests) as a ubiquitous tool for lightweight reasoning about program equivalence, and yet, numerous variants of it came along afterwards to answer the demand for more refined flavors of semantics, such as stateful, concurrent, exceptional, hybrid, branching time, etc. We detach Kleene iteration from Kleene algebra and analyze it from the categorical perspective. The notion, we arrive at is that of Kleene-iteration category (with coproducts and tests), which we show to be general and robust in the sense of compatibility with programming language features, such as exceptions, store, concurrent behaviour, etc. We attest the proposed notion w.r.t. various yardsticks, most importantly, by characterizing the free model as a certain category of (nondeterministic) rational trees.
Cite as
Sergey Goncharov and Tarmo Uustalu. A Unifying Categorical View of Nondeterministic Iteration and Tests. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{goncharov_et_al:LIPIcs.CONCUR.2024.25,
author = {Goncharov, Sergey and Uustalu, Tarmo},
title = {{A Unifying Categorical View of Nondeterministic Iteration and Tests}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {25:1--25:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.25},
URN = {urn:nbn:de:0030-drops-207979},
doi = {10.4230/LIPIcs.CONCUR.2024.25},
annote = {Keywords: Kleene iteration, Elgot iteration, Kleene algebra, coalgebraic resumptions}
}
Document
Phase-Bounded Broadcast Networks over Topologies of Communication
Abstract
We study networks of processes that all execute the same finite state protocol and that communicate through broadcasts. The processes are organized in a graph (a topology) and only the neighbors of a process in this graph can receive its broadcasts. The coverability problem asks, given a protocol and a state of the protocol, whether there is a topology for the processes such that one of them (at least) reaches the given state. This problem is undecidable [G. Delzanno et al., 2010]. We study here an under-approximation of the problem where processes alternate a bounded number of times k between phases of broadcasting and phases of receiving messages. We show that, if the problem remains undecidable when k is greater than 6, it becomes decidable for k = 2, and ExpSpace-complete for k = 1. Furthermore, we show that if we restrict ourselves to line topologies, the problem is in P for k = 1 and k = 2.
Cite as
Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Phase-Bounded Broadcast Networks over Topologies of Communication. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{guillou_et_al:LIPIcs.CONCUR.2024.26,
author = {Guillou, Lucie and Sangnier, Arnaud and Sznajder, Nathalie},
title = {{Phase-Bounded Broadcast Networks over Topologies of Communication}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {26:1--26:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.26},
URN = {urn:nbn:de:0030-drops-207987},
doi = {10.4230/LIPIcs.CONCUR.2024.26},
annote = {Keywords: Parameterized verification, Coverability, Broadcast Networks}
}
Document
Inaproximability in Weighted Timed Games
Abstract
We consider two-player, turn-based weighted timed games played on timed automata equipped with (positive and negative) integer weights, in which one player seeks to reach a goal location whilst minimising the cumulative weight of the underlying path. Although the value problem for such games (is the value of the game below a given threshold?) is known to be undecidable, the question of whether one can approximate this value has remained a longstanding open problem. In this paper, we resolve this question by showing that approximating arbitrarily closely the value of a given weighted timed game is computationally unsolvable.
Cite as
Quentin Guilmant and Joël Ouaknine. Inaproximability in Weighted Timed Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{guilmant_et_al:LIPIcs.CONCUR.2024.27,
author = {Guilmant, Quentin and Ouaknine, Jo\"{e}l},
title = {{Inaproximability in Weighted Timed Games}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {27:1--27:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.27},
URN = {urn:nbn:de:0030-drops-207998},
doi = {10.4230/LIPIcs.CONCUR.2024.27},
annote = {Keywords: Weighted timed games, approximation, undecidability}
}
Document
Faster and Smaller Solutions of Obliging Games
Abstract
Obliging 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.
Cite as
Daniel Hausmann and Nir Piterman. Faster and Smaller Solutions of Obliging Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{hausmann_et_al:LIPIcs.CONCUR.2024.28,
author = {Hausmann, Daniel and Piterman, Nir},
title = {{Faster and Smaller Solutions of Obliging Games}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {28:1--28:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.28},
URN = {urn:nbn:de:0030-drops-208008},
doi = {10.4230/LIPIcs.CONCUR.2024.28},
annote = {Keywords: Two-player games, reactive synthesis, Emerson-Lei games, parity games}
}
Document
Strategic Dominance: A New Preorder for Nondeterministic Processes
Abstract
We study the following refinement relation between nondeterministic state-transition models: model ℬ strategically dominates model 𝒜 iff every deterministic refinement of 𝒜 is language contained in some deterministic refinement of ℬ. While language containment is trace inclusion, and the (fair) simulation preorder coincides with tree inclusion, strategic dominance falls strictly between the two and can be characterized as "strategy inclusion" between 𝒜 and ℬ: every strategy that resolves the nondeterminism of 𝒜 is dominated by a strategy that resolves the nondeterminism of ℬ. Strategic dominance can be checked in 2-ExpTime by a decidable first-order Presburger logic with quantification over words and strategies, called resolver logic. We give several other applications of resolver logic, including checking the co-safety, co-liveness, and history-determinism of boolean and quantitative automata, and checking the inclusion between hyperproperties that are specified by nondeterministic boolean and quantitative automata.
Cite as
Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Strategic Dominance: A New Preorder for Nondeterministic Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{henzinger_et_al:LIPIcs.CONCUR.2024.29,
author = {Henzinger, Thomas A. and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
title = {{Strategic Dominance: A New Preorder for Nondeterministic Processes}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {29:1--29:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.29},
URN = {urn:nbn:de:0030-drops-208011},
doi = {10.4230/LIPIcs.CONCUR.2024.29},
annote = {Keywords: quantitative automata, refinement relation, resolver, strategy, history-determinism}
}
Document
Around Classical and Intuitionistic Linear Processes
Abstract
Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classical versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to ILL due to Laurent, we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey. Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency.
Cite as
Juan C. Jaramillo, Dan Frumin, and Jorge A. Pérez. Around Classical and Intuitionistic Linear Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{jaramillo_et_al:LIPIcs.CONCUR.2024.30,
author = {Jaramillo, Juan C. and Frumin, Dan and P\'{e}rez, Jorge A.},
title = {{Around Classical and Intuitionistic Linear Processes}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {30:1--30:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.30},
URN = {urn:nbn:de:0030-drops-208026},
doi = {10.4230/LIPIcs.CONCUR.2024.30},
annote = {Keywords: Process calculi, session types, linear logic}
}
Document
Bi-Reachability in Petri Nets with Data
Abstract
We investigate Petri nets with data, an extension of plain Petri nets where tokens carry values from an infinite data domain, and executability of transitions is conditioned by equalities between data values. We provide a decision procedure for the bi-reachability problem: given a Petri net and its two configurations, we ask if each of the configurations is reachable from the other. This pushes forward the decidability borderline, as the bi-reachability problem subsumes the coverability problem (which is known to be decidable) and is subsumed by the reachability problem (whose decidability status is unknown).
Cite as
Łukasz Kamiński and Sławomir Lasota. Bi-Reachability in Petri Nets with Data. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 31:1-31:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{kaminski_et_al:LIPIcs.CONCUR.2024.31,
author = {Kami\'{n}ski, {\L}ukasz and Lasota, S{\l}awomir},
title = {{Bi-Reachability in Petri Nets with Data}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {31:1--31:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.31},
URN = {urn:nbn:de:0030-drops-208038},
doi = {10.4230/LIPIcs.CONCUR.2024.31},
annote = {Keywords: Petri nets, Petri nets with data, reachability, bi-reachability, reversible reachability, mutual reachability, orbit-finite sets}
}
Document
Minimising the Probabilistic Bisimilarity Distance
Abstract
A labelled Markov decision process (MDP) is a labelled Markov chain with nondeterminism; i.e., together with a strategy a labelled MDP induces a labelled Markov chain. The model is related to interval Markov chains. Motivated by applications to the verification of probabilistic noninterference in security, we study problems of minimising probabilistic bisimilarity distances of labelled MDPs, in particular, whether there exist strategies such that the probabilistic bisimilarity distance between the induced labelled Markov chains is less than a given rational number, both for memoryless strategies and general strategies. We show that the distance minimisation problem is ∃ℝ-complete for memoryless strategies and undecidable for general strategies. We also study the computational complexity of the qualitative problem about making the distance less than one. This problem is known to be NP-complete for memoryless strategies. We show that it is EXPTIME-complete for general strategies.
Cite as
Stefan Kiefer and Qiyi Tang. Minimising the Probabilistic Bisimilarity Distance. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2024.32,
author = {Kiefer, Stefan and Tang, Qiyi},
title = {{Minimising the Probabilistic Bisimilarity Distance}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {32:1--32:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.32},
URN = {urn:nbn:de:0030-drops-208049},
doi = {10.4230/LIPIcs.CONCUR.2024.32},
annote = {Keywords: Markov decision processes, Markov chains}
}
Document
Automating Memory Model Metatheory with Intersections
Abstract
In the weak memory consistency literature, the semantics of concurrent programs is typically defined as a constraint on execution graphs, expressed in relational algebra. Prior work has shown that basic metatheoretic questions about memory models are decidable as long as they can be expressed as irreflexivity and emptiness constraints over Kleene Algebra with Tests (KAT), a condition that rules out practical memory models such the C/C++ and the Linux kernel models.
In this paper, we extend these results to memory models containing arbitrary intersections with uninterpreted relations. We can thus automatically establish compilation correctness and derive efficient incremental consistency checkers for RC11, LKMM, and other memory models.
Cite as
Aristotelis Koutsouridis, Michalis Kokologiannakis, and Viktor Vafeiadis. Automating Memory Model Metatheory with Intersections. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{koutsouridis_et_al:LIPIcs.CONCUR.2024.33,
author = {Koutsouridis, Aristotelis and Kokologiannakis, Michalis and Vafeiadis, Viktor},
title = {{Automating Memory Model Metatheory with Intersections}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {33:1--33:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.33},
URN = {urn:nbn:de:0030-drops-208050},
doi = {10.4230/LIPIcs.CONCUR.2024.33},
annote = {Keywords: Kleene Algebra, Weak Memory Models}
}
Document
On Continuous Pushdown VASS in One Dimension
Abstract
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown stack. The algorithmic analysis of PVASS has applications such as static analysis of recursive programs manipulating integer variables. Unfortunately, reachability analysis, even for one-dimensional PVASS is not known to be decidable. So, we relax the model of one-dimensional PVASS to make the counter updates continuous and show that in this case reachability, coverability, and boundedness are decidable in polynomial time. In addition, for the extension of the model with lower-bound guards on the states, we show that coverability and reachability are NP-complete, and boundedness is coNP-complete.
Cite as
Guillermo A. Pérez and Shrisha Rao. On Continuous Pushdown VASS in One Dimension. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{perez_et_al:LIPIcs.CONCUR.2024.34,
author = {P\'{e}rez, Guillermo A. and Rao, Shrisha},
title = {{On Continuous Pushdown VASS in One Dimension}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {34:1--34:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.34},
URN = {urn:nbn:de:0030-drops-208065},
doi = {10.4230/LIPIcs.CONCUR.2024.34},
annote = {Keywords: Vector addition systems, Pushdown automata, Reachability}
}
Document
Nominal Tree Automata with Name Allocation
Abstract
Data trees serve as an abstraction of structured data, such as XML documents. A number of specification formalisms for languages of data trees have been developed, many of them adhering to the paradigm of register automata, which is based on storing data values encountered on the tree in registers for subsequent comparison with further data values. Already on word languages, the expressiveness of such automata models typically increases with the power of control (e.g. deterministic, non-deterministic, alternating). Language inclusion is typically undecidable for non-deterministic or alternating models unless the number of registers is radically restricted, and even then often remains non-elementary. We present an automaton model for data trees that retains a reasonable level of expressiveness, in particular allows non-determinism and any number of registers, while admitting language inclusion checking in elementary complexity, in fact in parametrized exponential time. We phrase the description of our automaton model in the language of nominal sets, building on the recently introduced paradigm of explicit name allocation in nominal automata.
Cite as
Simon Prucker and Lutz Schröder. Nominal Tree Automata with Name Allocation. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{prucker_et_al:LIPIcs.CONCUR.2024.35,
author = {Prucker, Simon and Schr\"{o}der, Lutz},
title = {{Nominal Tree Automata with Name Allocation}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {35:1--35:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.35},
URN = {urn:nbn:de:0030-drops-208071},
doi = {10.4230/LIPIcs.CONCUR.2024.35},
annote = {Keywords: Data languages, tree automata, nominal automata, inclusion checking}
}
Document
Branching Bisimilarity for Processes with Time-Outs
Abstract
This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process algebra with recursion. The last section presents a complete axiomatisation for guarded processes without infinite sequences of unobservable actions.
Cite as
Gaspard Reghem and Rob J. van Glabbeek. Branching Bisimilarity for Processes with Time-Outs. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{reghem_et_al:LIPIcs.CONCUR.2024.36,
author = {Reghem, Gaspard and van Glabbeek, Rob J.},
title = {{Branching Bisimilarity for Processes with Time-Outs}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {36:1--36:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.36},
URN = {urn:nbn:de:0030-drops-208082},
doi = {10.4230/LIPIcs.CONCUR.2024.36},
annote = {Keywords: Reactive Systems, Time-outs, Branching Bisimilarity, Modal Characterisation, Congruence, Axiomatisation}
}
Document
A Spectrum of Approximate Probabilistic Bisimulations
Abstract
This paper studies various notions of approximate probabilistic bisimulation on labeled Markov chains (LMCs). We introduce approximate versions of weak and branching bisimulation, as well as a notion of ε-perturbed bisimulation that relates LMCs that can be made (exactly) probabilistically bisimilar by small perturbations of their transition probabilities. We explore how the notions interrelate and establish their connections to other well-known notions like ε-bisimulation.
Cite as
Timm Spork, Christel Baier, Joost-Pieter Katoen, Jakob Piribauer, and Tim Quatmann. A Spectrum of Approximate Probabilistic Bisimulations. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{spork_et_al:LIPIcs.CONCUR.2024.37,
author = {Spork, Timm and Baier, Christel and Katoen, Joost-Pieter and Piribauer, Jakob and Quatmann, Tim},
title = {{A Spectrum of Approximate Probabilistic Bisimulations}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {37:1--37:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.37},
URN = {urn:nbn:de:0030-drops-208099},
doi = {10.4230/LIPIcs.CONCUR.2024.37},
annote = {Keywords: Markov chains, Approximate bisimulation, Abstraction, Model checking}
}
Document
Progress, Justness and Fairness in Modal μ-Calculus Formulae
Abstract
When verifying liveness properties on a transition system, it is often necessary to discard spurious violating paths by making assumptions on which paths represent realistic executions. Capturing that some property holds under such an assumption in a logical formula is challenging and error-prone, particularly in the modal μ-calculus. In this paper, we present template formulae in the modal μ-calculus that can be instantiated to a broad range of liveness properties. We consider the following assumptions: progress, justness, weak fairness, strong fairness, and hyperfairness, each with respect to actions. The correctness of these formulae has been proven.
Cite as
Myrthe S. C. Spronck, Bas Luttik, and Tim A. C. Willemse. Progress, Justness and Fairness in Modal μ-Calculus Formulae. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 38:1-38:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{spronck_et_al:LIPIcs.CONCUR.2024.38,
author = {Spronck, Myrthe S. C. and Luttik, Bas and Willemse, Tim A. C.},
title = {{Progress, Justness and Fairness in Modal \mu-Calculus Formulae}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {38:1--38:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.38},
URN = {urn:nbn:de:0030-drops-208102},
doi = {10.4230/LIPIcs.CONCUR.2024.38},
annote = {Keywords: Modal \mu-calculus, Property specification, Completeness criteria, Progress, Justness, Fairness, Liveness properties}
}
Document
Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions
Abstract
We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results on graph conditions. Furthermore we introduce a notion of witnesses, allowing the detection of infinite models in some cases. To ensure completeness, paths in a tableau must be fair, where fairness requires that all parts of a condition are processed eventually. Since the correctness arguments are non-trivial, we rely on coinductive proof methods and up-to techniques that structure the arguments. We distinguish between two types of categories: categories where all sections are isomorphisms, allowing for a simpler tableau calculus that includes finite model generation; in categories where this requirement does not hold, model generation does not work, but we still obtain a sound and complete calculus.
Cite as
Lara Stoltenow, Barbara König, Sven Schneider, Andrea Corradini, Leen Lambers, and Fernando Orejas. Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 39:1-39:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{stoltenow_et_al:LIPIcs.CONCUR.2024.39,
author = {Stoltenow, Lara and K\"{o}nig, Barbara and Schneider, Sven and Corradini, Andrea and Lambers, Leen and Orejas, Fernando},
title = {{Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {39:1--39:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.39},
URN = {urn:nbn:de:0030-drops-208113},
doi = {10.4230/LIPIcs.CONCUR.2024.39},
annote = {Keywords: satisfiability, graph conditions, coinductive techniques, category theory}
}
Document
A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs
Abstract
Markov Decision Processes (MDPs) model systems with uncertain transition dynamics. Multiple-environment MDPs (MEMDPs) extend MDPs. They intuitively reflect finite sets of MDPs that share the same state and action spaces but differ in the transition dynamics. The key objective in MEMDPs is to find a single strategy that satisfies a given objective in every associated MDP. The main result of this paper is PSPACE-completeness for almost-sure Rabin objectives in MEMDPs. This result clarifies the complexity landscape for MEMDPs and contrasts with results for the more general class of partially observable MDPs (POMDPs), where almost-sure reachability is already EXP-complete, and almost-sure Rabin objectives are undecidable.
Cite as
Marnix Suilen, Marck van der Vegt, and Sebastian Junges. A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 40:1-40:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{suilen_et_al:LIPIcs.CONCUR.2024.40,
author = {Suilen, Marnix and van der Vegt, Marck and Junges, Sebastian},
title = {{A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs}},
booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)},
pages = {40:1--40:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-339-3},
ISSN = {1868-8969},
year = {2024},
volume = {311},
editor = {Majumdar, Rupak and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.40},
URN = {urn:nbn:de:0030-drops-208120},
doi = {10.4230/LIPIcs.CONCUR.2024.40},
annote = {Keywords: Markov Decision Processes, partial observability, linear-time Objectives}
}