Abstract
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 reachability analysis based on the concept of abstract interpretation. The new algorithm may terminate in cases where the original algorithm diverges.
This work was partially supported by ESPRIT Basic Research Action “SPEC”
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
A. Bouajjani, S. Bensalem, C. Loiseaux, and J. Sifakis. Property preserving simulations. In Workshop on Computer-Aided Verification (CAV), Montréal, page, To appear LNCS, June 1992.
J.R. Burch, E.M. Clarke, K.L McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th IEEE,LICS, 1990.
A. Bouali and R. de Simone. Symbolic bisimulation minimisation. In Fourth Workshop on Computer-Aided Verification,Montreal, june 1992.
A. Bouajjani, J.C. Fernandez, and N. Halbwachs. Minimal model generation. In Workshop on Computer-aided Verification, Rutgers, American Mathematical Society, Association for Computing Machinery, June 1990.
A. Bouajjani, J.C. Fernandez, N. Halbwachs, C. Ratel, and P. Raymond. Minimal state graph generation. Science of Computer Programming, 18(3), June 1992.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.
O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In International Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, Springer Verlag, 1989.
P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In 2th Int. Symp. on Programming, pages 106, 130, Dunod, 1976.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th POPL, January 1977.
P. Cousot and R. Cousot. Comparing the Galois Connectionn and Widening/Narrowing Approaches to Abstract Interpretation. Technical Report, LIX, Ecole Polytechnique, May 1990.
P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5th. Annual Symp. on Principles of Programming Languages, pages 84–87, 1977.
P. Cousot. Semantic Foundations of Program Analysis, chapter 10. Prentice Hall, Inc., Englewood Cliffs, 1981.
R. Enders, T. Filkorn, and D. Taubner. Generating bdds for symbolic model checking in ccs. In K. G. Larsen, editor, Proceedings of the 3rd Workshop on Computer-Aided Verification (Aalborg, Denmark), july 1–4 1991.
J. C. Fernandez. An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13(2–3), May 1990.
J. Cl. Fernandez, A. Kerbrat, and L. Mounier. Symbolic equivalence checking. In Workshop on Computer-aided Verification, University of Crete, to appear, July 1993.
J.Cl. Fernandez and L. Mounier. A tool set for deciding behavioural equivalences. In J.F. Groote J.C.M. Baeten, editor, CONCUR'91, Concurrency theory, LNCS 527, Springer Verlag, August 26–29 1991.
R.J. Van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). CS-R 8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989.
N. Halbwachs. Détermination Automatique de Relations Linéaires Vérifiées par les Variables d'un Programme. PhD thesis, Université de Grenoble, 1979.
N. Halbwachs, P. Raymond, and C. Ratel. Generating efficient code from dataflow programs. In Third International Symposium on Programming Language Implementation and Logic Programming, Passau, August 1991.
P. Kanellakis and S. Smolka. Ccs expressions, finite state processes and three problems of equivalence. Information and Computation, 86(1), May 1990.
R. Milner. A calculus of communication systems. In LNCS 92, Springer Verlag, 1980.
D. Park. Concurrency and automata on infinite sequences. In 5th GI-Conference on Theorical Computer Science, Springer Verlag, 1981. LNCS 104.
Luis E. Sanchis. Data types as lattices: retractions, projection and projection. In RAIRO Theorical computer science, vol 11, nr 4, pages 339–344, 1977.
J. Sifakis. A unified approach for studying the properties of transition systems. TCS, 18, 1982.
J. Sifakis. Property preserving homomorphisms of transition systems. In 4th Workshop on Logics of Programs, Pittsburgh, LNCS 164, Springer Verlag, June 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fernandez, J.C. (1993). Abstract interpretation and verification of reactive systems. In: Cousot, P., Falaschi, M., Filé, G., Rauzy, A. (eds) Static Analysis. WSA 1993. Lecture Notes in Computer Science, vol 724. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57264-3_29
Download citation
DOI: https://doi.org/10.1007/3-540-57264-3_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57264-0
Online ISBN: 978-3-540-48027-3
eBook Packages: Springer Book Archive