Assumption-Based Argumentation (ABA) is a well-established formalism for modelling and reasoning over debates, with a wide range of applications. However, the high computational complexity of core reasoning tasks in ABA poses a significant challenge for its applicability. This issue is further aggravated when ABA frameworks (ABAFs) are instantiated into graph-based argumentation formalisms, such as Dung's Argumentation Frameworks (AFs) and Argumentation Frameworks with Collective Attacks (SETAFs). In knowledge representation and reasoning, a key strategy to address computational intractability is to optimise reasoning over a given knowledge base through divide-and-conquer algorithms. A paradigmatic example of this approach is splitting, where extensions of a given framework are computed incrementally, by restricting the search space to sub-frameworks only, and then combining the obtained results. This approach has been successfully applied to AFs, for which also a parametrised version has been introduced under stable semantics. However, the exponential growth produced by the instantiation might undermine the usefulness of splitting on the argument graphs induced by ABAFs. To address this issue, our work investigates the concept of splitting on the knowledge base rather than on its graph-based instantiation. Furthermore, we generalise splitting to its parametrised version for ABAFs.

We consider a particular subclass of normal programs that we call simple guess-and-check (SGC) programs. SGC programs consist of guess rules (i.e. rules without positive body atoms) and arbitrary constraints. Many simple combinatorial problems such as graph coloring can be encoded via SGC programs. Moreover, constraint-free SGC programs are known to have a close relation to abstract argumentation frameworks. Our main result shows that for SGC programs the notions of strong and uniform equivalence coincide (in contrast to general normal programs), but do not amount to classical equivalence (as is the case of positive programs). Moreover, we study the characteristics of SE-models for SGC programs; this allows to check whether an arbitrary program (part) can be equivalently formulated within the simpler class of SGC programs. Finally, we briefly discuss our results in relation to other classes of programs.

Assumption-based argumentation (ABA) is a powerful defeasible reasoning formalism which is based on the interplay of assumptions, their contraries, and inference rules. ABA with preferences ( ABA + ) generalizes the basic model by allowing a qualitative comparison of assumptions. The integration of preferences however comes with a cost. In ABA + , the evaluation under two central and well-established semantics—grounded and complete semantics—is not guaranteed to yield an outcome. Moreover, while ABA frameworks without preferences allow for a graph-based representation in Dung-style frameworks, an according instantiation for general ABA + frameworks has not been established so far. In this work, we tackle both issues: First, we develop a novel abstract argumentation formalism based on set-to-set attacks. We show that our so-called Hyper Argumentation Frameworks (HYPAFs) capture the attack relation between assumptions in ABA + . Second, we exploit this correspondence between ABA + and HYPAFs to obtain relaxed variants of complete and grounded semantics for HYPAFs that yield an extension for all frameworks by design, while still faithfully generalizing the established semantics of Dung-style Argumentation Frameworks. Finally, we discuss basic properties and provide a thorough complexity analysis for both the abstract HYPAFs as well as ABA + .

Assumption-based argumentation (ABA) is a powerful defeasible reasoning formalism which is based on the interplay of assumptions, their contraries, and inference rules. ABA with preferences (ABA+) generalizes the basic model by allowing qualitative comparison between assumptions. The integration of preferences however comes with a cost. In ABA+, the evaluation under two central and well-established semantics---grounded and complete semantics---is not guaranteed to yield an outcome. Moreover, while ABA frameworks without preferences allow for a graph-based representation in Dung-style frameworks, an according instantiation for general ABA+ frameworks has not been established so far. In this work, we tackle both issues: First, we develop a novel abstract argumentation formalism based on set-to-set attacks. We show that our so-called Hyper Argumentation Frameworks (HYPAFs) capture ABA+. Second, we propose relaxed variants of complete and grounded semantics for HYPAFs that yield an extension for all frameworks by design, while still faithfully generalizing the established semantics of Dung-style Argumentation Frameworks. We exploit the newly established correspondence between ABA+ and HYPAFs to obtain variants for grounded and complete ABA+ semantics that are guaranteed to yield an outcome. Finally, we discuss basic properties and provide a complexity analysis. Along the way, we settle the computational complexity of several ABA+ semantics.

Already in Dung’s seminal paper introducing Abstract Argumentation Frameworks (AFs), several connections to seemingly unrelated reasoning formalisms have been illustrated. In this work, we continue this trend and establish a connection between abstract argumentation frameworks and boolean networks (BNs). BNs, in a nutshell, mimic simple binary-valued systems, where for each point in time, the value of each bit (component) depends only on the other components’ values of the previous point in time of the network. This formalism is widely used to formally analyze biological processes, where from simple rules complex behavior emerges. We show that stable extensions of an arbitrary AF correspond to single state attractors of its canonically corresponding BN, the complete extensions correspond to a distinctive 2-state attractor, and the admissible sets correspond to the seeds of the BN. We thereby lay the groundwork for a fruitful exchange of ideas between the two research areas.

In this system description we briefly describe the GSAF solver and verifier for SETAFs. The solver is a genuine CDCL-based solver and facilitates the creation of certificates to prove the correctness of negative results if a given instance is deemed to have no extensions. Furthermore, the accompanying verifier can be used to verify such certificates to ensure the correctness thereof.

