Automated Verification of Infinite State Concurrent Systems
The paper shows how to use partitioning techniques to generate abstract state spaces (models) preserving similarity and injectivity. Since these relations are weaker than bisimilarity and surjectivity, our algorithms generate smaller models. This method can be applied for improving several existing partitioning algorithms used for generating finite models of concurrent programs, Time Petri Nets and Timed Automata.
Unable to display preview. Download preview PDF.
- [ACD+92a]_R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi, An implementation of three algorithms for timing verification based on automata emptiness, Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS’92), IEEE Soc. Press, 1992, pp. 157–166.Google Scholar
- [ACD+92b]_R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi, Minimization of timed transition systems, Proc. of CONCUR’92, LNCS, vol. 630, Springer-Verlag, 1992, pp. 340–354.Google Scholar
- [BG00]D. Bustan and O. Grumberg, Simulation based minimization, Proc. of the 17th Int. Conf. on Automated Deduction (ICAD’2000) (Pittsburgh), 2000, pp. 255–270.Google Scholar
- [GKP92]U. Goltz, R. Kuiper, and W. Penczek, Propositional temporal logics and equivalences, Proc. of CONCUR’92, LNCS, vol. 630, Springer-Verlag, 1992, pp. 222–236.Google Scholar
- [GL91]O. Grumberg and D. E. Long, Model checking and modular verification, Proc. of CONCUR’91, LNCS, vol. 527, Springer-Verlag, 1991, pp. 250–265.Google Scholar
- [HHK95]M. Henzinger, T. Henzinger, and P. Kopke, Computing simulations on finite and infinite graphs, Proc. of the 36th Annual IEEE Symposium on Foundations of Computer Science (FOCS’95), 1995, pp. 453–462.Google Scholar
- [PP01]W. Penczek and A. Półrola, Abstractions and partial order reductions for checking branching properties of Time Petri Nets, Proc. of the Int. Conf. on Applications and Theory of Petri Nets (ICATPN’01), LNCS, vol. 2075, Springer-Verlag, 2001, pp. 323–342.Google Scholar
- [TY96]S. Tripakis and S. Yovine, Analysis of timed systems based on time-abstracting bisimulations, Proc. of CAV’96, LNCS, vol. 1102, Springer-Verlag, 1996, pp. 232–243.Google Scholar