17 Search Results for "Pérez, Guillermo A."


Volume

LIPIcs, Volume 279

34th International Conference on Concurrency Theory (CONCUR 2023)

CONCUR 2023, September 18-23, 2023, Antwerp, Belgium

Editors: Guillermo A. Pérez and Jean-François Raskin

Document
The Futures of Reactive Synthesis (Dagstuhl Seminar 23391)

Authors: Nathanaël Fijalkow, Bernd Finkbeiner, Guillermo A. Pérez, Elizabeth Polgreen, and Rémi Morvan

Published in: Dagstuhl Reports, Volume 13, Issue 9 (2024)


Abstract
The Dagstuhl Seminar 23391 "The Futures of Reactive Synthesis" held in September 2023 was meant to gather neighbouring communities on a joint goal: Reactive Synthesis. We identified five trends: neural-symbolic computation, template-based solving for constraint programming, symbolic algorithms, syntax-guided synthesis, and model learning; and the objective was to discuss the potential futures of the field.

Cite as

Nathanaël Fijalkow, Bernd Finkbeiner, Guillermo A. Pérez, Elizabeth Polgreen, and Rémi Morvan. The Futures of Reactive Synthesis (Dagstuhl Seminar 23391). In Dagstuhl Reports, Volume 13, Issue 9, pp. 166-184, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@Article{fijalkow_et_al:DagRep.13.9.166,
  author =	{Fijalkow, Nathana\"{e}l and Finkbeiner, Bernd and P\'{e}rez, Guillermo A. and Polgreen, Elizabeth and Morvan, R\'{e}mi},
  title =	{{The Futures of Reactive Synthesis (Dagstuhl Seminar 23391)}},
  pages =	{166--184},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{9},
  editor =	{Fijalkow, Nathana\"{e}l and Finkbeiner, Bernd and P\'{e}rez, Guillermo A. and Polgreen, Elizabeth and Morvan, R\'{e}mi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.9.166},
  URN =		{urn:nbn:de:0030-drops-198259},
  doi =		{10.4230/DagRep.13.9.166},
  annote =	{Keywords: program synthesis, program verification, reactive synthesis, temporal synthesis}
}
Document
Complete Volume
LIPIcs, Volume 279, CONCUR 2023, Complete Volume

Authors: Guillermo A. Pérez and Jean-François Raskin

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


Abstract
LIPIcs, Volume 279, CONCUR 2023, Complete Volume

Cite as

34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 1-666, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@Proceedings{perez_et_al:LIPIcs.CONCUR.2023,
  title =	{{LIPIcs, Volume 279, CONCUR 2023, Complete Volume}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{1--666},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023},
  URN =		{urn:nbn:de:0030-drops-189936},
  doi =		{10.4230/LIPIcs.CONCUR.2023},
  annote =	{Keywords: LIPIcs, Volume 279, CONCUR 2023, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Guillermo A. Pérez and Jean-François Raskin

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{perez_et_al:LIPIcs.CONCUR.2023.0,
  author =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.0},
  URN =		{urn:nbn:de:0030-drops-189942},
  doi =		{10.4230/LIPIcs.CONCUR.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
CONCUR Test-Of-Time Award 2023 (Invited Paper)

Authors: Bengt Jonsson, Marta Kwiatkowska, and Igor Walukiewicz

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


Abstract
This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the paper that received the Award in 2023.

Cite as

Bengt Jonsson, Marta Kwiatkowska, and Igor Walukiewicz. CONCUR Test-Of-Time Award 2023 (Invited Paper). In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{jonsson_et_al:LIPIcs.CONCUR.2023.1,
  author =	{Jonsson, Bengt and Kwiatkowska, Marta and Walukiewicz, Igor},
  title =	{{CONCUR Test-Of-Time Award 2023}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.1},
  URN =		{urn:nbn:de:0030-drops-189953},
  doi =		{10.4230/LIPIcs.CONCUR.2023.1},
  annote =	{Keywords: CONCUR Test-of-Time Award}
}
Document
The Geometry of Reachability in Continuous Vector Addition Systems with States

Authors: Shaull Almagor, Arka Ghosh, Tim Leys, and Guillermo A. Pérez

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)


Abstract
We study the geometry of reachability sets of continuous vector addition systems with states (VASS). In particular we establish that they are "almost" Minkowski sums of convex cones and zonotopes generated by the vectors labelling the transitions of the VASS. We use the latter to prove that short so-called linear path schemes suffice as witnesses of reachability in continuous VASS. Then, we give new polynomial-time algorithms for the reachability problem for linear path schemes. Finally, we also establish that enriching the model with zero tests makes the reachability problem intractable already for linear path schemes of dimension two.

Cite as

Shaull Almagor, Arka Ghosh, Tim Leys, and Guillermo A. Pérez. The Geometry of Reachability in Continuous Vector Addition Systems with States. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 11:1-11:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.MFCS.2023.11,
  author =	{Almagor, Shaull and Ghosh, Arka and Leys, Tim and P\'{e}rez, Guillermo A.},
  title =	{{The Geometry of Reachability in Continuous Vector Addition Systems with States}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{11:1--11:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.11},
  URN =		{urn:nbn:de:0030-drops-185457},
  doi =		{10.4230/LIPIcs.MFCS.2023.11},
  annote =	{Keywords: Vector addition system with states, reachability, continuous approximation}
}
Document
Parikh One-Counter Automata

Authors: Michaël Cadilhac, Arka Ghosh, Guillermo A. Pérez, and Ritam Raha

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)


Abstract
Counting abilities in finite automata are traditionally provided by two orthogonal extensions: adding a single counter that can be tested for zeroness at any point, or adding ℤ-valued counters that are tested for equality only at the end of runs. In this paper, finite automata extended with both types of counters are introduced. They are called Parikh One-Counter Automata (POCA): the "Parikh" part referring to the evaluation of counters at the end of runs, and the "One-Counter" part to the single counter that can be tested during runs. Their expressiveness, in the deterministic and nondeterministic variants, is investigated; it is shown in particular that there are deterministic POCA languages that cannot be expressed without nondeterminism in the original models. The natural decision problems are also studied; strikingly, most of them are no harder than in the original models. A parametric version of nonemptiness is also considered.

Cite as

Michaël Cadilhac, Arka Ghosh, Guillermo A. Pérez, and Ritam Raha. Parikh One-Counter Automata. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 30:1-30:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{cadilhac_et_al:LIPIcs.MFCS.2023.30,
  author =	{Cadilhac, Micha\"{e}l and Ghosh, Arka and P\'{e}rez, Guillermo A. and Raha, Ritam},
  title =	{{Parikh One-Counter Automata}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{30:1--30:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.30},
  URN =		{urn:nbn:de:0030-drops-185645},
  doi =		{10.4230/LIPIcs.MFCS.2023.30},
  annote =	{Keywords: Parikh automata, Context-free languages, One-counter automata}
}
Document
Revisiting Parameter Synthesis for One-Counter Automata

Authors: Guillermo A. Pérez and Ritam Raha

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)


Abstract
We study the synthesis problem for one-counter automata with parameters. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The synthesis problem for such automata asks whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some ω-regular property. Lechner showed that (the complement of) the problem can be encoded in a restricted one-alternation fragment of Presburger arithmetic with divisibility. In this work (i) we argue that said fragment, called ∀∃_RPAD^+, is unfortunately undecidable. Nevertheless, by a careful re-encoding of the problem into a decidable restriction of ∀∃_RPAD^+, (ii) we prove that the synthesis problem is decidable in general and in 2NEXP for several fixed ω-regular properties. Finally, (iii) we give polynomial-space algorithms for the special cases of the problem where parameters can only be used in counter tests.

Cite as

Guillermo A. Pérez and Ritam Raha. Revisiting Parameter Synthesis for One-Counter Automata. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{perez_et_al:LIPIcs.CSL.2022.33,
  author =	{P\'{e}rez, Guillermo A. and Raha, Ritam},
  title =	{{Revisiting Parameter Synthesis for One-Counter Automata}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{33:1--33:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.33},
  URN =		{urn:nbn:de:0030-drops-157534},
  doi =		{10.4230/LIPIcs.CSL.2022.33},
  annote =	{Keywords: Parametric one-counter automata, Reachability, Software Verification}
}
Document
Coverability in 1-VASS with Disequality Tests

Authors: Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model of vector addition systems with states (VASS). We consider a version of the vertex-to-vertex reachability problem in which the accumulated weight of a path is required always to be non-negative. This is equivalent to the so-called control-state reachability problem (also called the coverability problem) for 1-dimensional VASS. We show that this problem lies in NC: the class of problems solvable in polylogarithmic parallel time. In our main result we generalise the problem to allow disequality constraints on edges (i.e., we allow edges to be disabled if the accumulated weight is equal to a specific value). We show that in this case the vertex-to-vertex reachability problem is solvable in polynomial time even though a shortest path may have exponential length. In the language of VASS this means that control-state reachability is in polynomial time for 1-dimensional VASS with disequality tests.

Cite as

Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell. Coverability in 1-VASS with Disequality Tests. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2020.38,
  author =	{Almagor, Shaull and Cohen, Nathann and P\'{e}rez, Guillermo A. and Shirmohammadi, Mahsa and Worrell, James},
  title =	{{Coverability in 1-VASS with Disequality Tests}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{38:1--38:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.38},
  URN =		{urn:nbn:de:0030-drops-128501},
  doi =		{10.4230/LIPIcs.CONCUR.2020.38},
  annote =	{Keywords: Reachability, Vector addition systems with states, Weighted graphs}
}
Document
On the Complexity of Reachability in Parametric Markov Decision Processes

Authors: Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, and Joost-Pieter Katoen

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


Abstract
This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. Fixing values for all parameters yields MDPs. In particular, this paper studies the complexity of finding values for these parameters such that the induced MDP satisfies some reachability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably provide ETR-completeness results for distinct variants of this problem. Furthermore, we provide insights in the functions describing the induced reachability probabilities, and how pMDPs generalise concurrent stochastic reachability games.

Cite as

Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, and Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{winkler_et_al:LIPIcs.CONCUR.2019.14,
  author =	{Winkler, Tobias and Junges, Sebastian and P\'{e}rez, Guillermo A. and Katoen, Joost-Pieter},
  title =	{{On the Complexity of Reachability in Parametric Markov Decision Processes}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{14:1--14:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.14},
  URN =		{urn:nbn:de:0030-drops-109162},
  doi =		{10.4230/LIPIcs.CONCUR.2019.14},
  annote =	{Keywords: Parametric Markov decision processes, Formal verification, ETR, Complexity}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
On the Complexity of Value Iteration (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Nikhil Balaji, Stefan Kiefer, Petr Novotný, Guillermo A. Pérez, and Mahsa Shirmohammadi

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)


Abstract
Value iteration is a fundamental algorithm for solving Markov Decision Processes (MDPs). It computes the maximal n-step payoff by iterating n times a recurrence equation which is naturally associated to the MDP. At the same time, value iteration provides a policy for the MDP that is optimal on a given finite horizon n. In this paper, we settle the computational complexity of value iteration. We show that, given a horizon n in binary and an MDP, computing an optimal policy is EXPTIME-complete, thus resolving an open problem that goes back to the seminal 1987 paper on the complexity of MDPs by Papadimitriou and Tsitsiklis. To obtain this main result, we develop several stepping stones that yield results of an independent interest. For instance, we show that it is EXPTIME-complete to compute the n-fold iteration (with n in binary) of a function given by a straight-line program over the integers with max and + as operators. We also provide new complexity results for the bounded halting problem in linear-update counter machines.

Cite as

Nikhil Balaji, Stefan Kiefer, Petr Novotný, Guillermo A. Pérez, and Mahsa Shirmohammadi. On the Complexity of Value Iteration (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 102:1-102:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{balaji_et_al:LIPIcs.ICALP.2019.102,
  author =	{Balaji, Nikhil and Kiefer, Stefan and Novotn\'{y}, Petr and P\'{e}rez, Guillermo A. and Shirmohammadi, Mahsa},
  title =	{{On the Complexity of Value Iteration}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{102:1--102:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.102},
  URN =		{urn:nbn:de:0030-drops-106782},
  doi =		{10.4230/LIPIcs.ICALP.2019.102},
  annote =	{Keywords: Markov decision processes, Value iteration, Formal verification}
}
Document
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints

Authors: Jan Kretínský, Guillermo A. Pérez, and Jean-François Raskin

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


Abstract
We formalize the problem of maximizing the mean-payoff value with high probability while satisfying a parity objective in a Markov decision process (MDP) with unknown probabilistic transition function and unknown reward function. Assuming the support of the unknown transition function and a lower bound on the minimal transition probability are known in advance, we show that in MDPs consisting of a single end component, two combinations of guarantees on the parity and mean-payoff objectives can be achieved depending on how much memory one is willing to use. (i) For all epsilon and gamma we can construct an online-learning finite-memory strategy that almost-surely satisfies the parity objective and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma. (ii) Alternatively, for all epsilon and gamma there exists an online-learning infinite-memory strategy that satisfies the parity objective surely and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma. We extend the above results to MDPs consisting of more than one end component in a natural way. Finally, we show that the aforementioned guarantees are tight, i.e. there are MDPs for which stronger combinations of the guarantees cannot be ensured.

Cite as

Jan Kretínský, Guillermo A. Pérez, and Jean-François Raskin. Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2018.8,
  author =	{Kret{\'\i}nsk\'{y}, Jan and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.8},
  URN =		{urn:nbn:de:0030-drops-95468},
  doi =		{10.4230/LIPIcs.CONCUR.2018.8},
  annote =	{Keywords: Markov decision processes, Reinforcement learning, Beyond worst case}
}
Document
When is Containment Decidable for Probabilistic Automata?

Authors: Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, and James Worrell

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)


Abstract
The containment problem for quantitative automata is the natural quantitative generalisation of the classical language inclusion problem for Boolean automata. We study it for probabilistic automata, where it is known to be undecidable in general. We restrict our study to the class of probabilistic automata with bounded ambiguity. There, we show decidability (subject to Schanuel's conjecture) when one of the automata is assumed to be unambiguous while the other one is allowed to be finitely ambiguous. Furthermore, we show that this is close to the most general decidable fragment of this problem by proving that it is already undecidable if one of the automata is allowed to be linearly ambiguous.

Cite as

Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, and James Worrell. When is Containment Decidable for Probabilistic Automata?. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 121:1-121:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{daviaud_et_al:LIPIcs.ICALP.2018.121,
  author =	{Daviaud, Laure and Jurdzinski, Marcin and Lazic, Ranko and Mazowiecki, Filip and P\'{e}rez, Guillermo A. and Worrell, James},
  title =	{{When is Containment Decidable for Probabilistic Automata?}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{121:1--121:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.121},
  URN =		{urn:nbn:de:0030-drops-91251},
  doi =		{10.4230/LIPIcs.ICALP.2018.121},
  annote =	{Keywords: Probabilistic automata, Containment, Emptiness, Ambiguity}
}
Document
Admissibility in Quantitative Graph Games

Authors: Romain Brenguier, Guillermo A. Pérez, Jean-Francois Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
Admissibility has been studied for games of infinite duration with Boolean objectives. We extend here this study to games of infinite duration with quantitative objectives. First, we show that, under the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the notion of adversarial and cooperative values of a history, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterizations can be used to design algorithms to decide relevant verification and synthesis problems.

Cite as

Romain Brenguier, Guillermo A. Pérez, Jean-Francois Raskin, and Ocan Sankur. Admissibility in Quantitative Graph Games. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 42:1-42:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{brenguier_et_al:LIPIcs.FSTTCS.2016.42,
  author =	{Brenguier, Romain and P\'{e}rez, Guillermo A. and Raskin, Jean-Francois and Sankur, Ocan},
  title =	{{Admissibility in Quantitative Graph Games}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{42:1--42:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.42},
  URN =		{urn:nbn:de:0030-drops-68772},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.42},
  annote =	{Keywords: Quantitative games, Verification, Reactive synthesis, Admissibility}
}
Document
Minimizing Regret in Discounted-Sum Games

Authors: Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)


Abstract
In this paper, we study the problem of minimizing regret in discounted-sum games played on weighted game graphs. We give algorithms for the general problem of computing the minimal regret of the controller (Eve) as well as several variants depending on which strategies the environment (Adam) is permitted to use. We also consider the problem of synthesizing regret-free strategies for Eve in each of these scenarios.

Cite as

Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Minimizing Regret in Discounted-Sum Games. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{hunter_et_al:LIPIcs.CSL.2016.30,
  author =	{Hunter, Paul and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Minimizing Regret in Discounted-Sum Games}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{30:1--30:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.30},
  URN =		{urn:nbn:de:0030-drops-65704},
  doi =		{10.4230/LIPIcs.CSL.2016.30},
  annote =	{Keywords: Quantitative games, Regret, Verification, Synthesis, Game theory}
}
  • Refine by Author
  • 15 Pérez, Guillermo A.
  • 5 Raskin, Jean-François
  • 2 Almagor, Shaull
  • 2 Ghosh, Arka
  • 2 Hunter, Paul
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Logic and verification
  • 4 Theory of computation → Concurrency
  • 3 Theory of computation → Probabilistic computation
  • 2 Theory of computation → Markov decision processes
  • 2 Theory of computation → Quantitative automata
  • Show More...

  • Refine by Keyword
  • 4 Quantitative games
  • 2 Formal verification
  • 2 Markov decision processes
  • 2 Reachability
  • 2 Verification
  • Show More...

  • Refine by Type
  • 16 document
  • 1 volume

  • Refine by Publication Year
  • 6 2023
  • 2 2015
  • 2 2016
  • 2 2018
  • 2 2019
  • Show More...

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