A fuzzy fixed-point theorem and its applications to maximal elements and Nash equilibria in noncompact CAT(0) spaces

In this paper, based on the KKM method, we prove a new fuzzy fixed-point theorem in noncompact CAT(0) spaces. As applications of this fixed-point theorem, we obtain some existence theorems of fuzzy maximal element points. Finally, we utilize these fuzzy maximal element theorems to establish some new existence theorems of Nash equilibrium points for generalized fuzzy noncooperative games and fuzzy noncooperative qualitative games in noncompact CAT(0) spaces. The results obtained in this paper generalize and extend many known results in the existing literature.

Two Options for the Branching of Histories

The chapter discusses how the histories in a common BST structure are related. By the axioms of the core theory of BST, any two histories share some past, but there are different ways to implement this. These are distinguished by the so-called prior choice principles, which make specific demands on the way in which histories branch. On one option (which yields structures of BST92), histories branch, or remain undivided, at points, which means that there is a maximal element in the overlap of any two histories. The other option (which yields BSTNF structures) prohibits the existence of such maximal elements and works with so-called choice sets. The chapter discusses the pattern of branching in the two theories, BST92 and BSTNF, also with respect to topology. As it turns out, the two theories are are intertranslatable. The chapter ends with a sketch of these translatability results.

Vacuity in synthesis

In reactive synthesis, one begins with a temporal specification $$\varphi $$ φ , and automatically synthesizes a system $$M$$ M such that $$M\models \varphi $$ M ⊧ φ . As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies $$\varphi $$ φ non-vacuously, then M is likely to be closer to the user’s intent, because it satisfies $$\varphi $$ φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.

Arrovian Aggregation of Convex Preferences

We consider social welfare functions that satisfy Arrow's classic axioms of independence of irrelevant alternatives and Pareto optimality when the outcome space is the convex hull of some finite set of alternatives. Individual and collective preferences are assumed to be continuous and convex, which guarantees the existence of maximal elements and the consistency of choice functions that return these elements, even without insisting on transitivity. We provide characterizations of both the domains of preferences and the social welfare functions that allow for anonymous Arrovian aggregation. The domains admit arbitrary preferences over alternatives, which completely determine an agent's preferences over all mixed outcomes. On these domains, Arrow's impossibility turns into a complete characterization of a unique social welfare function, which can be readily applied in settings involving divisible resources such as probability, time, or money.

Minimal Coverability Tree Construction Made Complete and Efficient

Downward closures of Petri net reachability sets can be finitely represented by their set of maximal elements called the minimal coverability set or Clover. Many properties (coverability, boundedness, ...) can be decided using Clover, in a time proportional to the size of Clover. So it is crucial to design algorithms that compute it efficiently. We present a simple modification of the original but incomplete Minimal Coverability Tree algorithm (MCT), computing Clover, which makes it complete: it memorizes accelerations and fires them as ordinary transitions. Contrary to the other alternative algorithms for which no bound on the size of the required additional memory is known, we establish that the additional space of our algorithm is at most doubly exponential. Furthermore we have implemented a prototype which is already very competitive: on benchmarks it uses less space than all the other tools and its execution time is close to the one of the fastest tool.

a-Pseudo complementation on ADL’s

In this paper, we introduce the concept of an [Formula: see text]-pseudo complementation [Formula: see text] on an Almost Distributive Lattice [Formula: see text] for an arbitrary fixed element [Formula: see text] and any [Formula: see text] of [Formula: see text] and discuss several properties of this. Here, we obtain a bijection correspondence between the [Formula: see text]-pseudo complementations on [Formula: see text] and maximal elements of [Formula: see text] We prove that the set [Formula: see text] is a Boolean algebra which is independent(upto isomorphism) of the [Formula: see text]-pseudo complementation [Formula: see text].

On Maximal Elements with Applications to Abstract Economies, Fixed Point Theory and Eigenvector Problems

Two existence theorems of maximal elements in H-spaces are obtained without compactness. More accurately, we deal with the correspondence to be of L -majorized mappings in the setting of noncompact strategy sets but merely requiring a milder coercive condition. As applications, we obtain an equilibrium existence theorem for general abstract economies, a new fixed point theorem, and give a sufficient condition for the existence of solutions of the eigenvector problem (EIVP).