4 Search Results for "Mover, Sergio"

Document
DOI: 10.4230/LIPIcs.ITCS.2025.10
Algorithmic Collusion Without Threats

Authors: Eshwar Ram Arunachaleswaran, Natalie Collina, Sampath Kannan, Aaron Roth, and Juba Ziani

Published in: LIPIcs, Volume 325, 16th Innovations in Theoretical Computer Science Conference (ITCS 2025)

Abstract
There has been substantial recent concern that automated pricing algorithms might learn to "collude." Supra-competitive prices can emerge as a Nash equilibrium of repeated pricing games, in which sellers play strategies which threaten to punish their competitors if they ever "defect" from a set of supra-competitive prices, and these strategies can be automatically learned. But threats are anti-competitive on their face. In fact, a standard economic intuition is that supra-competitive prices emerge from either the use of threats, or a failure of one party to correctly optimize their payoff. Is this intuition correct? Would explicitly preventing threats in algorithmic decision-making prevent supra-competitive prices when sellers are optimizing for their own revenue? No. We show that supra-competitive prices can robustly emerge even when both players are using algorithms which do not explicitly encode threats, and which optimize for their own revenue. Since deploying an algorithm is a form of commitment, we study sequential Bertrand pricing games (and a continuous variant) in which a first mover deploys an algorithm and then a second mover optimizes within the resulting environment. We show that if the first mover deploys any algorithm with a no-regret guarantee, and then the second mover even approximately optimizes within this now static environment, monopoly-like prices arise. The result holds for any no-regret learning algorithm deployed by the first mover and for any pricing policy of the second mover that obtains them profit at least as high as a random pricing would - and hence the result applies even when the second mover is optimizing only within a space of non-responsive pricing distributions which are incapable of encoding threats. In fact, there exists a set of strategies, neither of which explicitly encode threats that form a Nash equilibrium of the simultaneous pricing game in algorithm space, and lead to near monopoly prices. This suggests that the definition of "algorithmic collusion" may need to be expanded, to include strategies without explicitly encoded threats.
Cite as

