BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Valentin Goranko

Valentin Goranko contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer ScienceComputer Science and Game Theorymath.LOMultiagent SystemsArtificial Intelligencemath.COCryptography and Security

Trust snapshot

Quick read

Trust 21 - Emerging
13works
0followers
7topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

13 published item(s)

preprint2023arXiv

Structural theory of trees. I. Branching and condensations of trees

Trees are partial orders in which every element has a linearly ordered set of predecessors. Here we initiate the exploration of the structural theory of trees with the study of different notions of \emph{branching in trees} and of \emph{condensed trees}, which are trees in which every node is a branching node. We then introduce and investigate two different constructions of \emph{tree condensations} -- one shrinking, and the other expanding, the tree to a condensed tree.

0 citations0 reviewsNo code linkedOpen access
preprint2023arXiv

Structural theory of trees. II. Completeness and completions of trees

Trees are partial orderings where every element has a linearly ordered set of smaller elements. We define and study several natural notions of completeness of trees, extending Dedekind completeness of linear orders and Dedekind-MacNeille completions of partial orders. We then define constructions of \emph{tree completions} that extend any tree to a minimal one satisfying the respective completeness property.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

The temporal logic of coalitional goal assignments in concurrent multi-player games

We introduce and study a natural extension of the Alternating time temporal logic ATL, called Temporal Logic of Coalitional Goal Assignments (TLCGA). It features just one, but quite expressive, coalitional strategic operator, viz. the coalitional goal assignment operator, which is based on a mapping assigning to each set of players in the game its coalitional goal, formalised by a path formula of the language of TLCGA, i.e. a formula prefixed with a temporal operator X,U, or G, representing a temporalised objective for the respective coalition, describing the property of the plays on which that objective is satisfied. We establish fixpoint characterizations of the temporal goal assignments in a mu-calculus extension of TLCGA, discuss its expressiveness and illustrate it with some examples, prove bisimulation invariance and Hennessy-Milner property for it with respect to a suitably defined notion of bisimulation, construct a sound and complete axiomatic system for TLCGA, and obtain its decidability via finite model property.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

A Logic for Conditional Local Strategic Reasoning

We consider systems of rational agents who act and interact in pursuit of their individual and collective objectives. We study and formalise the reasoning of an agent, or of an external observer, about the expected choices of action of the other agents based on their objectives, in order to assess the reasoner's ability, or expectation, to achieve their own objective. To formalize such reasoning we extend Pauly's Coalition Logic with three new modal operators of conditional strategic reasoning, thus introducing the Logic for Local Conditional Strategic Reasoning ConStR. We provide formal semantics for the new conditional strategic operators in concurrent game models, introduce the matching notion of bisimulation for each of them, prove bisimulation invariance and Hennessy-Milner property for each of them, and discuss and compare briefly their expressiveness. Finally, we also propose systems of axioms for each of the basic operators of ConStR and for the full logic.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Logic-based Specification and Verification of Homogeneous Dynamic Multi-agent Systems

We develop a logic-based framework for formal specification and algorithmic verification of homogeneous and dynamic concurrent multi-agent transition systems (HDMAS). Homogeneity means that all agents have the same available actions at any given state and the actions have the same effects regardless of which agents perform them. The state transitions are therefore determined only by the vector of numbers of agents performing each action and are specified symbolically, by means of conditions on these numbers definable in Presburger arithmetic. The agents are divided into controllable (by the system supervisor/controller) and uncontrollable, representing the environment or adversary. Dynamicity means that the numbers of controllable and uncontrollable agents may vary throughout the system evolution, possibly at every transition. As a language for formal specification we use a suitably extended version of Alternating-time Temporal Logic (ATL), where one can specify properties of the type "a coalition of (at least) $n$ controllable agents can ensure against (at most) $m$ uncontrollable agents that any possible evolution of the system satisfies a given objective $φ$", where $φ$ is specified again as a formula of that language and each of $n$ and $m$ is either a fixed number or a variable that can be quantified over. We provide formal semantics to our logic $\mathcal{L}_{HDMAS}$ and define normal form of its formulae. We then prove that every formula in $\mathcal{L}_{HDMAS}$ is equivalent in the finite to one in a normal form and develop an algorithm for global model checking of formulae in normal form in finite HDMAS models, which invokes model checking truth of Presburger formulae. We establish worst case complexity estimates for the model checking algorithm and illustrate it on a running example.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temporal Logic ATL+

