For the most recent entries see the Petri Nets Newsletter.

Automated Verification of Infinite State Concurrent Systems.

Dembinski, Piotr; Penczek, Wojciech; Pólrola, Agata

In: R. Wyrzykowski, J. Dongarra, M. Paprzycki, J. Wasniewski (Eds.): Parallel Processing and Applied Mathematics, 4th International Conference, PPAM 2001 Naleczów, Poland, September 9-12, 2001. Revised Papers, pages 1-247pp. Springer Verlag, LNCS 2328, June 2002.

Abstract: 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.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography