We study two-player zero-sum turn-based games played on graphs with multiple reachability objectives called generalised reachability games. In classic reachability games the goal of one player, Eve, is to visit a given target set of vertices, and that of the other player, Adam, is to prevent this. In generalised reachability games, the single target set is replaced with a family of target sets and the objective of Eve is to visit all of them in any order. We study the complexity of deciding the winner in two-player games with generalised reachability objectives. Our study reveals that an important parameter that determines the complexity of this problem is the size of the target sets. We first prove that deciding the winner in such games is PSPACE-complete, and the PSPACE lower bound holds even when the size of each target set is at most three. By contrast, we show that the problem is FPT in the number of target sets of size greater than one. Moreover, we consider the memory requirements for both players and give matching upper and lower bounds on the sizes of winning strategies. We also study optimisation variants of these games. For the optimisation problems, we show intractability for most interesting cases. Particularly, in contrast to the tractability of generalised reachability in the case with singleton target sets, the optimisation problem is coNP-hard when Eve tries to maximise the number of target sets that are visited. Tractability of this case can be recovered in a different optimisation setting where Eve is required to pledge a maximum sized subset of target sets that she can guarantee to visit.

Nearly a decade ago, Calude et al. showed that parity games can be solved in quasi-polynomial time. This result is now understood in terms of universal trees. By reduction to parity games, the quasi-polymonial result can benefit all omega-regular games. However, beyond such reductions, and with the exception of Rabin games, our understanding of the role of universal trees in direct solutions is still quite limited. In this work, we refute the common view that universal trees are relevant only for games that admit memoryless winning strategies. We contribute a full understanding of how universal trees interact with Zielonka trees for the solution of Streett and Emerson-Lei games. As a consequence, we show that winning regions and strategies in Streett games with n vertices, m edges, and k pairs can be computed in time O(mklog(k)k!|U(n,k)|), where U(n,k) is a universal tree for n leaves and depth k. This improves upon the best previously known complexity result for Streett games, which relied on reduction to parity games and their quasi-polynomial solution. Furthermore, we show that winning regions and strategies for Emerson-Lei games with n vertices, m edges, and c colors can be computed in time O(mclog(c)c!|U(n,c/2)|), again improving over reductions to parity games. Notably, our approach yields memory-optimal strategies, in contrast to those obtained via reductions to parity games. Finally, we show how universal trees can be used to bound the recursion tree of the Zielonka-McNaughton algorithm for Emerson-Lei games. This leads to a symbolic algorithm that replaces the factor n^c in the time complexity of existing symbolic approaches with |U(n,c)|.

We study synthesis for obligation properties expressed in LTLfp, the extension of LTLf to infinite traces. Obligation properties are positive Boolean combinations of safety and guarantee (co-safety) properties and form the second level of the temporal hierarchy of Manna and Pnueli. Although obligation properties are expressed over infinite traces, they retain most of the simplicity of LTLf. In particular, we show that they admit a translation into symbolically represented deterministic weak automata (DWA) obtained directly from the symbolic deterministic finite automata (DFA) for the underlying LTLf properties on trace prefixes. DWA inherit many of the attractive algorithmic features of DFA, including Boolean closure and polynomial-time minimization. Moreover, we show that synthesis for LTLfp obligation properties is theoretically highly efficient - solvable in linear time once the DWA is constructed. We investigate several symbolic algorithms for solving DWA games that arise in the synthesis of obligation properties and evaluate their effectiveness experimentally. Overall, the results indicate that synthesis for LTLfp obligation properties can be performed with virtually the same effectiveness as LTLf synthesis.

Formal languages over infinite alphabets serve as abstractions of structures and processes carrying data. Automata models over infinite alphabets, such as classical register automata or, equivalently, nominal orbit-finite automata, tend to have computationally hard or even undecidable reasoning problems unless stringent restrictions are imposed on either the power of control or the number of registers. This has been shown to be ameliorated in automata models with name allocation such as regular nondeterministic nominal automata, which allow for deciding language inclusion in elementary complexity even with unboundedly many registers while retaining a reasonable level of expressiveness. In the present work, we demonstrate that elementary complexity survives under extending the power of control to alternation: We introduce regular alternating nominal automata (RANAs), and show that their non-emptiness and inclusion problems have elementary complexity even when the number of registers is unbounded. Moreover, we show that RANAs allow for nearly complete de-alternation, specifically de-alternation up to a single deadlocked universal state. As a corollary to our results, we improve the complexity of model checking for a flavour of Bar-μTL, a fixed-point logic with name allocation over finite data words, by one exponential level.

Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLfp and PPLTLp, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. In this paper, we present the first actual solvers for reactive synthesis in these logics. These are based on games on graphs that leverage DFA-based techniques from LTLf/PPLTL to construct the game arena. We start with a symbolic solver based on Emerson-Lei games, which reduces lower-class properties (guarantee, safety) to higher ones (recurrence, persistence) before solving the game. We then introduce Manna-Pnueli games, which natively embed Manna-Pnueli objectives into the arena. These games are solved by composing solutions to a DAG of simpler Emerson-Lei games, resulting in a provably more efficient approach. We implemented the solvers and practically evaluated their performance on a range of representative formulas. The results show that Manna-Pnueli games often offer significant advantages, though not universally, indicating that combining both approaches could further enhance practical performance.