In this paper, we study the effect of preferences in abstract argumentation under a claim-centric perspective. Recent work has revealed that semantical and computational properties can change when reasoning is performed on claim-level rather than on the argument-level, while under certain natural restrictions (arguments with the same claims have the same outgoing attacks) these properties are conserved. We now investigate these effects when, in addition, preferences have to be taken into account and consider four prominent reductions to handle preferences between arguments. As we shall see, these reductions give rise to four new classes of claim-augmented argumentation frameworks. These classes behave differently from each other with respect to semantic properties and computational complexity, but also in connection with structured argumentation formalisms such as assumption-based argumentation. This strengthens the view that the actual choice for handling preferences has to be taken with care.

Argumentation frameworks (AFs) are a key formalism in AI research. Their semantics have been investigated in terms of principles, which define characteristic properties in order to deliver guidance for analyzing established and developing new semantics. Because of the simple structure of AFs, many desired properties hold almost trivially, at the same time hiding interesting concepts behind syntactic notions. We extend the principle-based approach to argumentation frameworks with collective attacks (SETAFs) and provide a comprehensive overview of common principles for their semantics. Our analysis shows that investigating principles based on decomposing the given SETAF (e.g. directionality or SCC-recursiveness) poses additional challenges in comparison to usual AFs. We introduce the notion of the reduct as well as the modularization principle for SETAFs which will prove beneficial for this kind of investigation. We then demonstrate how our findings can be utilized for incremental computation of extensions and show how we can use graph properties of the frameworks to speed up these algorithms.

In this paper, we study the effect of preferences in abstract argumentation under a claim-centric perspective. Recent work has revealed that semantical and computational properties can change when reasoning is performed on claim-level rather than on the argument-level, while under certain natural restrictions (arguments with the same claims have the same outgoing attacks) these properties are conserved. We now investigate these effects when, in addition, preferences have to be taken into account and consider four prominent reductions to handle preferences between arguments. As we shall see, these reductions give rise to different classes of claim-augmented argumentation frameworks, and behave differently in terms of semantic properties and computational complexity. This strengthens the view that the actual choice for handling preferences has to be taken with care.

Claim-augmented argumentation frameworks (CAFs) provide a formal basis to analyze conclusion-oriented problems in argumentation by adapting a claim-focused perspective; they extend Dung AFs by associating a claim to each argument representing its conclusion. This additional layer offers various possibilities to generalize abstract argumentation semantics, i.e. the re-interpretation of arguments in terms of their claims can be performed at different stages in the evaluation of the framework: One approach is to perform the evaluation entirely at argument-level before interpreting arguments by their claims (inherited semantics); alternatively, one can perform certain steps in the process (e.g., maximization) already in terms of the arguments' claims (claim-level semantics). The inherent difference of these approaches not only potentially results in different outcomes but, as we will show in this paper, is also mirrored in terms of computational complexity. To this end, we provide a comprehensive complexity analysis of the four main reasoning problems with respect to claim-level variants of preferred, naive, stable, semi-stable and stage semantics and complete the complexity results of inherited semantics by providing corresponding results for semi-stable and stage semantics. Furthermore, we provide complexity results for these types of frameworks when restricted to specific graph classes and when parameterized by the number of claims within the framework. Moreover, we show that deciding, whether for a given framework the two approaches of a semantics coincide (concurrence) can be surprisingly hard, ranging up to the third level of the polynomial hierarchy.

Dung's abstract argumentation frameworks (AFs) are a key formalism in AI research nowadays. Claims are an inherent part of each argument; they substantially determine the structure of the abstract representation. Nevertheless, they are often not taken into account on the abstract level, which restricts the modeling capacities of AFs to problems that do not involve claims in the evaluation. In this work, we address this shortcoming and conduct a structural analysis of claim-based argumentation semantics utilizing claim-augmented argumentation frameworks (CAFs) which extend AFs by assigning a claim to each argument. Our main contributions are as follows: We first propose novel variants for preferred, naive, stable, semi-stable, and stage semantics based on claim-defeat and claim-set maximization, complementing existing CAF semantics. Among our findings is that for a certain subclass, namely well-formed CAFs, the different versions of preferred and stable semantics coincide, which is not the case for the other semantics. We then conduct a principle-based analysis of the semantics with respect to general and well-formed CAFs. Finally, we study the expressiveness of the semantics by characterizing their signatures. In summary, this paper provides a thorough analysis of fundamental properties of abstract argumentation semantics (along the lines of existing results for AFs) but from the perspective of the claims the arguments represent. This shift of perspective provides novel results which we deem relevant when abstract argumentation is used in an instantiation-based setting.

Argumentation frameworks (AFs) are a core formalism in the field of formal argumentation. As most standard computational tasks regarding AFs are hard for the first or second level of the Polynomial Hierarchy, a variety of algorithmic approaches to achieve manageable runtimes have been considered in the past. Among them, the backdoor-approach and the treewidth-approach turned out to yield fixed-parameter tractable fragments. However, many applications yield high parameter values for these methods, often rendering them infeasible in practice. We introduce the backdoor-treewidth approach for abstract argumentation, combining the best of both worlds with a guaranteed parameter value that does not exceed the minimum of the backdoor- and treewidth-parameter. In particular, we formally define backdoor-treewidth and establish fixed-parameter tractability for standard reasoning tasks of abstract argumentation. Moreover, we provide systems to find and exploit backdoors of small width, and conduct systematic experiments evaluating the new parameter.

