A method-based ahead-of-time compiler for android applications. - Chih-Sheng Wang; Guillermo A. Pérez 001; Yeh-Ching Chung; Wei-Chung Hsu; Wei-Kuan Shih; Hong-Rong Hsu (CASES, 2011)

A hybrid just-in-time compiler for android: comparing JIT types and the result of cooperation. - Guillermo A. Pérez 001; Chung-Min Kao; Yeh-Ching Chung; Wei-Chung Hsu (CASES, 2012)

Mean-payoff Games with Incomplete Information. - Paul Hunter 001; Guillermo A. Pérez 001; Jean-François Raskin (CoRR, 2013)

Mean-Payoff Games with Partial-Observation - (Extended Abstract). - Paul Hunter 001; Guillermo A. Pérez 001; Jean-François Raskin (RP, 2014)

AbsSynthe: abstract synthesis from succinct safety specifications. - Romain Brenguier; Guillermo A. Pérez 001; Jean-François Raskin; Ocan Sankur (SYNT, 2014)

Quantitative Games under Failures. - Thomas Brihaye; Gilles Geeraerts; Axel Haddad; Benjamin Monmege; Guillermo A. Pérez 001; Gabriel Renault (FSTTCS, 2015)

Compositional Algorithms for Succinct Safety Games. - Romain Brenguier; Guillermo A. Pérez 001; Jean-François Raskin; Ocan Sankur (SYNT, 2015)

The Second Reactive Synthesis Competition (SYNTCOMP 2015). - Swen Jacobs; Roderick Bloem; Romain Brenguier; Robert Könighofer; Guillermo A. Pérez 001; Jean-François Raskin; Leonid Ryzhyk; Ocan Sankur; Martina Seidl; Leander Tentrup; Adam Walker (SYNT, 2015)

The fixed initial credit problem for energy games with partial-observation is Ackermann-complete. - Guillermo A. Pérez 001 (CoRR, 2015)

Minimizing Regret in Discounted-Sum Games. - Paul Hunter 001; Guillermo A. Pérez 001; Jean-François Raskin (CSL, 2016)

Admissibility in Quantitative Graph Games. - Romain Brenguier; Guillermo A. Pérez 001; Jean-François Raskin; Ocan Sankur (FSTTCS, 2016)

Non-Zero Sum Games for Reactive Synthesis. - Romain Brenguier; Lorenzo Clemente; Paul Hunter 001; Guillermo A. Pérez 001; Mickael Randour; Jean-François Raskin; Ocan Sankur; Mathieu Sassolas (LATA, 2016)

Optimizing Expectation with Guarantees in POMDPs (Technical Report). - Krishnendu Chatterjee; Petr Novotný 001; Guillermo A. Pérez 001; Jean-François Raskin; Dorde Zikelic (CoRR, 2016)

The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results. - Swen Jacobs; Roderick Bloem; Romain Brenguier; Ayrat Khalimov 001; Felix Klein 001; Robert Könighofer; Jens Kreber; Alexander Legg; Nina Narodytska; Guillermo A. Pérez 001; Jean-François Raskin; Leonid Ryzhyk; et al. (SYNT@CAV, 2016)

Optimizing Expectation with Guarantees in POMDPs. - Krishnendu Chatterjee; Petr Novotný 001; Guillermo A. Pérez 001; Jean-François Raskin; Dorde Zikelic (AAAI, 2017)

Reduction Techniques for Model Checking and Learning in MDPs. - Suda Bharadwaj; Stéphane Le Roux 001; Guillermo A. Pérez 001; Ufuk Topcu (IJCAI, 2017)

On delay and regret determinization of max-plus automata. - Emmanuel Filiot; Ismaël Jecker; Nathan Lhote; Guillermo A. Pérez 001; Jean-François Raskin (LICS, 2017)

Reactive synthesis without regret. - Paul Hunter 001; Guillermo A. Pérez 001; Jean-François Raskin (Acta Informatica, 2017)

The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results. - Swen Jacobs; Nicolas Basset; Roderick Bloem; Romain Brenguier; Maximilien Colange; Peter Faymonville; Bernd Finkbeiner; Ayrat Khalimov 001; Felix Klein 001; Thibaud Michaud; Guillermo A. Pérez 001; Jean-François Raskin; et al. (SYNT@CAV, 2017)

The fixed initial credit problem for partial-observation energy games is Ack-complete. - Guillermo A. Pérez 001 (Inf. Process. Lett., 2017)