We develop a sound, complete and practically implementable tableaux-based decision method for constructive satisfiability testing and model synthesis in the fragment ATL+ of the full Alternating time temporal logic ATL*. The method extends in an essential way a previously developed tableaux-based decision method for ATL and works in 2EXPTIME, which is the optimal worst case complexity of the satisfiability problem for ATL+ . We also discuss how suitable parametrizations and syntactic restrictions on the class of input ATL+ formulae can reduce the complexity of the satisfiability problem.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Secure aggregation of distributed information: How a team of agents can safely share secrets in front of a spy

We consider the generic problem of Secure Aggregation of Distributed Information (SADI), where several agents acting as a team have information distributed among them, modeled by means of a publicly known deck of cards distributed among the agents, so that each of them knows only her cards. The agents have to exchange and aggregate the information about how the cards are distributed among them by means of public announcements over insecure communication channels, intercepted by an adversary "eavesdropper", in such a way that the adversary does not learn who holds any of the cards. We present a combinatorial construction of protocols that provides a direct solution of a class of SADI problems and develop a technique of iterated reduction of SADI problems to smaller ones which are eventually solvable directly. We show that our methods provide a solution to a large class of SADI problems, including all SADI problems with sufficiently large size and sufficiently balanced card distributions.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games (Extended Abstract)

We propose a logical framework combining a game-theoretic study of abilities of agents to achieve quantitative objectives in multi-player games by optimizing payoffs or preferences on outcomes with a logical analysis of the abilities of players for achieving qualitative objectives of players, i.e., reaching or maintaining game states with desired properties. We enrich concurrent game models with payoffs for the normal form games associated with the states of the model and propose a quantitative extension of the logic ATL* enabling the combination of quantitative and qualitative reasoning.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Non-cooperative games with preplay negotiations

We consider an extension of strategic normal form games with a phase of negotiations before the actual play of the game, where players can make binding offers for transfer of utilities to other players after the play of the game, in order to provide additional incentives for each other to play designated strategies. Such offers are conditional on the recipients playing the specified strategies and they effect transformations of the payoff matrix of the game by accordingly transferring payoffs between players. We introduce and analyze solution concepts for 2-player normal form games with such preplay offers under various assumptions for the preplay negotiation phase and obtain results for existence of efficient negotiation strategies of the players. Then we extend the framework to coalitional preplay offers in N-player games, as well as to extensive form games with inter-play offers for side payments.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Two-player preplay negotiation games with conditional offers

We consider an extension of strategic normal form games with a phase before the actual play of the game, where players can make binding offers for transfer of utilities to other players after the play of the game, contingent on the recipient playing the strategy indicated in the offer. Such offers transform the payoff matrix of the original game but preserve its non-cooperative nature. The type of offers we focus on here are conditional on a suggested 'matching offer' of the same kind made in return by the receiver. Players can exchange a series of such offers, thus engaging in a bargaining process before a strategic normal form game is played. In this paper we study and analyze solution concepts for two-player normal form games with such preplay negotiation phase, under several assumptions for the bargaining power of the players, such as the possibility of withdrawing previously made offers and opting out from the negotiation process, as well as the value of time for the players in such negotiations. We obtain results describing the possible solutions of such bargaining games and analyze the degrees of efficiency and fairness that can be achieved in such negotiation process.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Tableau-based decision procedure for the multi-agent epistemic logic with all coalitional operators for common and distributed knowledge

We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi-agent epistemic logic CMAEL(CD) with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for CMAEL(CD) and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using that result, we design an incremental tableau-building procedure that eventually constructs a satisfying Hintikka structure for every satisfiable input set of formulae of CMAEL(CD) and closes for every unsatisfiable input set of formulae.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Transformations of normal form games by preplay offers for payments among players

We consider transformations of normal form games by binding preplay offers of players for payments of utility to other players conditional on them playing designated in the offers strategies. The game-theoretic effect of such preplay offers is transformation of the payoff matrix of the game by transferring payoffs between players. Here we analyze and completely characterize the possible transformations of the payoff matrix of a normal form game by sets of preplay offers.

0 citations0 reviewsNo code linkedOpen access
preprint2008arXiv

Tableau-based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge

We develop an incremental-tableau-based decision procedure for the multi-agent epistemic logic MAEL(CD) (aka S5_n (CD)), whose language contains operators of individual knowledge for a finite set Ag of agents, as well as operators of distributed and common knowledge among all agents in Ag. Our tableau procedure works in (deterministic) exponential time, thus establishing an upper bound for MAEL(CD)-satisfiability that matches the (implicit) lower-bound known from earlier results, which implies ExpTime-completeness of MAEL(CD)-satisfiability. Therefore, our procedure provides a complexity-optimal algorithm for checking MAEL(CD)-satisfiability, which, however, in most cases is much more efficient. We prove soundness and completeness of the procedure, and illustrate it with an example.

0 citations0 reviewsNo code linkedOpen access