In this paper, we study conditional preferences in abstract argumentation by introducing a new generalization of Dung-style argumentation frameworks (AFs) called Conditional Preference-based AFs (CPAFs). Each subset of arguments in a CPAF can be associated with its own preference relation. This generalizes existing approaches for preference-handling in abstract argumentation, and allows us to reason about conditional preferences in a general way. We conduct a principle-based analysis of CPAFs and compare them to related generalizations of AFs. Specifically, we highlight similarities and differences to Modgil’s Extended AFs and show that our formalism can capture Value-based AFs.

Abstract Argumentation is a key formalism to resolve conflicts in incomplete or inconsistent knowledge bases. Argumentation Frameworks (AFs) and extended versions thereof turned out to be a fruitful approach to reason in a flexible and intuitive setting. The addition of collective attacks, we refer to this class of frameworks as SETAFs, enriches the expressiveness and allows for compacter instantiations from knowledge bases, while maintaining the computational complexity of standard argumentation frameworks. This means, however, that standard reasoning tasks are intractable and worst-case runtimes for known standard algorithms can be exponential. In order to still obtain manageable runtimes, we exploit graph properties of these frameworks. In this paper, we initiate a parameterized complexity analysis of SETAFs in terms of the popular graph parameter treewidth. While treewidth is well studied in the context of AFs with their graph structure, it cannot be directly applied to the (directed) hypergraphs representing SETAFs. We thus introduce two generalizations of treewidth based on different graphs that can be associated with SETAFs, i.e., the primal graph and the incidence graph. We show that while some of these notions allow for parameterized tractability results, reasoning remains intractable for other notions, even if we fix the parameter to a small constant.

In this paper, we give an overview of several recent proposals for non-admissible non-naive semantics for abstract argumentation frameworks. We highlight the similarities and differences between weak admissibility-based approaches and undecidedness-blocking approaches using examples and principles as well as a study of their computational complexity. We introduce a kind of strengthened undecidedness-blocking semantics combining some of the distinctive behaviours of weak admissibility-based semantics with the lower complexity of undecidedness-blocking approaches. We call it loop semantics, because in our new semantics, an argument can only be undecided if it is part of a loop of undecided arguments. Our paper shows how a principle-based approach and a complexity-based approach can be used in tandem to further develop the foundations of formal argumentation.

Abstract dialectical frameworks (ADFs) have been introduced as a formalism for modeling and evaluating argumentation allowing general logical satisfaction conditions. Different criteria used to settle the acceptance of arguments are called semantics. Semantics of ADFs have so far mainly been defined based on the concept of admissibility. Recently, the notion of strong admissibility has been introduced for ADFs. In the current work we study the computational complexity of the following reasoning tasks under strong admissibility semantics. We address 1. the credulous/skeptical decision problem; 2. the verification problem; 3. the strong justification problem; and 4. the problem of finding a smallest witness of strong justification of a queried argument.

We study the computational complexity of abstract argumentation semantics based on weak admissibility, a recently introduced concept to deal with arguments of self-defeating nature. Our results reveal that semantics based on weak admissibility are of much higher complexity (under typical assumptions) compared to all argumentation semantics which have been analysed in terms of complexity so far. In fact, we show PSPACE-completeness of all non-trivial standard decision problems for weak-admissible based semantics. We then investigate potential tractable fragments and show that restricting the frameworks under consideration to certain graph-classes significantly reduces the complexity. We also show that weak-admissibility based extensions can be computed by dividing the given graph into its strongly connected components (SCCs). This technique ensures that the bottleneck when computing extensions is the size of the largest SCC instead of the size of the graph itself and therefore contributes to the search for fixed-parameter tractable implementations for reasoning with weak admissibility.

We study the computational complexity of abstract argumentation semantics based on weak admissibility, a recently introduced concept to deal with arguments of self-defeating nature. Our results reveal that semantics based on weak admissibility are of much higher complexity (under typical assumptions) compared to all argumentation semantics which have been analysed in terms of complexity so far. In fact, we show PSPACE-completeness of all non-trivial standard decision problems for weak-admissible based semantics. We then investigate potential tractable fragments and show that restricting the frameworks under consideration to certain graph-classes significantly reduces the complexity. As a strategy for implementation we also provide a polynomial-time reduction to DATALOG with stratified negation.

Claim-augmented argumentation frameworks (CAFs) provide a formal basis to analyze conclusion-oriented problems in argumentation by adapting a claim-focused perspective; they extend Dung AFs by associating a claim to each argument representing its conclusion. This additional layer offers various possibilities to generalize abstract argumentation semantics as the re-interpretation of arguments in terms of their claims can be performed at different stages in the evaluation of the framework: One approach is to perform the evaluation entirely at argument-level before interpreting arguments by their claims (inherited semantics); alternatively, one can perform certain steps in the process (e.g., maximization) already in terms of the arguments’ claims (claim-level semantics). The inherent difference of these approaches not only potentially results in different outcomes but, as we will show in this paper, is also mirrored in terms of computational complexity. To this end, we provide a comprehensive complexity analysis of the four main reasoning problems with respect to claim-level variants of preferred, naive, stable, semi-stable and stage semantics and complete the complexity results of inherited semantics by providing corresponding results for semi-stable and stage semantics. Moreover, we show that deciding, whether for a given framework the two approaches of a semantics coincide (concurrence) can be surprisingly hard, ranging up to the third level of the polynomial hierarchy.