The first reactive synthesis competition (SYNTCOMP 2014). - Swen Jacobs; Roderick Bloem; Romain Brenguier; Rüdiger Ehlers; Timotheus Hell; Robert Könighofer; Guillermo A. Pérez 001; Jean-François Raskin; Leonid Ryzhyk; Ocan Sankur; Martina Seidl; Leander Tentrup; et al. (Int. J. Softw. Tools Technol. Transf., 2017)

Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints. - Jan Kretínský; Guillermo A. Pérez 001; Jean-François Raskin (CONCUR, 2018)

The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes. - Stéphane Le Roux 001; Guillermo A. Pérez 001 (FoSSaCS, 2018)

When is Containment Decidable for Probabilistic Automata?. - Laure Daviaud; Marcin Jurdzinski; Ranko Lazic 001; Filip Mazowiecki; Guillermo A. Pérez 001; James Worrell 001 (ICALP, 2018)

Looking at mean payoff through foggy windows. - Paul Hunter 001; Guillermo A. Pérez 001; Jean-François Raskin (Acta Informatica, 2018)

On the Complexity of Iterative Tropical Computation with Applications to Markov Decision Processes. - Nikhil Balaji; Stefan Kiefer; Petr Novotný 001; Guillermo A. Pérez 001; Mahsa Shirmohammadi (CoRR, 2018)

Mean-payoff games with partial observation. - Paul Hunter 001; Arno Pauly; Guillermo A. Pérez 001; Jean-François Raskin (Theor. Comput. Sci., 2018)

The Impatient May Use Limited Optimism to Minimize Regret. - Michaël Cadilhac; Guillermo A. Pérez 001; Marie van den Bogaard (FoSSaCS, 2019)

On the Complexity of Value Iteration. - Nikhil Balaji; Stefan Kiefer; Petr Novotný 001; Guillermo A. Pérez 001; Mahsa Shirmohammadi (ICALP, 2019)

Partial Solvers for Generalized Parity Games. - Véronique Bruyère; Guillermo A. Pérez 001; Jean-François Raskin; Clément Tamines (RP, 2019)

The Extended HOA Format for Synthesis. - Guillermo A. Pérez 001 (CoRR, 2019)

Robustness Verification for Classifier Ensembles. - Dennis Gross; Nils Jansen 001; Guillermo A. Pérez 001; Stephan Raaijmakers (ATVA, 2020)

Coverability in 1-VASS with Disequality Tests. - Shaull Almagor; Nathann Cohen; Guillermo A. Pérez 001; Mahsa Shirmohammadi; James Worrell 001 (CONCUR, 2020)

Finite-Memory Near-Optimal Learning for Markov Decision Processes with Long-Run Average Reward. - Jan Kretínský; Fabian Michel; Lukas Michel; Guillermo A. Pérez 001 (UAI, 2020)

Revisiting Synthesis for One-Counter Automata. - Guillermo A. Pérez 001; Ritam Raha (CoRR, 2020)

Safe Learning for Near Optimal Scheduling. - Gilles Geeraerts; Shibashis Guha; Guillermo A. Pérez 001; Jean-François Raskin (CoRR, 2020)

Adversarial Patch Camouflage against Aerial Detection. - Ajaya Adhikari; Richard den Hollander; Ioannis Tolios; Michael van Bekkum; Anneloes Bal; Stijn Hendriks; Maarten Kruithof; Dennis Gross; Nils Jansen 001; Guillermo A. Pérez 001; Kit Buurman; Stephan Raaijmakers (CoRR, 2020)

Airtime-Based Resource Allocation Modeling for Network Slicing in IEEE 802.11 RANs. - Pedro Heleno Isolani; Nelson Cardona; Carlos Donato; Guillermo A. Pérez 001; Johann M. Márquez-Barja; Lisandro Zambenedetti Granville; Steven Latré (IEEE Commun. Lett., 2020)

Weak Cost Register Automata are Still Powerful. - Shaull Almagor; Michaël Cadilhac; Filip Mazowiecki; Guillermo A. Pérez 001 (Int. J. Found. Comput. Sci., 2020)

Active Learning of Sequential Transducers with Side Information About the Domain. - Raphaël Berthon; Adrien Boiret; Guillermo A. Pérez 001; Jean-François Raskin (DLT, 2021)

Let's Agree to Degree: Comparing Graph Convolutional Networks in the Message-Passing Framework. - Floris Geerts; Filip Mazowiecki; Guillermo A. Pérez 001 (ICML, 2021)

