2000/08/22 by G. Senizergues, Géraud Sénizergues, Senizergues, G.
Computer Science · #Discrete Mathematics (cs.DM) #F.1.1 #F.4.2 #F.4.3 #FOS: Computer and information sciences #Formal Methods in Verification #G.2.2 #Logic in Computer Science (cs.LO) #Polynomial and algebraic computation #cs.DM #cs.LO #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.cs/0008018
98 pages, 4 figures, submitted to JACM
arxiv created 2000/08/22 · openalex publication_date 2000/08/22 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The "bisimulation problem" for equational graphs of finite out-degree is shown to be decidable. We reduce this problem to the bisimulation problem for deterministic rational (vectors of) boolean series on the alphabet of a dpda M. We then exhibit a complete formal system for deducing equivalent pairs of such vectors.