The semantics of alternating-time temporal logic (ATL) and the more expressive alternating-time μ-calculus (AMC) is standardly given in terms of concurrent game frames (CGF). The information required to interpret AMC formulas is equivalently represented in terms of effectivity frames in the sense of Pauly; in many cases, this representation is more compact than the corresponding CGF, and in principle allows for faster evaluation of coalitional modalities. In the present work, we investigate whether implementing a model checker based on effectivity frames leads to better performance in practice. We implement the translation from concurrent game frames to effectivity frames and analyse performance gains in model checking based on corresponding instantiations of a generic model checker for coalgebraic μ-calculi, using dedicated benchmark series as well as random systems and formulas. In the process, we also compare performance to the state-of-the-art ATL model checkerMCMAS. Our results indicate that on large systems, the overhead involved in converting a CGF to an effectivity frame is often outweighed by the benefits in subsequent model checking.

We propose a method for solving parity games with acyclic (DAG) sub-structures by computing nested fixpoints of a DAG attractor function that lives over the non-DAG parts of the game, thereby restricting the domain of the involved fixpoint operators. Intuitively, this corresponds to accelerating fixpoint computation by inlining cycle-free parts during the solution of parity games, leading to earlier convergence. We also present an economic later-appearance-record construction that takes Emerson-Lei games to parity games, and show that it preserves DAG sub-structures; it follows that the proposed method can be used also for the accelerated solution of Emerson-Lei games.

We study how to distribute trace languages in a setting where processes communicate via reconfigurable communication channels. That is, the different processes can connect and disconnect from channels at run time. We restrict attention to communication via tree-like communication architectures. These allow channels to connect more than two processes in a way that maintains an underlying spanning tree and keeps communication continuous on the tree. We make the reconfiguration explicit in the language allowing both a centralized automaton as well as the distributed processes to share relevant information about the current communication configuration. We show that Zielonka's seminal result regarding distribution of regular languages for asynchronous automata can be generalized in this setting, incorporating both reconfiguration and more than binary tree architectures.

RATIONALE AND OBJECTIVES:Multiparametric MRI (mpMRI) substantially improves the detection of significant prostate carcinoma (PCa) compared to systematic biopsy. Nevertheless, mpMRI can overlook aggressive forms of PCa. Recent studies showed, that infiltrative growth (INF) has less restricted diffusion. This study aims to explore the impact of growth patterns on the detection of lesions. MATERIALS AND METHODS:This retrospective study analyzed 52 patients who underwent radical prostatectomy, with preoperative mpMRI. For each patient, one dominant lesion was identified on one whole-mount prostatectomy section. Two pathologists (P1, P2) independently classified the growth pattern whether as expansive (EXP) being defined with at least three 5mm² regions of interest consisting entirely of carcinoma without benign glands or else as infiltrative (INF). Two radiologists (R1, R2) independently classified selected lesions according to PI-RADSv2.1. based on pathological localization. Apparent diffusion coefficient (ADC) values were measured in correlation with matched histopathology slides. Interreader-agreement was evaluated using weighted Cohen's Kappa. The relationship between PI-RADS scores and pathological diagnoses was analyzed using logistic regression. RESULTS:Pathologic lesion characterization regarding growth patterns achieved almost perfect agreement (κ = 0.88), so did PI-RADS classification of mpMRI (κ = 0.90). PI-RADS scores correlated significantly with EXP growth patterns. Average ADC values were lower for EXP lesions (0.83×10-3 mm2/s, CI: 0.72-0.94×10-3 mm2/s) compared to INF lesions (0.97×10-3 mm2/s, CI: 0.86-1.07×10-3 mm2/s; p = 0.08). On T2 images, 8 of 28 (29%) INF lesions and 1 of 24 (4%) EXP lesions were not visible. CONCLUSION:PCa missed on mpMRI more frequently demonstrate INF growth patterns. Lesions with EXP growth patterns show lower ADC values and have higher PI-RADS scores.

