5 Search Results for "Victor, Will"


Document
Invited Talk
A Tour on Ecumenical Systems (Invited Talk)

Authors: Elaine Pimentel and Luiz Carlos Pereira

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)


Abstract
Ecumenism can be understood as a pursuit of unity, where diverse thoughts, ideas, or points of view coexist harmoniously. In logic, ecumenical systems refer, in a broad sense, to proof systems for combining logics. One captivating area of research over the past few decades has been the exploration of seamlessly merging classical and intuitionistic connectives, allowing them to coexist peacefully. In this paper, we will embark on a journey through ecumenical systems, drawing inspiration from Prawitz' seminal work [Dag Prawitz, 2015]. We will begin by elucidating Prawitz' concept of "ecumenism" and present a pure sequent calculus version of his system. Building upon this foundation, we will expand our discussion to incorporate alethic modalities, leveraging Simpson’s meta-logical characterization. This will enable us to propose several proof systems for ecumenical modal logics. We will conclude our tour with some discussion towards a term calculus proposal for the implicational propositional fragment of the ecumenical logic, the quest of automation using a framework based in rewriting logic, and an ecumenical view of proof-theoretic semantics.

Cite as

Elaine Pimentel and Luiz Carlos Pereira. A Tour on Ecumenical Systems (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{pimentel_et_al:LIPIcs.CALCO.2023.3,
  author =	{Pimentel, Elaine and Pereira, Luiz Carlos},
  title =	{{A Tour on Ecumenical Systems}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{3:1--3:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.3},
  URN =		{urn:nbn:de:0030-drops-188003},
  doi =		{10.4230/LIPIcs.CALCO.2023.3},
  annote =	{Keywords: Intuitionistic logic, classical logic, modal logic, ecumenical systems, proof theory}
}
Document
New Menger-Like Dualities in Digraphs and Applications to Half-Integral Linkages

Authors: Victor Campos, Jonas Costa, Raul Lopes, and Ignasi Sau

Published in: LIPIcs, Volume 274, 31st Annual European Symposium on Algorithms (ESA 2023)


Abstract
We present new min-max relations in digraphs between the number of paths satisfying certain conditions and the order of the corresponding cuts. We define these objects in order to capture, in the context of solving the half-integral linkage problem, the essential properties needed for reaching a large bramble of congestion two (or any other constant) from the terminal set. This strategy has been used ad-hoc in several articles, usually with lengthy technical proofs, and our objective is to abstract it to make it applicable in a simpler and unified way. We provide two proofs of the min-max relations, one consisting in applying Menger’s Theorem on appropriately defined auxiliary digraphs, and an alternative simpler one using matroids, however with worse polynomial running time. As an application, we manage to simplify and improve several results of Edwards et al. [ESA 2017] and of Giannopoulou et al. [SODA 2022] about finding half-integral linkages in digraphs. Concerning the former, besides being simpler, our proof provides an almost optimal bound on the strong connectivity of a digraph for it to be half-integrally feasible under the presence of a large bramble of congestion two (or equivalently, if the directed tree-width is large, which is the hard case). Concerning the latter, our proof uses brambles as rerouting objects instead of cylindrical grids, hence yielding much better bounds and being somehow independent of a particular topology. We hope that our min-max relations will find further applications as, in our opinion, they are simple, robust, and versatile to be easily applicable to different types of routing problems in digraphs.

Cite as

Victor Campos, Jonas Costa, Raul Lopes, and Ignasi Sau. New Menger-Like Dualities in Digraphs and Applications to Half-Integral Linkages. In 31st Annual European Symposium on Algorithms (ESA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 274, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{campos_et_al:LIPIcs.ESA.2023.30,
  author =	{Campos, Victor and Costa, Jonas and Lopes, Raul and Sau, Ignasi},
  title =	{{New Menger-Like Dualities in Digraphs and Applications to Half-Integral Linkages}},
  booktitle =	{31st Annual European Symposium on Algorithms (ESA 2023)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-295-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{274},
  editor =	{G{\o}rtz, Inge Li and Farach-Colton, Martin and Puglisi, Simon J. and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2023.30},
  URN =		{urn:nbn:de:0030-drops-186838},
  doi =		{10.4230/LIPIcs.ESA.2023.30},
  annote =	{Keywords: directed graphs, min-max relation, half-integral linkage, directed disjoint paths, bramble, parameterized complexity, matroids}
}
Document
Invited Talk
Theory Meets Practice in the Algorand Blockchain (Invited Talk)

Authors: Victor Luchangco

Published in: LIPIcs, Volume 253, 26th International Conference on Principles of Distributed Systems (OPODIS 2022)


Abstract
Robust and effective distributed systems require good theory and good engineering, not separately but in concert: user requirements and system constraints are not merely implementation details but often must inform the design of algorithms for such systems. Blockchains are an excellent example. The heart of a blockchain is its (Byzantine) consensus protocol, and consensus protocols have been extensively studied in the theory community for decades. But traditional consensus protocols are not directly applicable to blockchains, which have, or hope to have, millions of participants. Furthermore, public blockchains, which allow anyone to participate, must have some mechanism to guarantee the security of the protocol, and traditional fault models do not adequately capture the assumptions of such mechanisms. In this talk, I will discuss these and other ways in which theory and practice meet in the context of the Algorand blockchain, and how Algorand is able to achieve high transaction throughput with low latency.

Cite as

Victor Luchangco. Theory Meets Practice in the Algorand Blockchain (Invited Talk). In 26th International Conference on Principles of Distributed Systems (OPODIS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 253, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{luchangco:LIPIcs.OPODIS.2022.1,
  author =	{Luchangco, Victor},
  title =	{{Theory Meets Practice in the Algorand Blockchain}},
  booktitle =	{26th International Conference on Principles of Distributed Systems (OPODIS 2022)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-265-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{253},
  editor =	{Hillel, Eshcar and Palmieri, Roberto and Rivi\`{e}re, Etienne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2022.1},
  URN =		{urn:nbn:de:0030-drops-176219},
  doi =		{10.4230/LIPIcs.OPODIS.2022.1},
  annote =	{Keywords: Theory and practice, Design of distributed systems, Blockchain, Consensus, Algorand}
}
Document
Slimming down Petri Boxes: Compact Petri Net Models of Control Flows

Authors: Victor Khomenko, Maciej Koutny, and Alex Yakovlev

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)


Abstract
We look at the construction of compact Petri net models corresponding to process algebra expressions supporting sequential, choice, and parallel compositions. If "silent" transitions are disallowed, a construction based on Cartesian product is traditionally used to construct places in the target Petri net, resulting in an exponential explosion in the net size. We demonstrate that this exponential explosion can be avoided, by developing a link between this construction problem and the problem of finding an edge clique cover of a graph that is guaranteed to be complement-reducible (i.e., a cograph). It turns out that the exponential number of places created by the Cartesian product construction can be reduced down to polynomial (quadratic) even in the worst case, and to logarithmic in the best (non-degraded) case. As these results affect the "core" modelling techniques based on Petri nets, eliminating a source of an exponential explosion, we hope they will have applications in Petri net modelling and translations of various formalisms to Petri nets.

Cite as

Victor Khomenko, Maciej Koutny, and Alex Yakovlev. Slimming down Petri Boxes: Compact Petri Net Models of Control Flows. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{khomenko_et_al:LIPIcs.CONCUR.2022.8,
  author =	{Khomenko, Victor and Koutny, Maciej and Yakovlev, Alex},
  title =	{{Slimming down Petri Boxes: Compact Petri Net Models of Control Flows}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.8},
  URN =		{urn:nbn:de:0030-drops-170710},
  doi =		{10.4230/LIPIcs.CONCUR.2022.8},
  annote =	{Keywords: Petri net, Petri box, cograph, edge clique cover, control flow, static construction, local construction, interface graph, Burst automata, composition}
}
Document
An Efficient Algorithm for Placing Electric Vehicle Charging Stations

Authors: Pankaj K. Agarwal, Jiangwei Pan, and Will Victor

Published in: LIPIcs, Volume 64, 27th International Symposium on Algorithms and Computation (ISAAC 2016)


Abstract
Motivated by the increasing popularity of electric vehicles (EV) and a lack of charging stations in the road network, we study the shortest path hitting set (SPHS) problem. Roughly speaking, given an input graph G, the goal is to compute a small-size subset H of vertices of G such that by placing charging stations at vertices in H, every shortest path in G becomes EV-feasible, i.e., an EV can travel between any two vertices of G through the shortest path with a full charge. In this paper, we propose a bi-criteria approximation algorithm with running time near-linear in the size of G that has a logarithmic approximation on |H| and may require the EV to slightly deviate from the shortest path. We also present a data structure for computing an EV-feasible path between two query vertices of G.

Cite as

Pankaj K. Agarwal, Jiangwei Pan, and Will Victor. An Efficient Algorithm for Placing Electric Vehicle Charging Stations. In 27th International Symposium on Algorithms and Computation (ISAAC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 64, pp. 7:1-7:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{agarwal_et_al:LIPIcs.ISAAC.2016.7,
  author =	{Agarwal, Pankaj K. and Pan, Jiangwei and Victor, Will},
  title =	{{An Efficient Algorithm for Placing Electric Vehicle Charging Stations}},
  booktitle =	{27th International Symposium on Algorithms and Computation (ISAAC 2016)},
  pages =	{7:1--7:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-026-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{64},
  editor =	{Hong, Seok-Hee},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2016.7},
  URN =		{urn:nbn:de:0030-drops-67782},
  doi =		{10.4230/LIPIcs.ISAAC.2016.7},
  annote =	{Keywords: Shortest path hitting set, Charging station placement, Electric vehicle}
}
  • Refine by Author
  • 1 Agarwal, Pankaj K.
  • 1 Campos, Victor
  • 1 Costa, Jonas
  • 1 Khomenko, Victor
  • 1 Koutny, Maciej
  • Show More...

  • Refine by Classification
  • 1 Computer systems organization → Dependable and fault-tolerant systems and networks
  • 1 Mathematics of computing → Graph algorithms
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Distributed algorithms
  • 1 Theory of computation → Fixed parameter tractability
  • Show More...

  • Refine by Keyword
  • 1 Algorand
  • 1 Blockchain
  • 1 Burst automata
  • 1 Charging station placement
  • 1 Consensus
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 3 2023
  • 1 2016
  • 1 2022

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