This paper presents a variant of a refined partition algorithm, which exploits the irrelevance of unreachable states. When the state space is infinite, the number of accessible classes may be finite and the number of inaccessible classes infinite. The underlying idea is to incorporate a teachability analysis based on the concept of abstract interpretation. The new algoritlm, may terminate in cases where the original algoritlnn diverges.
CITATION STYLE
Fernandez, J. C. (1993). Abstract interpretation and verification of reactive systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 724 LNCS, pp. 60–71). Springer Verlag. https://doi.org/10.1007/3-540-57264-3_29
Mendeley helps you to discover research relevant for your work.