Emerson-Lei conditions have recently attracted attention due to both their succinctness and their favorable closure properties. In the current work, we show how infinite-duration games with Emerson-Lei objectives can be analyzed in two different ways. First, we show that the Zielonka tree of the Emerson-Lei condition naturally gives rise to a new reduction to parity games. This reduction, however, does not result in optimal analysis. Second, we show based on the first reduction (and the Zielonka tree) how to provide a direct fixpoint-based characterization of the winning region. The fixpoint-based characterization allows for symbolic analysis. It generalizes the solutions of games with known winning conditions such as Büchi, GR[1], parity, Streett, Rabin and Muller objectives, and in the case of these conditions reproduces previously known symbolic algorithms and complexity results. We also show how the capabilities of the proposed algorithm can be exploited in reactive synthesis, suggesting a new expressive fragment of LTL that can be handled symbolically. Our fragment combines a safety specification and a liveness part. The safety part is unrestricted and the liveness part allows to define Emerson-Lei conditions on occurrences of letters. The symbolic treatment is enabled due to the simplicity of determinization in the case of safety languages and by using our new algorithm for game solving. This approach maximizes the number of steps solved symbolically in order to maximize the potential for efficient symbolic implementations.

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.

We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph G=(V,E) and a set of fair moves E_f⊆ E a player is said to play fair in G if they choose an edge e∈ E_f infinitely often whenever the source node of e is visited infinitely often. Otherwise, they play unfair. We equip such games with two ω -regular winning conditions α and β deciding the winner of mutually fair and mutually unfair plays, respectively. Whenever one player plays fair and the other plays unfair, the fairly playing player wins the game. The resulting games are called fair α /β games. We formalize fair α /β games and show that they are determined. For fair parity/parity games, i.e., fair α /β games where α and β are given each by a parity condition over G, we provide a polynomial reduction to (normal) parity games via a gadget construction inspired by the reduction of stochastic parity games to parity games. We further give a direct symbolic fixpoint algorithm to solve fair parity/parity games. On a conceptual level, we illustrate the translation between the gadget-based reduction and the direct symbolic algorithm which uncovers the underlying similarities of solution algorithms for fair and stochastic parity games, as well as for the recently considered class of fair games in which only one player is restricted by fair moves.

The coalgebraic $\mu$-calculus provides a generic semantic framework for fixpoint logics over systems whose branching type goes beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic $\mu$-calculus includes an exponential-time upper bound on satisfiability checking, which however relies on the availability of tableau rules for the next-step modalities that are sufficiently well-behaved in a formally defined sense; in particular, rule matches need to be representable by polynomial-sized codes, and the sequent duals of the rules need to absorb cut. While such rule sets have been identified for some important cases, they are not known to exist in all cases of interest, in particular ones involving either integer weights as in the graded $\mu$-calculus, or real-valued weights in combination with non-linear arithmetic. In the present work, we prove the same upper complexity bound under more general assumptions, specifically regarding the complexity of the (much simpler) satisfiability problem for the underlying one-step logic, roughly described as the nesting-free next-step fragment of the logic. The bound is realized by a generic global caching algorithm that supports on-the-fly satisfiability checking. Notably, our approach directly accommodates unguarded formulae, and thus avoids use of the guardedness transformation. Example applications include new exponential-time upper bounds for satisfiability checking in an extension of the graded $\mu$-calculus with polynomial inequalities (including positive Presburger arithmetic), as well as an extension of the (two-valued) probabilistic $\mu$-calculus with polynomial inequalities.

In recent years, there has been an increasing interest in the connections between supervisory control theory and reactive synthesis. As the two fields use similar techniques there is great hope that technologies from one field could be used in the other. In this spirit, we provide an alternative reduction from the supervisor synthesis problem to solving Büchi games via games with a non-blocking objective. Our reduction is more compact and uniform than previous reductions. As a consequence, it gives an asymptotically better upper bound on the time complexity of the supervisory control synthesis problem. Our reduction also breaks a widely held belief about the impossibility of reducing the supervisory control synthesis problem to a game with a linear winning condition.

We report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (nondeterministic, game-based, probabilistic etc.) and in the next-step modalities used in formulae. The tool implements generic model checking algorithms developed in coalgebraic logic that are easily adapted to concrete instance logics. Apart from the standard modal $\mu$-calculus, COOL-MC currently supports alternating-time, graded, probabilistic and monotone variants of the $\mu$-calculus, but is also effortlessly extensible with new instance logics. The model checking process is realized by polynomial reductions to parity game solving, or, alternatively, by a local model checking algorithm that directly computes the extensions of formulae in a lazy fashion, thereby potentially avoiding the construction of the full parity game. We evaluate COOL-MC on informative benchmark sets.

