Abstract
The model checking of a counters system S often reduces to the effective computation of the set of predecessors Pre*S(X) of a set of integer vectors X. Because the exact computation of this set is not possible in general, we are interested in characterizing the minimal Number Decision Diagrams (NDD) [WB00] that represents the set Pre≤k(X). In particular, its size is proved to be just polynomially bounded in k when S is a counters system with a finite monoïd [FL02], explaining why there is no exponential blow up in k. © Springer-Verlag Berlin Heidelberg 2004.
Cite
CITATION STYLE
Finkel, A., & Leroux, J. (2004). Image computation in infinite state model checking. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3114, 361–371. https://doi.org/10.1007/978-3-540-27813-9_28
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
