85 citations · 262 across the 21 of their papers we have counts for
18 papers · 1 filter
A Myhill-Nerode style Characterization for Timed Automata With Integer Resets
Kyveli Doveri, Pierre Ganty, B. Srivathsan
The well-known Nerode equivalence for finite words plays a fundamental role in our understanding of the class of regular languages. The equivalence leads to the Myhill-Nerode theor…
A Uniform Framework for Language Inclusion Problems
Kyveli Doveri, Pierre Ganty, Chana Weil-Kennedy
We present a uniform approach for solving language inclusion problems. Our approach relies on a least fixpoint characterization and a quasiorder to compare words of the "smaller" l…
Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification
Pierre Ganty, Dario Della Monica
This volume contains the proceedings of the 13th International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2022). The aim of GandALF 2022 symposium is to b…
FORQ-based Language Inclusion Formal Testing
Kyveli Doveri, Pierre Ganty, Nicolas Mazzocchi
We propose a novel algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage a not…
Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification
Pierre Ganty, Davide Bresolin
This volume contains the proceedings of the 12th International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2021). The aim of GandALF 2021 symposium is to b…
A Congruence-Based Perspective on Finite Tree Automata
Pierre Ganty, Elena Gutiérrez, Pedro Valero
We provide new insights on the determinization and minimization of tree automata using congruences on trees. From this perspective, we study a Brzozowski's style minimization algor…
A Quasiorder-based Perspective on Residual Automata
Pierre Ganty, Elena Gutiérrez, Pedro Valero
In this work, we define a framework of automata constructions based on quasiorders over words to provide new insights on the class of residual automata. We present a new residualiz…
A Congruence-based Perspective on Automata Minimization Algorithms
Pierre Ganty, Elena Gutiérrez, Pedro Valero
In this work we use a framework of finite-state automata constructions based on equivalences over words to provide new insights on the relation between well-known methods for compu…
Complete Abstractions for Checking Language Inclusion
Pierre Ganty, Francesco Ranzato, Pedro Valero
We study the language inclusion problem where is regular or context-free. Our approach relies on abstract interpretation and checks whether an overapproxi…
Regular Expression Search on Compressed Text
Pierre Ganty, Pedro Valero
We present an algorithm for searching regular expression matches in compressed text. The algorithm reports the number of matching lines in the uncompressed text in time linear in t…
The Parikh Property for Weighted Context-Free Grammars
Pierre Ganty, Elena Gutiérrez
Parikh's Theorem states that every context-free grammar (CFG) is equivalent to some regular CFG when the ordering of symbols in the words is ignored. The same is not true for the s…
Parikh Image of Pushdown Automata
Pierre Ganty, Elena Gutiérrez
We compare pushdown automata (PDAs for short) against other representations. First, we show that there is a family of PDAs over a unary alphabet with states and …
A Language-theoretic View on Network Protocols
Pierre Ganty, Boris Köpf, Pedro Valero
Input validation is the first line of defense against malformed or malicious inputs. It is therefore critical that the validator (which is often part of the parser) is free of bugs…
Bounded-oscillation Pushdown Automata
Pierre Ganty, Damir Valput
We present an underapproximation for context-free languages by filtering out runs of the underlying pushdown automaton depending on how the stack height evolves over time. In parti…
Interprocedural Reachability for Flat Integer Programs
Pierre Ganty, Radu Iosif
We study programs with integer data, procedure calls and arbitrary call graphs. We show that, whenever the guards and updates are given by octagonal relations, the reachability pro…
A Perfect Model for Bounded Verification
Javier Esparza, Pierre Ganty, Rupak Majumdar
A class of languages C is perfect if it is closed under Boolean operations and the emptiness problem is decidable. Perfect language classes are the basis for the automata-theoretic…
Approximating Petri Net Reachability Along Context-free Traces
Mohamed Faouzi Atig, Pierre Ganty
We investigate the problem asking whether the intersection of a context-free language (CFL) and a Petri net language (PNL) is empty. Our contribution to solve this long-standing pr…
Parikh's Theorem: A simple and direct automaton construction
Javier Esparza, Pierre Ganty, Stefan Kiefer +1
Parikh's theorem states that the Parikh image of a context-free language is semilinear or, equivalently, that every context-free language has the same Parikh image as some regular…