There is a wide range of modal logics whose semantics goes beyond relational structures, and instead involves, e.g., probabilities, multi-player games, weights, or neighbourhood structures. Coalgebraic logic serves as a unifying semantic and algorithmic framework for such logics. It provides uniform reasoning algorithms that are easily instantiated to particular, concretely given logics. The COOL 2 reasoner provides an implementation of such generic algorithms for coalgebraic modal fixpoint logics. As concrete instances, we obtain in particular reasoners for the aconjunctive and alternation-free fragments of the graded $\mu$-calculus and the alternating-time $\mu$-calculus. We evaluate the tool on standard benchmark sets for fixpoint-free graded modal logic and alternating-time temporal logic (ATL), as well as on a dedicated set of benchmarks for the graded $\mu$-calculus.

. Algorithms for model checking and satisfiability of the modal µ -calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more compli-cated.Wereview the non-emptiness checking of alternating tree automata by a reduction to solving parity games of a certain structure, so-called emptiness games . Since the emptiness problem for alternating tree automata is ExpTime -complete, the size of these games is exponential in the number of states of the input automaton. We show how the construction of the emptiness games combines a (fixed) structural part with (history-)determinization of parity word automata. For tree automata with certain syntactic structures, simpler methods may be used to handle the treatment of the word automata, which then may be asymptotically smaller than in the general case. These results have direct consequences in satisfiability and validity checking for (various fragments of) the modal µ -calculus.

Background The combination of motion-insensitive, high-temporal, and spatial resolution imaging with evaluation of quantitative perfusion has the potential to increase the diagnostic capabilities of magnetic resonance imaging (MRI) in the female pelvis. Purpose To compare a free-breathing compressed-sensing VIBE (fbVIBE) with flexible temporal resolution (range = 4.6–13.8 s) with breath-hold VIBE (bhVIBE) and to evaluate the potential value of quantifying uterine perfusion. Material and Methods A total of 70 datasets from 60 patients (bhVIBE: n = 30; fbVIBE: n = 40) were evaluated by two radiologists. Only temporally resolved reconstruction (fbVIBE) was performed on 30 of the fbVIBE datasets. For a subset (n = 10) of the fbVIBE acquisitions, a time- and motion-resolved reconstruction (mrVIBE) was evaluated. Image quality (IQ), artifacts, diagnostic confidence (DC), and delineation of uterine structures (DoS) were graded on Likert scales (IQ/DC/DoS: 1 (non-diagnostic) to 5 (perfect); artifacts: 1 (no artifacts) to 5 (severe artifacts)). A Tofts model was applied for perfusion analysis. Ktrans was obtained in the myometrium (Mm), junctional zone (Jz), and cervix (Cx). Results The median IQ/DoS/DC scores of fbVIBE (4/5/5 κ >0.7–0.9) and bhVIBE (4/4/4; κ = 0.5–0.7; P > 0.05) were high, but Artifacts were graded low (fbVIBE/bhVIBE: 2/2; κ = 0.6/0.5; P > 0.05). Artifacts were only slightly improved by the additional motion-resolved reconstruction (fbVIBE/mrVIBE: 2/1.5; P = 0.08); fbVIBE was preferred in most cases (7/10). Significant differences of Ktrans values were found between Cx, Jz, and Mm (0.12/0.21/0.19; P < 0.05). Conclusion The fbVIBE sequence allows functional and morphological assessment of the uterus at comparable IQ to bhVIBE.

Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach omega-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e. resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking.

It is well-known that the winning region of a parity game with n nodes and k priorities can be computed as a k-nested fixpoint of a suitable function; straightforward computation of this nested fixpoint requires 𝒪(n^k/2) iterations of the function. Calude et al.’s recent quasipolynomial-time parity game solving algorithm essentially shows how to compute the same fixpoint in only quasipolynomially many iterations by reducing parity games to quasipolynomially sized safety games. Universal graphs have been used to modularize this transformation of parity games to equivalent safety games that are obtained by combining the original game with a universal graph. We show that this approach naturally generalizes to the computation of solutions of systems of any fixpoint equations over finite lattices; hence, the solution of fixpoint equation systems can be computed by quasipolynomially many iterations of the equations. We present applications to modal fixpoint logics and games beyond relational semantics. For instance, the model checking problems for the energy μ -calculus, finite latticed μ -calculi, and the graded and the (two-valued) probabilistic μ -calculus – with numbers coded in binary – can be solved via nested fixpoints of functions that differ substantially from the function for parity games but still can be computed in quasipolynomial time; our result hence implies that model checking for these μ -calculi is in QP . Moreover, we improve the exponent in known exponential bounds on satisfiability checking.