In: Doron A. Peled, Yih-Kuen Tsay (Eds.): Lecture Notes in Computer Science, 3707: Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005., pages 187-201. Springer-Verlag, October 2005. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/1156294816,.
Abstract: Object-based systems present particular challenges for state space exploration. Objects can be dynamically created and discarded, and can be referenced via object identifiers. Consistent relabelling of object identifiers in a state leads to a state that is superficially different but behaviourally equivalent to the original. Similarly, object-based systems can include garbage which has no effect on subsequent behaviour but which results in unnecessary differentiation of states. Both of these factors can lead to state space explosion. This paper considers state space exploration for object-based systems based on the Petri Net formalism. It addresses the above issues by using both equivalence reduction and the sweep-line technique. Experimental results are presented for a simple case study of a communication protocol.