Argumentation frameworks are a core formalism in the field of formal argumentation, with several semantics being proposed in the literature. Among them, preferred semantics is one of the most popular but comes with relatively high complexity. In fact, deciding whether an argument is skeptically accepted, i.e. contained in each preferred extension, is Pi^P_2-complete. In this work we study the complexity of this problem w.r.t. the length of the cycles in the considered AF. Our results show which bounds are necessary to decrease the complexity to coNP and P, respectively. We also consider argumentation frameworks with collective attacks and achieve Pi^P_2-hardness already for cycles of length 4.

We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with n vertices and m edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires O(n2) symbolic operations and O(1) symbolic space. The only other symbolic algorithm for the MEC decomposition requires O(n√m ) symbolic operations and O(√m ) symbolic space. The main open question has been whether the worst-case O(n2) bound for symbolic operations can be beaten for MEC decomposition computation. In this work, we answer the open question in the affirmative. We present a symbolic algorithm that requires ~O( n1.5) symbolic operations and ~O( √n ) symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and esymbolic space: for all 02 - ∈) symbolic operations and ~O( n∈) symbolic space (~O(·) hides poly-logarithmic factors).Using our techniques we also present faster algorithms for computing the almost-sure winning regions of ω-regular objectives for MDPs. We consider the canonical parity objectives for ω-regular objectives, and for parity objectives with d-priorities we present an algorithm that computes the almost-sure winning region with ~O( n2 - ∈) symbolic operations and ~O( n∈) symbolic space, for all 02· d) symbolic operations and O(log n) symbolic space; or (b) O(n√m ·d) symbolic operations and ~O( √m ) symbolic space. Thus we improve the time-space product from ~O( n2·d ) to ~O( n2).

We consider planning problems for graphs, Markov Decision Processes (MDPs), and games on graphs in an explicit state space. While graphs represent the most basic planning model, MDPs represent interaction with nature and games on graphs represent interaction with an adversarial environment. We consider two planning problems with k different target sets: (a) the coverage problem asks whether there is a plan for each individual target set; and (b) the sequential target reachability problem asks whether the targets can be reached in a given sequence. For the coverage problem, we present a linear-time algorithm for graphs, and quadratic conditional lower bound for MDPs and games on graphs. For the sequential target problem, we present a linear-time algorithm for graphs, a sub-quadratic algorithm for MDPs, and a quadratic conditional lower bound for games on graphs. Our results with conditional lower bounds, based on the boolean matrix multiplication (BMM) conjecture and strong exponential time hypothesis (SETH), establish (i) model-separation results showing that for the coverage problem MDPs and games on graphs are harder than graphs, and for the sequential reachability problem games on graphs are harder than MDPs and graphs; and (ii) problem-separation results showing that for MDPs the coverage problem is harder than the sequential target problem.

The paper provides an initial study on how ranking semantics in argumentation have to be handled when leaving the purely abstract setting. We employ claim-augmented frameworks where each argument is associated to a claim it stands for. We propose liftings from argument- to claim-level in two veins: for desired properties and for actual rankings. Our main contribution is to investigate whether the satisfaction of properties by argument-based ranking semantics carries over to the lifted, claim-based, variants of the corresponding properties and semantics.

In this work we revisit computational aspects of strongly admissible semantics in Dung's abstract argumentation frameworks. First, we complement the existing complexity analysis by focusing on the problem of computing strongly admissible sets of minimum size that contain a given argument and providing NP-hardness as well as hardness of approximation results. Based on these results, we then investigate two approaches to compute (minimum-sized) strongly admissible sets based on Answer Set Programming (ASP) and Integer Linear Programming (ILP), and provide an experimental comparison of their performance.

Generalizing the attack structure in argumentation frameworks (AFs) has been studied in different ways. Most prominently, the binary attack relation of Dung frameworks has been extended to the notion of collective attacks. The resulting formalism is often termed SETAFs. Another approach is provided via abstract dialectical frameworks (ADFs), where acceptance conditions specify the relation between arguments; restricting these conditions naturally allows for so-called support-free ADFs. The aim of the paper is to shed light on the relation between these two different approaches. To this end, we investigate and compare the expressiveness of SETAFs and support-free ADFs under the lens of 3-valued semantics. Our results show that it is only the presence of unsatisfiable acceptance conditions in support-free ADFs that discriminate the two approaches.

