4 papers
A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
Kyveli Doveri, Pierre Ganty, B. Srivathsan
We present a Myhill-Nerode style characterization for languages recognized by one-clock deterministic timed automata (1-DTA). Although there is only one clock, distinct automata ma…
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…
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…