We present the first machine-checked formalization of Jaffe and Ehrenfeucht, Parikh and Rozenberg’s (EPR) pumping lemmas in the Coq proof assistant. We formulate regularity in terms of finite derivatives, and prove that both Jaffe’s pumping property and EPR’s block pumping property precisely characterize regularity. We illuminate EPR’s classical proof that the block cancellation property implies regularity, and discover that—as best we can tell—their proof relies on the Axiom of Choice. We provide a new proof which eliminates the use of Choice. We explicitly construct an function which computes block cancelable languages from well-formed short languages.
Wed 4 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
Wed 4 Dec
Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
10:30 - 12:00 | Logic and AutomataResearch Papers at Bali Room Chair(s): Peter Thiemann University of Freiburg, Germany | ||
10:30 30mTalk | Pumping, With or Without Choice Research Papers Aquinas Hobor National University of Singapore, Singapore, Elaine Li Runtime Verification, Inc., Frank Stephan National University of Singapore | ||
11:00 30mTalk | Simulations in Rank-Based Buchi Automata Complementation Research Papers Yu-Fang Chen Academia Sinica, Vojtěch Havlena Brno University of Technology, Ondřej Lengál Brno University of Technology | ||
11:30 30mTalk | Succinct Determinisation of Counting Automata via Sphere Construction Research Papers Lukáš Holík Brno University of Technology, Tomáš Vojnar Brno University of Technology, Ondřej Lengál Brno University of Technology , Lenka Turoňová Brno University of Technology, Margus Veanes Microsoft Research, Olli Saarikivi | ||