Dung's abstract argumentation frameworks (AFs) are a popular conceptual tool to define semantics for advanced argumentation formalisms. Hereby, arguments representing a possible inference of a claim are constructed and an attack relation between arguments indicates certain conflicts between the claim of one argument and the inference of another. Based on this abstract model, sets of jointly acceptable arguments are then gathered and finally interpreted in terms of their claims. Argumentation formalisms following this type of instantiating Dung AFs naturally produce several arguments with the same claim. This causes several issues and challenges for argumentation systems: on the one hand, the relation between claims remains implicit and, on the other hand, determining the acceptance of claims requires additional computations on top of argument acceptance. An instantiation that avoids this situation could provide additional insights and advantages, thus complementing the standard instantiation process via Dung AFs. Consequently, the research question we tackle is as follows: Can one combine different arguments sharing the same claim to a single abstract argument without affecting the overall results (and which abstract formalisms can serve such a purpose)? As a main result we show that a certain class of frameworks, where arguments with the same claim have the same outgoing attacks, can be equivalently (for all standard semantics) represented as argumentation frameworks with collective attacks where each claim occurs in exactly one argument. We further identify a class of frameworks where one even obtains an equivalent Dung AF with just one argument per claim.

Claim-augmented argumentation frameworks (CAFs) constitute a generic formalism for conflict resolution of conclusion-oriented problems in argumentation. CAFs extend Dung argumentation frameworks (AFs) by assigning a claim to each argument. So far, semantics for CAFs are defined with respect to the underlying AF by interpreting the extensions of the respective AF semantics in terms of the claims of the accepted arguments; we refer to them as inherited semantics of CAFs. A central concept of many argumentation semantics is maximization, which can be done with respect to arguments as in preferred semantics, or with respect to the range as in semi-stable semantics. However, common instantiations of argumentation frameworks require maximality on the claim-level and inherited semantics often fail to provide maximal claim-sets even if the underlying AF semantics yields maximal argument sets. To address this issue, we investigate a different approach and introduce claim-level semantics (cl-semantics) for CAFs where maximization is performed on the claim-level. We compare these two approaches for five prominent semantics (preferred, naive, stable, semi-stable, and stage) and relate in total eleven CAF semantics to each other. Moreover, we show that for a certain subclass of CAFs, namely well-formed CAFs, the different versions of preferred and stable semantics coincide, which is not the case for the remaining semantics. We furthermore investigate a recently established translation between well-formed CAFs and SETAFs and show that, in contrast to the inherited naive, semi-stable and stage semantics, the cl-semantics correspond to the respective SETAF semantics. Finally, we investigate the expressiveness of the considered semantics in terms of their signatures.

Abstract Argumentation frameworks with collective attacks are a prominent extension of Dung’s abstract argumentation frameworks, where an attack can be drawn from a set of arguments to another argument. These frameworks are often abbreviated as SETAFs. Although SETAFs have received increasing interest recently, a thorough study on the actual behaviour of collective attacks has not been carried out yet. In particular, the richer attack structure SETAFs provide can lead to different forms of redundant attacks, i.e. attacks that are subsumed by attacks involving less arguments. Also the notion of strong equivalence, which is fundamental in nonmonotonic formalisms to characterize equivalent replacements, has not been investigated for SETAFs so far. In this paper, we first provide a classification of different types of collective attacks and analyse for which semantics they can be proven redundant. We do so for eleven well-established abstract argumentation semantics. We then study how strong equivalence between SETAFs can be decided with respect to the considered semantics and also consider variants of strong equivalence. Our results show that removing redundant attacks in a suitable way provides direct means to characterize strong equivalence by syntactical equivalence of so-called kernels, thus generalizing well-known results on strong equivalence between Dung AFs.

Abstract argumentation frameworks have been introduced by Dung as part of an argumentation process, where arguments and conflicts are derived from a given knowledge base. It is solely this relation between arguments that is then used in order to identify acceptable sets of arguments. A final step concerns the acceptance status of particular statements by reviewing the actual contents of the acceptable arguments. Complexity analysis of abstract argumentation so far has neglected this final step and is concerned with argument names instead of their contents, i.e. their claims. As we outline in this paper, this is not only a slight deviation but can lead to different complexity results. We, therefore, give a comprehensive complexity analysis of abstract argumentation under a claim-centric view and analyse the four main decision problems under seven popular semantics. In addition, we also address the complexity of common sub-classes and introduce novel parameterisations – which exploit the nature of claims explicitly – along with fixed-parameter tractability results.

The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes (MDPs). A basic specification formalism in the verification of reactive systems is the strong fairness (aka Streett) objective, where given different types of requests and corresponding grants, the requirement is that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All omega-regular objectives can be expressed as Streett objectives and hence they are canonical in verification. Consider graphs/MDPs with n vertices, m edges, and a Streett objectives with k pairs, and let b denote the size of the description of the Streett objective for the sets of requests and grants. The current best-known algorithm for the problem requires time $O(min(n^2, m \sqrt{m \log n}) + b \log n)$. In this work, we present randomized near-linear time algorithms, with expected running time $\widetilde{O}(m + b)$, where the $\widetilde{O}$ notation hides poly-log factors. Our randomized algorithms are near-linear in the size of the input, and hence optimal up to poly-log factors.

