In this paper we discuss reachability analysis for infinite-state systems. Infinite-state systems are formalized using transition systems over a first-order structure. We establish a common ground relating a large class of algorithms by analyzing the connections between the symbolic representation of transition systems and formulas used in various reachability algorithms. Our main results are related to the so-called guarded assignment systems. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Rybina, T., & Voronkov, A. (2003). A logical reconstruction of reachability. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2890, 222–237. https://doi.org/10.1007/978-3-540-39866-0_24
Mendeley helps you to discover research relevant for your work.