Safe Learning for Near-Optimal Scheduling. - Damien Busatto-Gaston; Debraj Chakraborty 002; Shibashis Guha; Guillermo A. Pérez 001; Jean-François Raskin (QEST, 2021)

Lecture Notes on Partially Known MDPs. - Guillermo A. Pérez 001 (CoRR, 2021)

Distillation of RL Policies with Formal Guarantees via Variational Abstraction of Markov Decision Processes (Technical Report). - Florent Delgrange; Ann Nowé; Guillermo A. Pérez 001 (CoRR, 2021)

When are emptiness and containment decidable for probabilistic automata? - Laure Daviaud; Marcin Jurdzinski; Ranko Lazic 001; Filip Mazowiecki; Guillermo A. Pérez 001; James Worrell 001 (J. Comput. Syst. Sci., 2021)

The complexity of reachability in parametric Markov decision processes. - Sebastian Junges; Joost-Pieter Katoen; Guillermo A. Pérez 001; Tobias Winkler 001 (J. Comput. Syst. Sci., 2021)

Distillation of RL Policies with Formal Guarantees via Variational Abstraction of Markov Decision Processes. - Florent Delgrange; Ann Nowé; Guillermo A. Pérez 001 (AAAI, 2022)

Revisiting Parameter Synthesis for One-Counter Automata. - Guillermo A. Pérez 001; Ritam Raha (CSL, 2022)

COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking. - Dennis Gross; Nils Jansen 001; Sebastian Junges; Guillermo A. Pérez 001 (SETTA, 2022)

Learning Realtime One-Counter Automata. - Véronique Bruyère; Guillermo A. Pérez 001; Gaëtan Staquet (TACAS (1), 2022)

Correction to: Reactive synthesis without regret. - Paul Hunter 001; Guillermo A. Pérez 001; Jean-François Raskin (Acta Informatica, 2022)

Preface for the formal methods in system design special issue on SYNT 2021. - Elizabeth Polgreen; Guillermo Alberto Pérez (Formal Methods Syst. Des., 2022)

Model Checking for Adversarial Multi-Agent Reinforcement Learning with Reactive Defense Methods. - Dennis Gross; Christoph Schmidl; Nils Jansen 001; Guillermo A. Pérez 001 (ICAPS, 2023)

Formally-Sharp DAgger for MCTS: Lower-Latency Monte Carlo Tree Search using Data Aggregation with Formal Methods. - Debraj Chakraborty 002; Damien Busatto-Gaston; Jean-François Raskin; Guillermo A. Pérez 001 (AAMAS, 2023)

Bi-objective Lexicographic Optimization in Markov Decision Processes with Related Objectives. - Damien Busatto-Gaston; Debraj Chakraborty 002; Anirban Majumdar 002; Sayan Mukherjee 002; Guillermo A. Pérez 001; Jean-François Raskin (ATVA (1), 2023)

Graph-Based Reductions for Parametric and Weighted MDPs. - Kasper Engelen; Guillermo A. Pérez 001; Shrisha Rao 002 (ATVA (1), 2023)

Automata with Timers. - Véronique Bruyère; Guillermo A. Pérez 001; Gaëtan Staquet; Frits W. Vaandrager (FORMATS, 2023)

Targeted Adversarial Attacks on Deep Reinforcement Learning Policies via Model Checking. - Dennis Gross; Thiago D. Simão; Nils Jansen 001; Guillermo A. Pérez 001 (ICAART (3), 2023)

Wasserstein Auto-encoded MDPs: Formal Verification of Efficiently Distilled RL Policies with Many-sided Guarantees. - Florent Delgrange; Ann Nowé; Guillermo A. Pérez 001 (ICLR, 2023)

A Framework for the Competitive Analysis of Model Predictive Controllers. - Stijn Bellis; Joachim Denil; Ramesh Krishnamurthy; Tim Leys; Guillermo A. Pérez 001; Ritam Raha (RP, 2023)

Validating Streaming JSON Documents with Learned VPAs. - Véronique Bruyère; Guillermo A. Pérez 001; Gaëtan Staquet (TACAS (1), 2023)

Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability. - Michaël Cadilhac; Guillermo A. Pérez 001 (TACAS (2), 2023)

The Temporal Logic Synthesis Format TLSF v1.2. - Swen Jacobs; Guillermo A. Pérez 001; Philipp Schlehuber-Caissier (CoRR, 2023)