In this paper, we consider SETAFs due to Nielsen and Parsons, an extension of Dung's abstract argumentation frameworks that allow for collective attacks. We first provide a comprehensive analysis of the expressiveness of SETAFs under conflict-free, naive, stable, complete, admissible and preferred semantics. Our analysis shows that SETAFs are strictly more expressive than Dung AFs. Towards a uniform characterization of SETAFs and Dung AFs we provide general results on expressiveness which take the maximum degree of the collective attacks into account. Our results show that, for each k>0, SETAFs that allow for collective attacks of k+1 arguments are more expressive than SETAFs that only allow for collective attacks of at most k arguments.

Solving parity games, which are equivalent to modal μ-calculus model checking, is a central algorithmic problem in formal methods, with applications in reactive synthesis, program repair, verification of branching-time properties, etc. Besides the standard compu- tation model with the explicit representation of games, another important theoretical model of computation is that of set-based symbolic algorithms. Set-based symbolic algorithms use basic set operations and one-step predecessor operations on the implicit description of games, rather than the explicit representation. The significance of symbolic algorithms is that they provide scalable algorithms for large finite-state systems, as well as for infinite-state systems with finite quotient. Consider parity games on graphs with n vertices and parity conditions with d priorities. While there is a rich literature of explicit algorithms for parity games, the main results for set-based symbolic algorithms are as follows: (a) the basic algorithm that requires O(nd) symbolic operations and O(d) symbolic space; and (b) an improved algorithm that requires O(nd/3+1) symbolic operations and O(n) symbolic space. In this work, our contributions are as follows: (1) We present a black-box set-based symbolic algorithm based on the explicit progress measure algorithm. Two important consequences of our algorithm are as follows: (a) a set-based symbolic algorithm for parity games that requires quasi-polynomially many symbolic operations and O(n) symbolic space; and (b) any future improvement in progress measure based explicit algorithms immediately imply an efficiency improvement in our set-based symbolic algorithm for parity games. (2) We present a set-based symbolic algorithm that requires quasi-polynomially many symbolic operations and O(d · log n) symbolic space. Moreover, for the important special case of d ≤ log n, our algorithm requires only polynomially many symbolic operations and poly-logarithmic symbolic space.

A model of computation that is widely used in the formal analysis of reactive systems is symbolic algorithms. In this model the access to the input graph is restricted to consist of symbolic operations, which are expensive in comparison to the standard RAM operations. We give lower bounds on the number of symbolic operations for basic graph problems such as the computation of the strongly connected components and of the approximate diameter as well as for fundamental problems in model checking such as safety, liveness, and coliveness. Our lower bounds are linear in the number of vertices of the graph, even for constant-diameter graphs. For none of these problems lower bounds on the number of symbolic operations were known before. The lower bounds show an interesting separation of these problems from the reachability problem, which can be solved with O(D) symbolic operations, where D is the diameter of the graph. Additionally we present an approximation algorithm for the graph diameter which requires symbolic steps to achieve a (1 + ∊)-approximation for any constant ∊ > 0. This compares to O(n · D) symbolic steps for the (naive) exact algorithm and O(D) symbolic steps for a 2-approximation. Finally we also give a refined analysis of the strongly connected components algorithms of [15], showing that it uses an optimal number of symbolic steps that is proportional to the sum of the diameters of the strongly connected components.

Graph games with ω-regular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify ω-regular winning conditions. Graph games with parity conditions are equivalent to μ-calculus model checking, and thus a very important algorithmic problem. Symbolic algorithms are of great significance because they provide scalable algorithms for the analysis of large finite-state systems, as well as algorithms for the analysis of infinite-state systems with finite quotient. A set-based symbolic algorithm uses the basic set operations and the one-step predecessor operators. We consider graph games with $n$ vertices and parity conditions with $c$ priorities. While many explicit algorithms exist for graph games with parity conditions, for set-based symbolic algorithms there are only two algorithms (notice that we use space to refer to the number of sets stored by a symbolic algorithm): (a) the basic algorithm that requires $O(n^c)$ symbolic operations and linear space; and (b) an improved algorithm that requires $O(n^{c/2+1})$ symbolic operations but also $O(n^{c/2+1})$ space (i.e., exponential space). In this work we present two set-based symbolic algorithms for parity games: (a) our first algorithm requires $O(n^{c/2+1})$ symbolic operations and only requires linear space; and (b) developing on our first algorithm, we present an algorithm that requires $O(n^{c/3+1})$ symbolic operations and only linear space. We also present the first linear space set-based symbolic algorithm for parity games that requires at most a sub-exponential number of symbolic operations.

We introduce a parametrized equivalence notion for abstract argumentation that subsumes standard and strong equivalence as corner cases. Under this notion, two argumentation frameworks are equivalent if they deliver the same extensions under any addition of arguments and attacks that do not affect a given set of core arguments. As we will see, this notion of equivalence nicely captures the concept of local simplifications. We provide exact characterizations and complexity results for deciding our new notion of equivalence.

Understanding the expressiveness of a formalism is undoubtedly an important part of understanding its possibilities and limitations. Translations between different formalisms have proven to be valuable tools for understanding this very expressiveness. In this work, we complement recent investigations of the intertranslatability of argumentation semantics for Dung's abstract argumentation frameworks. As our focus is on the expressiveness of argumentation semantics, we are not only interested in efficiently computable translations but also consider translations that might not (always) be efficiently computable. This allows us to provide translations between certain semantics, where under established complexity assumptions no efficiently computable translation exists. However, for some semantics we give strong translational impossibility results stating that even with arbitrary computational power we cannot in all situations translate one to the other. Finally, this allows us to draw a hierarchy for the expressiveness of argumentation semantics.

