Search Results

Documents authored by Perelli, Giuseppe

Document
DOI: 10.4230/LIPIcs.TIME.2022.15
Giving Instructions in Linear Temporal Logic

Authors: Julian Gutierrez, Sarit Kraus, Giuseppe Perelli, and Michael Wooldridge

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)

Abstract
Our aim is to develop a formal semantics for giving instructions to taskable agents, to investigate the complexity of decision problems relating to these semantics, and to explore the issues that these semantics raise. In the setting we consider, agents are given instructions in the form of Linear Temporal Logic (LTL) formulae; the intuitive interpretation of such an instruction is that the agent should act in such a way as to ensure the formula is satisfied. At the same time, agents are assumed to have inviolable and immutable background safety requirements, also specified as LTL formulae. Finally, the actions performed by an agent are assumed to have costs, and agents must act within a limited budget. For this setting, we present a range of interpretations of an instruction to achieve an LTL task Υ, intuitively ranging from "try to do this but only if you can do so with everything else remaining unchanged" up to "drop everything and get this done." For each case we present a formal pre-/post-condition semantics, and investigate the computational issues that they raise.
Cite as

Julian Gutierrez, Sarit Kraus, Giuseppe Perelli, and Michael Wooldridge. Giving Instructions in Linear Temporal Logic. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gutierrez_et_al:LIPIcs.TIME.2022.15,
  author =	{Gutierrez, Julian and Kraus, Sarit and Perelli, Giuseppe and Wooldridge, Michael},
  title =	{{Giving Instructions in Linear Temporal Logic}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{15:1--15:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-262-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{247},
  editor =	{Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.15},
  URN =		{urn:nbn:de:0030-drops-172622},
  doi =		{10.4230/LIPIcs.TIME.2022.15},
  annote =	{Keywords: Linear Temporal Logic, Synthesis, Game theory, Multi-Agent Systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.22
Equilibrium Design for Concurrent Games

Authors: Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael Wooldridge

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we study the design of incentives so that a desirable equilibrium is obtained, for instance, an equilibrium satisfying a given temporal logic property - a problem that we call equilibrium design. We base our study on a framework where system specifications are represented as temporal logic formulae, games as quantitative concurrent game structures, and players' goals as mean-payoff objectives. In particular, we consider system specifications given by LTL and GR(1) formulae, and show that implementing a mechanism to ensure that a given temporal logic property is satisfied on some/every Nash equilibrium of the game, whenever such a mechanism exists, can be done in PSPACE for LTL properties and in NP/Sigma^P_2 for GR(1) specifications. We also study the complexity of various related decision and optimisation problems, such as optimality and uniqueness of solutions, and show that the complexities of all such problems lie within the polynomial hierarchy. As an application, equilibrium design can be used as an alternative solution to the rational synthesis and verification problems for concurrent games with mean-payoff objectives whenever no solution exists, or as a technique to repair, whenever possible, concurrent games with undesirable rational outcomes (Nash equilibria) in an optimal way.
Cite as

Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael Wooldridge. Equilibrium Design for Concurrent Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{gutierrez_et_al:LIPIcs.CONCUR.2019.22,
  author =	{Gutierrez, Julian and Najib, Muhammad and Perelli, Giuseppe and Wooldridge, Michael},
  title =	{{Equilibrium Design for Concurrent Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{22:1--22:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.22},
  URN =		{urn:nbn:de:0030-drops-109246},
  doi =		{10.4230/LIPIcs.CONCUR.2019.22},
  annote =	{Keywords: Games, Temporal logic, Synthesis, Model checking, Nash equilibrium}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.6
Hierarchical Cost-Parity Games

Authors: Laura Bozzelli, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
Cost-parity games are a fundamental tool in system design for the analysis of reactive and distributed systems that recently have received a lot of attention from the formal methods research community. They allow to reason about the time delay on the requests granted by systems, with a bounded consumption of resources, in their executions. In this paper, we contribute to research on Cost-parity games by combining them with hierarchical systems, a successful method for the succinct representation of models. We show that determining the winner of a Hierarchical Cost-parity Game is PSpace-Complete, thus matching the complexity of the proper special case of Hierarchical Parity Games. This shows that reasoning about temporal delay can be addressed at a free cost in terms of complexity.
Cite as

Laura Bozzelli, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino. Hierarchical Cost-Parity Games. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bozzelli_et_al:LIPIcs.TIME.2017.6,
  author =	{Bozzelli, Laura and Murano, Aniello and Perelli, Giuseppe and Sorrentino, Loredana},
  title =	{{Hierarchical Cost-Parity Games}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.6},
  URN =		{urn:nbn:de:0030-drops-79175},
  doi =		{10.4230/LIPIcs.TIME.2017.6},
  annote =	{Keywords: Parity Games, Cost-Parity Games, Hierarchical Systems, System Verification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.17
Nash Equilibrium and Bisimulation Invariance

Authors: Julian Gutierrez, Paul Harrenstein, Giuseppe Perelli, and Michael Wooldridge

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Game theory provides a well-established framework for the analysis of concurrent and multi-agent systems. The basic idea is that concurrent processes (agents) can be understood as corresponding to players in a game; plays represent the possible computation runs of the system; and strategies define the behaviour of agents. Typically, strategies are modelled as functions from sequences of system states to player actions. Analysing a system in such a way involves computing the set of (Nash) equilibria in the game. However, we show that, with respect to the above model of strategies---the standard model in the literature---bisimilarity does not preserve the existence of Nash equilibria. Thus, two concurrent games which are behaviourally equivalent from a semantic perspective, and which from a logical perspective satisfy the same temporal formulae, nevertheless have fundamentally different properties from a game theoretic perspective. In this paper we explore the issues raised by this discovery, and investigate three models of strategies with respect to which the existence of Nash equilibria is preserved under bisimilarity. We also use some of these models of strategies to provide new semantic foundations for logics for strategic reasoning, and investigate restricted scenarios where bisimilarity can be shown to preserve the existence of Nash equilibria with respect to the conventional model of strategies in the literature.
Cite as

Julian Gutierrez, Paul Harrenstein, Giuseppe Perelli, and Michael Wooldridge. Nash Equilibrium and Bisimulation Invariance. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gutierrez_et_al:LIPIcs.CONCUR.2017.17,
  author =	{Gutierrez, Julian and Harrenstein, Paul and Perelli, Giuseppe and Wooldridge, Michael},
  title =	{{Nash Equilibrium and Bisimulation Invariance}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{17:1--17:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.17},
  URN =		{urn:nbn:de:0030-drops-77902},
  doi =		{10.4230/LIPIcs.CONCUR.2017.17},
  annote =	{Keywords: Bisumulation, Nash equilibrium, Multiagent systems, Strategy logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.648
Binding Forms in First-Order Logic

Authors: Fabio Mogavero and Giuseppe Perelli

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
Aiming to pinpoint the reasons behind the decidability of some complex extensions of modal logic, we propose a new classification criterion for sentences of first-order logic, which is based on the kind of binding forms admitted in their expressions, i.e., on the way the arguments of a relation can be bound to a variable. In particular, we describe a hierarchy of four fragments focused on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with several first-order limitations proposed in the literature, as the guarded and unary negation fragments. We also prove, via a novel model-theoretic technique, that our logic enjoys the finite-model property, Craig's interpolation, and Beth's definability. Furthermore, the associated model-checking and satisfiability problems are solvable in PTime and Sigma_3^P, respectively.
Cite as

Fabio Mogavero and Giuseppe Perelli. Binding Forms in First-Order Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 648-665, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{mogavero_et_al:LIPIcs.CSL.2015.648,
  author =	{Mogavero, Fabio and Perelli, Giuseppe},
  title =	{{Binding Forms in First-Order Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{648--665},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.648},
  URN =		{urn:nbn:de:0030-drops-54443},
  doi =		{10.4230/LIPIcs.CSL.2015.648},
  annote =	{Keywords: First-Order Logic, Decidable Fragments, Satisfiability, Model Checking}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact