Behaviour specifications of heterogeneously structured interacting system components in a distributed software architecture are coalgebras based on different endofunctors, whose interaction scenarios must be algebraically specified. We propose to formalise the concrete interaction rules as natural transformations, called coordination laws, and embed these specifications into a bialgebraic representation based on multi-sorted algebraic signatures. If the coordination laws can be transformed into an abstract GSOS format, the approach is compositional, i.e. syntactical operations on the individual components are fully abstract w.r.t. bisimilarity. We obtain resulting operational semantics as a holistic coalgebra, which comprises the behaviour of the individual components and the resulting global behaviour. This guarantees non-intrusiveness for the individual components and, furthermore, enables successive coordination steps building on each other by taking the individual components as initial input and yielding an ultimate compound behaviour as final output.
The recent development of quantum communication protocols calls for adequate modelling and verification techniques, which requires abstracting and focusing on the basic features of quantum concurrent systems, like process algebras have done for their classical counterparts. However, recovering the peculiar observational limitations prescribed by quantum theory has proven to be a challenging task in quantum systems expressing communication and non-determinism. The problem has been found to be in the interaction between quantum and non-determinism. We address it by resorting to schedulers, and we give behavioural equivalences for both branching and linear-time semantics that adheres to the prescriptions of quantum theory. Moreover, we show that the aforementioned difficulties occur also in simple systems that do not allow exchanging qubits via quantum channels.
Approaching reconfigurable systems as structured transition systems, where the states are models in a given institution, is a methodological approach pursued in [17]. The versatility of this approach lies in the assumption that the logic used for configurations can be chosen based on the nature of the system configurations to be developed. Technically, this is supported by using parametric methods to build modal logics on-demand (e.g. [12, 18]). In this paper, we go a step further by assuming that configurations can be governed by different logics, even within the same reconfigurable system. We operationalize this principle for the formal specification of systems by enriching and reshaping the formalism many-logics modal logic [10] within the theory of institutions and by introducing a number of relations between models that preserve logical properties.
We survey one branch of algebraic logic, namely modal semirings. They provide compact algebraic definitions of actions, with choice + and sequential composition · , together with modal operators box and diamond, parametrised by actions, that allow reasoning about successors and predecessors of states/worlds. Particular instances are homogeneous binary relations or sets of finite and infinite non-empty traces under fusing concatenation. As main examples of applications we present obstacle analysis for geographic wayfinders, Hoare Logic, O’Hearn’s Incorrectness Logic, General Correctness Logic, as well as the temporal logic ^* and its sublogics and . We also give glimpses at Epistemic Logics of belief and knowledge, pointer structures plus Separation Logic and preference database queries. Finally, we briefly discuss some related algebraic approaches.
Formal learning theory poses the question of how agents should use observations about their environment to arrive at accurate and true conclusions. To answer this question, empirical and formal inquiries have been provided with topological models in Domain Theory [1,16], Formal Learning Theory [3], Epistemology and Philosophy of Science [2,7,15]. The goal of our work is to present the initial steps of how precisely the topological formalization of empirical inquiry may be expressed in terms of abstract model theory. In this framework, following Genin and Kelly [5,6], we define what is a method, as well as verifiability, refutability, decidability and limiting verifiability of a proposition. Furthermore, we define what is an abstract empirical problem, and its solvability. We prove that verifiability, refutability, decidability, and limiting verifiability of a proposition and solvability of a problem are invariant under change of notation.
We introduce approximations to arithmetical data types called arithmetics by proxy or proxy arithmetics. Focusing on the common meadow of rational numbers, we examine the effect of imposing bounds on the numbers and finiteness on algebras that approximate the rationals. Starting with an established set of equations for common meadows, we explore sets of equational axioms for these approximating algebras. Then we give a new general algebraic construction that may serve as a way of making proxies for arbitrary data types. We apply the construction to the arithmetical case. Finally, we return to the sets of equations using notions of equality that are different from standard first order equality.
Adversarial risk analysis (ARA) provides decision-theoretic arguments to manage uncertainty in competitive decision-making environments. This paper introduces efficient algorithmic approaches to approximate ARA solutions in multi-stage games, covering both sequential and simultaneous settings, through augmented probability simulation. Two examples concerning international piracy and air combat illustrate the proposed methodology.
To make a choice in the presence of multiple criteria, we generally use an aggregation function which determines, for each alternative, the balance of its strengths and weaknesses and its overall evaluation. The aggregation function uses weights to adapt the model to the decision-maker's value system, by specifying the importance of the criteria and possibly their interactions. In this paper, we propose a noise-tolerant active learning method for these parameters, which not only effectively reduces the indeterminacy of the weights to identify an optimal or near-optimal decision among a given set of alternatives, but also simultaneously determines a predictive model of preferences capable of making relevant choices for the decision-maker on new instances. These outcomes are achieved by leveraging a general disagreement-based active learning approach that is theoretically guaranteed to be tolerant to noisy answers. The proposed method applies to various weighted aggregation functions, linear or not, classically used in decision theory.
Conditional preference networks (CP-nets) have received significant attention for modeling preferences over combinations of features. However, dominance testing, the problem of inferring from a CP-net whether one outcome is always preferred over another, is NP-hard, requiring exponential time in practice. In this paper, we introduce the use of independent relaxed subproblems as a heuristic for faster inference from CP-nets. We show how to relax the constraints in the conditional preference tables and partition the network, yielding smaller subproblems that can be solved easily. The lengths of these solutions can then be added together to provide a heuristic for informed search algorithms such as A* and applied to dominance testing in CP-nets. We prove that the resulting additive heuristic function is admissible and consistent, guaranteeing optimality and completeness. We show from experiments on randomly generated binary and multivalued CP-nets that our method performs better than the state of the art, and can further be combined with other pruning techniques, resulting in greatly improved performance for dominance testing.
Electoral control is a scenario where an election chair changes the structure of an election by actions such as adding or deleting either candidates or voters with the goal of either making a favorite candidate win or precluding a despised candidate's victory. Much work has been done on the computational complexity of controlling elections for single-winner voting rules, yet much less work on the control complexity for multiwinner voting rules which aim at electing not only a single winner but a winning committee of candidates. Meir et al. [20] initiated the investigation of electoral control for multiwinner voting rules, including single nontransferable vote (SNTV) and bloc voting. We study these two rules with respect to control by adding, deleting, or replacing candidates.
The global transition from manned to automated vehicles is anticipated to occur incrementally. As such, interactions between automated driving systems (ADS) and manned vehicles motivate related decision-support research. This manuscript develops a novel modeling framework based on adversarial risk analysis focusing on lane-changing maneuvers. An empirical evaluation is provided within a simulated environment serving to validate the modeling approach and solution methodology under a specified traffic scene. Additional model extensions to alternative traffic scenes and different driver-rationality assumptions are provided. In so doing, we showcase the potential for decision theory to manage ADS behavior in heterogeneous traffic. This research also highlights the need for an ADS to prudently balance computational resources between perception and decision tasks.
In Subset Sum Game as studied by Pieterse and Woeginger [Theory of Computing Systems, 2021], two players alternatingly fill a common knapsack each with items from a private collection. The goal of Player A is to reach a value of at least T_ , whereas Player B may follow different strategies. Subset Sum Game is NP-complete and solvable in pseudopolynomial time if Player B greedily selects the biggest available item in each turn; the game is PSPACE-complete, however, if Player B plays a hostile strategy where the only aim is to avoid that Player A wins. We continue the study of the game with these two strategies for Player B. First, we provide a faster pseudopolynomial-time algorithm for a greedy Player B and show that the problem with a hostile Player B is fixed-parameter tractable with respect to the knapsack capacity C. Moreover, we study the influence of further parameters such as T_ , the number of rounds in the game, and the number of different numbers in the input on the complexity of the problem. Second, we consider a further variant of the game, called Protective Subset Sum Game, where Player A additionally has the goal that Player B reaches a value of at least T_ . In a nutshell, we show that most algorithms for the nonprotective variant can be transferred to Protective Subset Sum Game.
The mathematical models of many real-world decision-making problems contain two levels of optimization. In these models, one of the optimization problems appears as a constraint of the other one, called follower and leader, respectively. These problems are known as bilevel optimization problems (BOPs) in mathematical programming and are widely studied by both classical and evolutionary optimization communities. The nested nature of these problems causes many difficulties such as non-convexity and disconnectedness for traditional methods, and requires a huge number of function evaluations for evolutionary algorithms. This paper proposes a fully Bayesian optimization approach, called FB-BLO. We aim to reduce the necessary function evaluations for both upper and lower level problems by iteratively approximating promising solutions with Gaussian process surrogate models at both levels. The proposed FB-BLO algorithm uses the other decision-makers' observations in its Gaussian process model to leverage the correlation between decisions and objective values. This allows us to extract knowledge from previous decisions for each level. The algorithm has been evaluated on numerous benchmark problems and compared with existing state-of-the-art algorithms. Our evaluation demonstrates the success of our proposed FB-BLO algorithm in terms of both effectiveness and efficiency.
Additive preference representation is standard in Multiple Criteria Decision Analysis, and learning such a preference model dates back from the UTA method [11]. In this seminal work, an additive piece-wise linear model is inferred from a learning set composed of pairwise comparisons. In this setting, the learning set is provided by a single Decision-Maker (DM), and an additive model is inferred to match the learning set. We extend this framework to the case where (i) multiple DMs with heterogeneous preferences provide part of the learning set, and (ii) the learning set is provided as a whole without knowing which DM expressed each pairwise comparison. Hence, the problem amounts to inferring a preference model for each DM and simultaneously "discovering" the segmentation of the learning set. In this paper, we show that this problem is computationally difficult. We propose a mathematical programming based resolution approach to solve this Preference Learning and Segmentation problem (PLS). We also propose a heuristic to deal with large datasets. We study the performance of both algorithms through experiments using synthetic and real data.
We consider the complexity of finding envy-free allocations for the class of graphical valuations. Graphical valuations were introduced by Christodoulou et al. [14] as a structured class of valuations that admit allocations that are envy-free up to any item(EFX). These are valuations where every item is valued by two agents, lending a (simple) graph structure to the utilities, where the agents are vertices and are adjacent if and only if they value a (unique) common item. Finding envy-free allocations for general valuations is known to be computationally intractable even for very special cases: in particular, even for binary valuations, and even for identical valuations with two agents. We show that, for binary graphical valuations, the existence of envy-free allocations can be determined in polynomial time. In contrast, we also show that allowing for even slightly more general utilities {0,1,d} leads to intractability even for graphical valuations. This motivates other approaches to tractability, and to that end, we exhibit the fixed-parameter tractability of the problem parameterized by the vertex cover number of the graph when the number of distinct utilities is bounded. We also show that, all graphical instances that admit EF allocations also admit one that is non-wasteful. Since EFX allocations are possibly wasteful, we also address the question of determining the price of fairness of EFX allocations. We show that the price of EFX with respect to utilitarian welfare is one for binary utilities, but can be arbitrarily large {0, 1, d} valuations. We also show the hardness of deciding the existence of an EFX allocation which is also welfare-maximizing and of finding a welfare-maximizing allocation within the set of EFX allocations.
Compiling the votes of a subelectorate is a well-known problem in computational social choice. The goal is to store the information contained in the votes cast by a subelectorate in a space-efficient way, such that when the rest of the votes become available, the winners can be accurately ascertained. This problem has been studied for single-winner voting rules. We provide a comprehensive compilation complexity landscape for several ordinal and approval-based multi-winner voting rules.
The problem of k -tiered coalition formation games ( k -TCFGs) has been considered for ranking members of a stochastic, intransitive round robin tournament, with the restriction that the ordering must have exactly k nonempty ranks for some integer k . As with other coalition formation games, an outcome of a k -TCFG may be evaluated for its stability, using the notions of Nash stability or core stability. An outcome is Nash stable if no one agent can move to a more preferable position, either by forming its own coalition or joining an existing one. An outcome is core stable if no set of agents can form a new coalition such that all agents in the set benefit. Previous research on k -TCFGs has focused on preferences derived from matchups, and has indicated that, under these matchup-oriented preferences, core stable outcomes may be significantly easier to find than Nash stable outcomes. However, the extent of this trend has not been explored. Here, we prove that for a key subset of k -TCFGs with matchup-oriented preferences, there is always at least one core stable partition. We include an illustration of the difference between Nash stabilizability and core stabilizability on an example game. We introduce a preference notation that can be used to represent any preference framework for k -TCFGs, and prove that under the subset of k -TCFGs which this notation can represent within polynomial space, the problem of determining if a game has a Nash stable list is NP-complete.
A tournament on n agents is a complete oriented graph with the agents as vertices and edges that describe the win-loss outcomes of the ( [ n; 2 ]) matches played between each pair of agents. The winner of a tournament is determined by a tournament rule that maps tournaments to probability distributions over the agents. We want these rules to be fair (choose a high-quality agent) and robust to strategic manipulation. Prior work has shown that under minimally fair rules, manipulations between two agents can be prevented when utility is nontransferable but not when utility is completely transferable. We introduce a partially transferable utility model that interpolates between these two extremes using a selfishness parameter λ . Our model is that an agent may be willing to lose on purpose, sacrificing some of her own chance of winning, but only if the colluding pair’s joint gain is more than λ times the individual’s sacrifice. We show that no fair tournament rule can prevent manipulations when λ < 1 . We computationally solve for fair and manipulation-resistant tournament rules for λ = 1 for up to 6 agents. We conjecture and leave as a major open problem that such a tournament rule exists for all n. We analyze the trade-offs between “relative” and “absolute” approximate strategyproofness for previously studied rules and derive as a corollary that all of these rules require λ≥ (n) to be robust to manipulation. We show that for stronger notions of fairness, non-manipulable tournament rules are closely related to tournament rules that witness decreasing gains from manipulation as the number of agents increases.
In dynamic programming and reinforcement learning, the policy for the sequential decision making of an agent in a stochastic environment is usually determined by expressing the goal as a scalar reward function and seeking a policy that maximizes the expected total reward. However, many goals that humans care about naturally concern multiple aspects of the world, and it may not be obvious how to condense those into a single reward function. Furthermore, maximization suffers from specification gaming, where the obtained policy achieves a high expected total reward in an unintended way, often taking extreme or nonsensical actions. Here we consider finite acyclic Markov Decision Processes with multiple distinct evaluation metrics, which do not necessarily represent quantities that the user wants to be maximized. We assume the task of the agent is to ensure that the vector of expected totals of the evaluation metrics falls into some given convex set, called the aspiration set. Our algorithm guarantees that this task is fulfilled by using simplices to approximate feasibility sets and propagate aspirations forward while ensuring they remain feasible. It has complexity linear in the number of possible state-action-successor triples and polynomial in the number of evaluation metrics. Moreover, the explicitly non-maximizing nature of the chosen policy and goals yields additional degrees of freedom, which can be used to apply heuristic safety criteria to the choice of actions. We discuss several such safety criteria that aim to steer the agent towards more conservative behavior.
A tournament organizer must select one of n possible teams as the winner of a competition after observing all ( [ n; 2 ]) matches between them. The organizer would like to find a tournament rule that simultaneously satisfies the following desiderata. It must be Condorcet-consistent (henceforth, CC), meaning it selects as the winner the unique team that beats all other teams (if one exists). It must also be strongly non-manipulable for groups of size k at probability α (henceforth, k-SNM-α ), meaning that no subset of ≤ k teams can fix the matches among themselves in order to increase the chances any of it’s members being selected by more than α . Our contributions are threefold. First, wee consider a natural generalization of the Randomized Single Elimination Bracket rule from [18] to d-ary trees and provide upper bounds to its manipulability. Then, we propose a novel tournament rule that is CC and 3-SNM-1/2 , a strict improvement upon the recent work of [7] who proposed a CC and 3-SNM-31/60 rule. Finally, we initiate the study of reductions among tournament rules.