Online social networks allow the collection of large amounts of data about the influence between users connected by a friendship-like relationship. When distributing items among agents forming a social network, this information allows us to exploit network externalities that each agent receives from his neighbors that get the same item. In this paper we consider Friends-of-Friends (2-hop) network externalities, i.e., externalities that not only depend on the neighbors that get the same item but also on neighbors of neighbors. For these externalities we study a setting where multiple different items are assigned to unit-demand agents. Specifically, we study the problem of welfare maximization under different types of externality functions. Let n be the number of agents and m be the number of items. Our contributions are the following: (1) We show that welfare maximization is APX-hard; we show that even for step functions with 2-hop (and also with 1-hop) externalities it is NP-hard to approximate social welfare better than (1−1/e). (2) On the positive side we present (i) an $O(\sqrt n)$ -approximation algorithm for general concave externality functions, (ii) an O(log m)-approximation algorithm for linear externality functions, and (iii) a $\frac {5}{18}(1-1/e)$ -approximation algorithm for 2-hop step function externalities. We also improve the result from [7] for 1-hop step function externalities by giving a $\frac {1}{2}(1-1/e)$ -approximation algorithm.

Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental ω-regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical ω-regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives.

Games on graphs provide the appropriate framework to study several central problems in computer science, such as verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized Büchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized Büchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification. We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider graph games with n vertices, m edges, and generalized Büchi objectives with k conjunctions. First, we present an algorithm with running time O(k*n^2), improving the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm is optimal for dense graphs under (A1). Second, we show that the basic algorithm for the problem is optimal for sparse graphs when the target sets have constant size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1 k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time algorithm for m > n^{1.5}.

In abstract argumentation theory, preferred semantics has become one of the most popular approaches for determining the sets of arguments that can collectively be accepted. However, the description of preferred semantics, as it was originally stated by Dung, has a mainly technical and mathematical nature, making it difficult for lay persons to understand what the concept of preferred semantics is essentially about. In the current article, we aim to bridge the gap between mathematics and philosophy by providing a reformulation of (credulous) preferred semantics in terms of Socratic discussion. In order to do so, we first provide a (semi-)formal treatment of some of the concepts in Socratic dialogue.

Recently, stage and cf 2 semantics for abstract argumentation attracted specific attention. By distancing from the notion of defence, they are capable to select arguments out of odd-length cycles. In case of cf 2 semantics, the SCC-recursive schema guarantees that important evaluation criteria for argumentation semantics, like directionality, weak- and CF -reinstatement, are fulfilled. Beside several desirable properties, both stage and cf 2 semantics still have some drawbacks. The stage semantics does not satisfy the above mentioned evaluation criteria, whereas cf 2 semantics produces some questionable results on frameworks with cycles of length ≥ 6. Therefore, we suggest to combine stage semantics with the SCC-recursive schema of cf 2 semantics. The resulting stage 2 semantics overcomes the problems regarding cf 2 and stage semantics. We study properties of stage 2 semantics and its relations to existing semantics, show that it fulfills the mentioned evaluation criteria, study strong equivalence for stage 2 semantics and provide a comprehensive complexity analysis of the associated reasoning problems. Besides the analysis of stage 2 semantics, we also complement existing complexity results for cf 2 by an analysis of tractable fragments and fixed parameter tractability. Furthermore, we provide answer-set programming (ASP) encodings for stage 2 semantics and labelling-based algorithms for cf 2 and stage 2 semantics.

Online social networks allow the collection of large amounts of data about the influence between users connected by a friendship-like relationship. When distributing items among agents forming a social network, this information allows us to exploit network externalities that each agent receives from his neighbors that get the same item. In this paper we consider Friends-of-Friends (2-hop) network externalities, i.e., externalities that not only depend on the neighbors that get the same item but also on neighbors of neighbors. For these externalities we study a setting where multiple different items are assigned to unit-demand agents. Specifically, we study the problem of welfare maximization under different types of externality functions. Let n be the number of agents and m be the number of items. Our contributions are the following: (1) We show that welfare maximization is APX-hard; we show that even for step functions with 2-hop (and also with 1-hop) externalities it is NP-hard to approximate social welfare better than (1-1/e). (2) On the positive side we present (i) an O(sqrt n)-approximation algorithm for general concave externality functions, (ii) an O(\log m)-approximation algorithm for linear externality functions, and (iii) an (1-1/e)\frac{1}{6}-approximation algorithm for 2-hop step function externalities. We also improve the result from [6] for 1-hop step function externalities by giving a (1-1/e)/2-approximation algorithm.

Within the last decade, abstract argumentation has emerged as a central field in Artificial Intelligence. Besides providing a core formalism for many advanced argumentation systems, abstract argumentation has also served to capture several non-monotonic logics and other AI related principles. Although the idea of abstract argumentation is appealingly simple, several reasoning problems in this formalism exhibit high computational complexity. This calls for advanced techniques when it comes to implementation issues, a challenge which has been recently faced from different angles. In this survey, we give an overview on different methods for solving reasoning problems in abstract argumentation and compare their particular features. Moreover, we highlight available state-of-the-art systems for abstract argumentation, which put these methods to practice.

