In this paper we present algorithms for efficient image computation for systems represented as arithmetic constraints. We use automata as a symbolic representation for such systems. We show that, for a common class of systems, given a set of states and a transition, the time required for image computation is bounded by the product of the sizes of the automata encoding the input set and the transition. We also show that the size of the result has the same bound. We obtain these results using a linear time projection operation for automata encoding linear arithmetic constraints. We also experimentally show the benefits of using these algorithms by comparing our implementation with LASH and BRAIN. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Bartzis, C., & Bultan, T. (2003). Efficient image computation in infinite state model checking. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2725, 249–261. https://doi.org/10.1007/978-3-540-45069-6_26
Mendeley helps you to discover research relevant for your work.