notesum.ai

Published at November 26

Weakly acyclic diagrams: A data structure for infinite-state symbolic verification

cs.LO

cs.DS

F.4.3; E.1

Released Date: November 26, 2024

Authors: Michael Blondin¹, Michaël Cadilhac², Xin-Yi Cui³, Philipp Czerner³, Javier Esparza³, Jakob Schulz³

Aff.: ¹Université de Sherbrooke, Canada; ²DePaul University, Chicago, USA; ³Technical University of Munich, Germany

Arxiv: http://arxiv.org/abs/2411.17250v1

identifier	succ. tuple			flag
	$a$	$b$	$c$
$q_{4}$	$q_{2}$	$q_{\Sigma^{*}}$	$q_{\Sigma^{*}}$	$0$
$q_{3}$	self	$q_{2}$	$q_{\emptyset}$	$1$
$q_{2}$	$q_{\Sigma^{*}}$	self	$q_{\emptyset}$	$0$
$q_{\Sigma^{*}}$	self	self	self	$1$
$q_{\emptyset}$	self	self	self	$0$