اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدATLsc with partial observation
345
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that uniform incomplete observation (where all players have the same observation) preserves decidability of the model-checking problem, even for very expressive logics such as ATLsc.
قيم البحث
اقرأ أيضاً
The current work introduces the notion of pdominant sets and studies their recursion-theoretic properties. Here a set A is called pdominant iff there is a partial A-recursive function {psi} such that for every partial recursive function {phi} and alm
ost every x in the domain of {phi} there is a y in the domain of {psi} with y<= x and {psi}(y) > {phi}(x). While there is a full {pi}01-class of nonrecursive sets where no set is pdominant, there is no {pi}01-class containing only pdominant sets. No weakly 2-generic set is pdominant while there are pdominant 1-generic sets below K. The halves of Chaitins {Omega} are pdominant. No set which is low for Martin-Lof random is pdominant. There is a low r.e. set which is pdominant and a high r.e. set which is not pdominant.
It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms as soon as they are not h-propositions. A natural question
is then whether univalence restricted to h-propositions is compatible with UIP. We answer this affirmatively by constructing a model where types are elements of a closed universe defined as a higher inductive type in homotopy type theory. This universe has a path constructor for simultaneous partial univalent completion, i.e., restricted to h-propositions. More generally, we show that univalence restricted to $(n-1)$-types is consistent with the assumption that all types are $n$-truncated. Moreover we parametrize our construction by a suitably well-behaved container, to abstract from a concrete choice of type formers for the universe.
Partial methods play an important role in formal methods and beyond. Recently such methods were developed for parity games, where polynomial-time partial solvers decide the winners of a subset of nodes. We investigate here how effective polynomial-ti
me partial solvers can be by studying interactions of partial solvers based on generic composition patterns that preserve polynomial-time computability. We show that use of such composition patterns discovers new partial solvers - including those that merge node sets that have the same but unknown winner - by studying games that composed partial solvers can neither solve nor simplify. We experimentally validate that this data-driven approach to refinement leads to polynomial-time partial solvers that can solve all standard benchmarks of structured games. For one of these polynomial-time partial solvers not even a sole random game from a few billion random games of varying configuration was found that it wont solve completely.
In this paper, the well-known forwarders dilemma is generalized by accounting for the presence of link quality fluctuations; the forwarders dilemma is a four-node interaction model with two source nodes and two destination nodes. It is known to be ve
ry useful to study ad hoc networks. To characterize the long-term utility region when the source nodes have to control their power with partial channel state information (CSI), we resort to a recent result in Shannon theory. It is shown how to exploit this theoretical result to find the long-term utility region and determine good power control policies. This region is of prime importance since it provides the best performance possible for a given knowledge at the nodes. Numerical results provide several new insights into the repeated forwarders dilemma power control problem; for instance, the knowledge of global CSI only brings a marginal performance improvement with respect to the local CSI case.
Auction theory traditionally assumes that bidders valuation distributions are known to the auctioneer, such as in the celebrated, revenue-optimal Myerson auction. However, this theory does not describe how the auctioneer comes to possess this informa
tion. Recently, Cole and Roughgarden [2014] showed that an approximation based on a finite sample of independent draws from each bidders distribution is sufficient to produce a near-optimal auction. In this work, we consider the problem of learning bidders valuation distributions from much weaker forms of observations. Specifically, we consider a setting where there is a repeated, sealed-bid auction with $n$ bidders, but all we observe for each round is who won, but not how much they bid or paid. We can also participate (i.e., submit a bid) ourselves, and observe when we win. From this information, our goal is to (approximately) recover the inherently recoverable part of the underlying bid distributions. We also consider extensions where different subsets of bidders participate in each round, and where bidders valuations have a common-value component added to their independent private values.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