The resolution-based grounded semantics constitutes one of the most interesting approaches for the evaluation of abstract argumentation frameworks. This particular semantics satisfies a large number of desired properties, among them all properties proposed by Baroni and Giacomin. In recent years, the analysis of argumentation semantics has been extended by further topics, among them characterizations for equivalence notions, intertranslatability issues, and expressibility in terms of signatures (all possible sets of extensions a semantics is capable to express). In this line of research, resolution-based grounded semantics has been neglected so far. We close this gap here, compare the expressibility of resolution-based grounded semantics with other prominent semantics, provide a characterization for strong equivalence and complement existing complexity results.

Abstract argumentation frameworks (AFs) are one of the most studied formalisms in AI. In this work, we introduce a certain subclass of AFs which we call compact. Given an extension-based semantics, the corresponding compact AFs are characterized by the feature that each argument of the AF occurs in at least one extension. This not only guarantees a certain notion of fairness; compact AFs are thus also minimal in the sense that no argument can be removed without changing the outcome. We address the following questions in the paper: (1) How are the classes of compact AFs related for different semantics? (2) Under which circumstances can AFs be transformed into equivalent compact ones? (3) Finally, we show that compact AFs are indeed a non-trivial subclass, since the verification problem remains coNP-hard for certain semantics.

Most reasoning tasks in abstract argumentation are in general computationally hard. One approach of dealing with such problems stems from the field of parameterized complexity theory. For so-called fixed-parameter tractable algorithms, one identifies problem parameters, e.g. the graph parameter tree width, such that the run-time of algorithms heavily scales with the parameter but only polynomially with the input size. The dynPARTIX system turns these fixed-parameter tractability results into practice by implementing dynamic programming algorithms for the graph parameter tree width.

We consider two instantiations of the SCC-recursive schema for argumentation semantics, cf2, using maximal conflict-free sets as base semantics, and stage2, using stage extensions as base semantics. Both of them have been shown to be in general of high complexity. We provide a detailed analysis of possible tractable fragments for these semantics. Moreover we present a labeling based algorithm for computing cf2 extension, which is complexity-sensitive w.r.t. one of the tractable fragments.

In this work we complement recent investigations of the intertranslatability of argumentation semantics. Our focus is on the expressiveness of argumentation semantics and thus we expand the area of interest beyond efficiently computable translations. To this end we provide new translations between semantics as well as new translational impossibility results. This allows us to draw a hierarchy for the expressiveness of argumentation semantics.

The concept of “ideal semantics” has been promoted as an alternative basis for skeptical reasoning within abstract argumentation settings. Informally, ideal acceptance not only requires an argument to be skeptically accepted in the traditional sense but further insists that the argument is in an admissible set all of whose arguments are also skeptically accepted. The original proposal was couched in terms of the so-called preferred semantics for abstract argumentation. We argue, in this paper, that the notion of “ideal acceptability” is applicable to arbitrary semantics and justify this claim by showing that standard properties of classical ideal semantics, e.g. unique status, continue to hold in any “reasonable” extension-based semantics. We categorise the relationship between the divers concepts of “ideal extension wrt semantics σ” that arise and we present a comprehensive analysis of algorithmic and complexity-theoretic issues.

Translations between different nonmonotonic formalisms always have been an important topic in the field, in particular to understand the knowledge-representation capabilities those formalisms offer. We provide such an investigation in terms of different semantics proposed for abstract argumentation frameworks, a nonmonotonic yet simple formalism which received increasing interest within the last decade. Although the properties of these different semantics are nowadays well understood, there are no explicit results about intertranslatability. We provide such translations wrt. different properties and also give a few novel complexity results which underlie some negative results.

Most computational problems in the area of abstract argumentation are intractable, thus identifying tractable fragments and developing efficient algorithms for such fragments are important objectives towards practically efficient argumentation systems. One approach to tractability is to view abstract argumentation frameworks (AFs) as directed graphs and bound certain graph parameters. In particular, Dunne showed that many problems can be solved in linear time for AFs of bounded treewidth. In this paper we consider the graph-parameter clique-width, which is more general than treewidth. An additional advantage of clique-width over treewidth is that it applies well to directed graphs and takes the orientation of edges into account. We first give theoretical tractability results for AFs of bounded clique-width and then introduce dynamic-programming algorithms for credulous and skeptical reasoning.

Alternation is a common tool in complexity theory, where it has been used to prove various complexity classifications. In this work, we show that it can also be used to enhance the expressive power of the imperative part of a programming language. In particular, we present Alter-Java -- an extension of Java by language constructs to express alternation, i.e., a sequence of "there exists" and "for all" statements. Moreover, we show that many practical problems have a very natural and succinct description in terms of alternation. In order to guarantee an efficient execution of such programs, we have introduced several optimizations. We also report on experiments with our implementation of Alter-Java. The results thus obtained illustrate that our alternation framework leads to competitive running times while the code to be written is significantly shorter than without this new language feature.