Eshwar Ram Arunachaleswaran, Natalie Collina, Sampath Kannan, Aaron Roth, and Juba Ziani. Algorithmic Collusion Without Threats. In 16th Innovations in Theoretical Computer Science Conference (ITCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 325, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{arunachaleswaran_et_al:LIPIcs.ITCS.2025.10,
  author =	{Arunachaleswaran, Eshwar Ram and Collina, Natalie and Kannan, Sampath and Roth, Aaron and Ziani, Juba},
  title =	{{Algorithmic Collusion Without Threats}},
  booktitle =	{16th Innovations in Theoretical Computer Science Conference (ITCS 2025)},
  pages =	{10:1--10:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-361-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{325},
  editor =	{Meka, Raghu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2025.10},
  URN =		{urn:nbn:de:0030-drops-226386},
  doi =		{10.4230/LIPIcs.ITCS.2025.10},
  annote =	{Keywords: Algorithmic Game Theory, Algorithmic Collusion, No-Regret Dynamics}
}
Document
Artifact
DOI: 10.4230/DARTS.5.2.13
Lifestate: Event-Driven Protocols and Callback Control Flow (Artifact)

Authors: Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang

Published in: DARTS, Volume 5, Issue 2, Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Developing interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interface (API) calls that in turn affect the set of possible future callbacks. An app violates the protocol when, for example, it calls a particular API method in a state of the framework where such a call is invalid. What makes automated reasoning hard in this domain is largely what makes programming apps against such frameworks hard: the specification of the protocol is unclear, and the control flow is complex, asynchronous, and higher-order. In this paper, we tackle the problem of specifying and modeling event-driven application-programming protocols. In particular, we formalize a core meta-model that captures the dialogue between event-driven frameworks and application callbacks. Based on this meta-model, we define a language called lifestate that permits precise and formal descriptions of application-programming protocols and the callback control flow imposed by the event-driven framework. Lifestate unifies modeling what app callbacks can expect of the framework with specifying rules the app must respect when calling into the framework. In this way, we effectively combine lifecycle constraints and typestate rules. To evaluate the effectiveness of lifestate modeling, we provide a dynamic verification algorithm that takes as input a trace of execution of an app and a lifestate protocol specification to either produce a trace witnessing a protocol violation or a proof that no such trace is realizable.
Cite as

Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang. Lifestate: Event-Driven Protocols and Callback Control Flow (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 13:1-13:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{meier_et_al:DARTS.5.2.13,
  author =	{Meier, Shawn and Mover, Sergio and Chang, Bor-Yuh Evan},
  title =	{{Lifestate: Event-Driven Protocols and Callback Control Flow}},
  pages =	{13:1--13:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{2},
  editor =	{Meier, Shawn and Mover, Sergio and Chang, Bor-Yuh Evan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.5.2.13},
  URN =		{urn:nbn:de:0030-drops-107902},
  doi =		{10.4230/DARTS.5.2.13},
  annote =	{Keywords: domain-specific languages, event-based programming, language implementation, new programming models or languages, object-oriented programming, semantics, testing, verification, automated}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2019.1
Lifestate: Event-Driven Protocols and Callback Control Flow

Authors: Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Developing interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interface (API) calls that in turn affect the set of possible future callbacks. An app violates the protocol when, for example, it calls a particular API method in a state of the framework where such a call is invalid. What makes automated reasoning hard in this domain is largely what makes programming apps against such frameworks hard: the specification of the protocol is unclear, and the control flow is complex, asynchronous, and higher-order. In this paper, we tackle the problem of specifying and modeling event-driven application-programming protocols. In particular, we formalize a core meta-model that captures the dialogue between event-driven frameworks and application callbacks. Based on this meta-model, we define a language called lifestate that permits precise and formal descriptions of application-programming protocols and the callback control flow imposed by the event-driven framework. Lifestate unifies modeling what app callbacks can expect of the framework with specifying rules the app must respect when calling into the framework. In this way, we effectively combine lifecycle constraints and typestate rules. To evaluate the effectiveness of lifestate modeling, we provide a dynamic verification algorithm that takes as input a trace of execution of an app and a lifestate protocol specification to either produce a trace witnessing a protocol violation or a proof that no such trace is realizable.
Cite as

Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang. Lifestate: Event-Driven Protocols and Callback Control Flow. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 1:1-1:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{meier_et_al:LIPIcs.ECOOP.2019.1,
  author =	{Meier, Shawn and Mover, Sergio and Chang, Bor-Yuh Evan},
  title =	{{Lifestate: Event-Driven Protocols and Callback Control Flow}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{1:1--1:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.1},
  URN =		{urn:nbn:de:0030-drops-107932},
  doi =		{10.4230/LIPIcs.ECOOP.2019.1},
  annote =	{Keywords: event-driven systems, application-programming protocols, application framework interfaces, callbacks, sound framework modeling, predictive dynamic verification}
}
Document
Informal Presentation
DOI: 10.4230/OASIcs.SynCoP.2015.106
Parameter Synthesis with IC3 (Informal Presentation)

Authors: Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
Parametric systems arise in many application domains, from real-time systems to software to cyber-physical systems. Parameters are fundamental to model unknown quantities at design time and allow a designer to explore different instantiation of the system (i.e. every parameter valuation induces a different system), during the early development phases. A key challenge is to automatically synthesize all the parameter valuations for which the system satisfies some properties. In this talk we focus on the parameter synthesis problem for infinite-state transition systems and invariant properties. We describe the synthesis algorithm Param IC3, which is based on IC3, one of the major recent breakthroughs in SAT-based model checking, and lately extended to the SMT case. The algorithm follows a general approach that first builds the set of "bad" parameter valuations and then obtain the set of "good" valuations by complement. The approach enumerates the counterexamples that violate the property, extracting from each counterexample a region of bad parameter valuations, existentially quantifying the state variables. ParamIC3 follows the same principles, but it overcomes some limitations of the previous approach by exploiting the IC3 features. First, IC3 may find a set of counterexamples s_o, ..., s_k, where each state in s_i is guaranteed to reach some of the bad states in s_k in k-i steps; this is exploited to apply the expensive quantifier elimination on shortest, and thus more amenable, counterexamples. Second, the internal structure of IC3 allows our extension to be integrated in a fully incremental fashion, never restarting the search from scratch to find a new counterexample. While various approaches already solve the parameter synthesis problem for several kind of systems, like infinite-state transition systems, timed and hybrid automata, the advantages ParamIC3 are that: it synthesizes an optimal region of parameters, it avoids computing the whole set of the reachable states, it is incremental and applies quantifier elimination only to small formulas. We present the results of an experimental evaluation performed on benchmarks from the timed and hybrid systems domain. We compared the approach with similar SMT-based techniques and with techniques based on the computation of the reachable states. The results show the potential of our approach.
Cite as

Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. Parameter Synthesis with IC3 (Informal Presentation). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 106-107, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cimatti_et_al:OASIcs.SynCoP.2015.106,
  author =	{Cimatti, Alessandro and Griggio, Alberto and Mover, Sergio and Tonetta, Stefano},
  title =	{{Parameter Synthesis with IC3}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{106--107},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.106},
  URN =		{urn:nbn:de:0030-drops-56144},
  doi =		{10.4230/OASIcs.SynCoP.2015.106},
  annote =	{Keywords: Parameter Synthesis, Infinite-state Transition Systems, Satisfiability Modulo Theories, IC3}
}
  • Refine by Type
  • 4 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 2 2019
  • 1 2015

  • Refine by Author
  • 3 Mover, Sergio
  • 2 Chang, Bor-Yuh Evan
  • 2 Meier, Shawn
  • 1 Arunachaleswaran, Eshwar Ram
  • 1 Cimatti, Alessandro
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs
  • 1 OASIcs
  • 1 DARTS

  • Refine by Classification
  • 2 Software and its engineering → Software verification
  • 1 Theory of computation → Algorithmic game theory

  • Refine by Keyword
  • 1 Algorithmic Collusion
  • 1 Algorithmic Game Theory
  • 1 IC3
  • 1 Infinite-state Transition Systems
  • 1 No-Regret Dynamics
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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