The Futures of Reactive Synthesis (Dagstuhl Seminar 23391). - Nathanaël Fijalkow; Bernd Finkbeiner; Guillermo A. Pérez 001; Elizabeth Polgreen; Rémi Morvan (Dagstuhl Reports, 2023)

Continuous One-counter Automata. - Michael Blondin; Tim Leys; Filip Mazowiecki; Philip Offtermatt; Guillermo A. Pérez 001 (ACM Trans. Comput. Log., 2023)

SLWM: A Library for Implementing Complex Training Workflows for surrogates of MPC's. - Stijn Bellis; Joachim Denil; Ramesh Krishnamurthy; Guillermo A. Pérez 001 (IEEE Big Data, 2024)

Analyzing Value Functions of States in Parametric Markov Chains. - Kasper Engelen; Guillermo A. Pérez 001; Shrisha Rao 002 (Principles of Verification (2), 2024)

Work-in-Progress: Worst-Case Execution-Time Measurement Techniques for Nonlinear Model Predictive Controllers. - Ramesh Krishnamurthy; Guillermo A. Pérez 001; Joachim Denil; Ward Goossens (CODES+ISSS, 2024)

On Continuous Pushdown VASS in One Dimension. - Guillermo A. Pérez 001; Shrisha Rao 002 (CONCUR, 2024)

The Wasserstein Believer: Learning Belief Updates for Partially Observable Environments through Reliable Latent Space Models. - Raphaël Avalos; Florent Delgrange; Ann Nowé; Guillermo A. Pérez 001; Diederik M. Roijers (ICLR, 2024)

Integer Programming with GCD Constraints. - Rémy Défossez; Christoph Haase; Alessio Mansutti; Guillermo A. Pérez 001 (SODA, 2024)

Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic. - Ritam Raha; Rajarshi Roy 002; Nathanaël Fijalkow; Daniel Neider; Guillermo A. Pérez 001 (VMCAI (2), 2024)

Inform: From Compartmental Models to Stochastic Bounded Counter Machines. - Tim Leys; Guillermo A. Pérez 001 (CoRR, 2024)

Continuous Pushdown VASS in One Dimension are Easy. - Guillermo A. Pérez 001; Shrisha Rao 002 (CoRR, 2024)

Synthesis of Hierarchical Controllers Based on Deep Reinforcement Learning Policies. - Florent Delgrange; Guy Avni; Anna Lukina; Christian Schilling 001; Ann Nowé; Guillermo A. Pérez 001 (CoRR, 2024)

Active Learning of Mealy Machines with Timers. - Véronique Bruyère; Bharat Garhewal; Guillermo A. Pérez 001; Gaëtan Staquet; Frits W. Vaandrager (CoRR, 2024)

The Reactive Synthesis Competition (SYNTCOMP): 2018-2021. - Swen Jacobs; Guillermo A. Pérez 001; Remco Abraham; Véronique Bruyère; Michaël Cadilhac; Maximilien Colange; Charly Delfosse; Tom van Dijk; Alexandre Duret-Lutz; Peter Faymonville; Bernd Finkbeiner; Ayrat Khalimov 001; et al. (Int. J. Softw. Tools Technol. Transf., 2024)

Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives. - Marius Belly; Nathanaël Fijalkow; Hugo Gimbert; Florian Horn 001; Guillermo A. Pérez 001; Pierre Vandenhove (AAAI, 2025)

Composing Reinforcement Learning Policies, with Formal Guarantees. - Florent Delgrange; Guy Avni; Anna Lukina; Christian Schilling 001; Ann Nowé; Guillermo A. Pérez 001 (AAMAS, 2025)

The geometry of reachability in continuous vector addition systems with states. - Shaull Almagor; Arka Ghosh 002; Tim Leys; Guillermo A. Pérez 001 (Inf. Comput., 2025)

Parikh one-counter automata. - Michaël Cadilhac; Arka Ghosh 002; Guillermo A. Pérez 001; Ritam Raha (Inf. Comput., 2025)

Algorithms for Markov Binomial Chains. - Alejandro Alarcón Gonzalez; Niel Hens; Tim Leys; Guillermo A. Pérez 001 (Log. Methods Comput. Sci., 2025)

Data Structures for Finite Downsets of Natural Vectors: Theory and Practice. - Michaël Cadilhac; Vanessa Flügel; Guillermo A. Pérez 001; Shrisha Rao 002 (CoRR, 2025)

Data-Efficient Safe Policy Improvement Using Parametric Structure. - Kasper Engelen; Guillermo A. Pérez 001; Marnix Suilen (CoRR, 2025)