Expand, enlarge and check: new algorithms for the coverability problem of WSTS. (English) Zbl 1105.68084

Geeraerts, G.; Raskin, J.-F.; Van Begin, L.

J. Comput. Syst. Sci. 72, No. 1, 180-203 (2006).

Summary: We present a general algorithmic schema called ‘Expand, Enlarge and Check’ from which new algorithms for the coverability problem of WSTS can be constructed. We show here that our schema allows us to define forward algorithms that decide the coverability problem for several classes of systems for which the Karp and Miller procedure cannot be generalized, and for which no complete forward algorithms were known. Our results have important applications for the verification of parameterized systems and communication protocols.
A preliminary version of this paper has been published as [G. Geeraerts, J.-F. Raskin and L. Van Begin, “Expand, enlarge and check: new algorithms for the coverability problem of WSTS”, Lect. Notes Comput. Sci. 3328, 287–298 (2004; Zbl 1105.68353)] in the proceedings of FSTTCS 2004.

MSC:

68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60	Specification and verification (program logics, model checking, etc.)

Keywords:

Well-structured transition systems; Verification; Coverability problem; Parameterized systems; Petri nets; Lossy channel systems

Citations:

Zbl 1105.68353

Software:

FAST

References:

[1]	P. Abdulla, A. Annichini, A. Bouajjani, Symbolic verification of lossy channel systems: application to the bounded retransmission protocol, in: Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), Lecture Notes in Computer Science, vol. 1579, Springer, Berlin, 1999, pp. 208-222.; P. Abdulla, A. Annichini, A. Bouajjani, Symbolic verification of lossy channel systems: application to the bounded retransmission protocol, in: Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), Lecture Notes in Computer Science, vol. 1579, Springer, Berlin, 1999, pp. 208-222.
[2]	P. Abdulla, A. Bouajjani, B. Jonsson, On-the-fly analysis of systems with unbounded, lossy FIFO channels, in: Proceedings of the 10th International Conference on Computer Aided Verification (CAV’98), Lecture Notes in Computer Science, vol. 1427, Springer, Berlin, 1998, pp. 305-318.; P. Abdulla, A. Bouajjani, B. Jonsson, On-the-fly analysis of systems with unbounded, lossy FIFO channels, in: Proceedings of the 10th International Conference on Computer Aided Verification (CAV’98), Lecture Notes in Computer Science, vol. 1427, Springer, Berlin, 1998, pp. 305-318.
[3]	Abdulla, P. A.; Cerans, K.; Jonsson, B.; Tsay, Y.-K., General decidability theorems for infinite-state systems, (Proceedings of the 11th Annual Symposium on Logic in Computer Science (LICS’96) (1996), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 313-321
[4]	Abdulla, P.; Jonsson, B., Verifying programs with unreliable channels, (Proceedings of the Eighth IEEE International Symposium in Logic in Computer Science (LICS’93) (1993), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 160-170
[5]	Alur, R.; Dill, D., A theory of timed automata, Theoret. Comput. Sci., 126, 2, 183-236 (1994) · Zbl 0803.68071
[6]	Araki, T.; Kasami, T., Some decision problems related to the reachability problem for petri nets, Theoret. Comput. Sci., 3, 1, 85-104 (1977) · Zbl 0352.68083
[7]	S. Bardin, A. Finkel, J. Leroux, L. Petrucci, FAST: fast acceleration of symbolic transition systems, in: Proceedings of the 15th International Conference on Computer Aided Verification (CAV’03), Lecture Notes in Computer Science, vol. 2725, Springer, Berlin, 2003, pp. 118-125.; S. Bardin, A. Finkel, J. Leroux, L. Petrucci, FAST: fast acceleration of symbolic transition systems, in: Proceedings of the 15th International Conference on Computer Aided Verification (CAV’03), Lecture Notes in Computer Science, vol. 2725, Springer, Berlin, 2003, pp. 118-125.
[8]	A. Bouajjani, B. Jonsson, M. Nilsson, T. Touili, Regular model checking, in: Proceedings of the Twelfth International Conference on Computer Aided Verification (CAV 2000), Lecture Notes in Computer Science, vol. 1855, Springer, Berlin, 2000, pp. 403-418.; A. Bouajjani, B. Jonsson, M. Nilsson, T. Touili, Regular model checking, in: Proceedings of the Twelfth International Conference on Computer Aided Verification (CAV 2000), Lecture Notes in Computer Science, vol. 1855, Springer, Berlin, 2000, pp. 403-418. · Zbl 0974.68118
[9]	A. Bouajjani, R. Mayr, Model checking lossy vector addition systems, in: Proceedings of the 16th Annual Symposium on Theoretical Aspects of Computer Science (STACS’99), Lecture Notes in Computer Science, vol. 1563, Springer, Berlin, 1999, pp. 323-333.; A. Bouajjani, R. Mayr, Model checking lossy vector addition systems, in: Proceedings of the 16th Annual Symposium on Theoretical Aspects of Computer Science (STACS’99), Lecture Notes in Computer Science, vol. 1563, Springer, Berlin, 1999, pp. 323-333. · Zbl 0926.03035
[10]	G. Ciardo, Petri nets with marking-dependent arc multiplicity: properties and analysis, in: Proceedings of the 15th International Conference on Applications and Theory of Petri Nets (ICATPN 94), Lecture Notes in Computer Science, vol. 815, Springer, Berlin, 1994, pp. 179-198.; G. Ciardo, Petri nets with marking-dependent arc multiplicity: properties and analysis, in: Proceedings of the 15th International Conference on Applications and Theory of Petri Nets (ICATPN 94), Lecture Notes in Computer Science, vol. 815, Springer, Berlin, 1994, pp. 179-198.
[11]	G. Delzanno, J.-F. Raskin, L. Van Begin, Towards the automated verification of multithreaded Java programs, in: Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2002), Lecture Notes in Computer Science, vol. 2280, Springer, Berlin, 2002, pp. 173-187.; G. Delzanno, J.-F. Raskin, L. Van Begin, Towards the automated verification of multithreaded Java programs, in: Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2002), Lecture Notes in Computer Science, vol. 2280, Springer, Berlin, 2002, pp. 173-187. · Zbl 1043.68530
[12]	C. Dufourd, A. Finkel, P. Schnoebelen, Reset nets between decidability and undecidability, in: Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP’98), Lecture Notes in Computer Science, vol. 1443, Springer, Berlin, 1998, pp. 103-115.; C. Dufourd, A. Finkel, P. Schnoebelen, Reset nets between decidability and undecidability, in: Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP’98), Lecture Notes in Computer Science, vol. 1443, Springer, Berlin, 1998, pp. 103-115. · Zbl 0909.68124
[13]	Emerson, E. A.; Namjoshi, K. S., On model checking for non-deterministic infinite-state systems, (Proceedings of the 13th Annual Symposium on Logic in Computer Science (LICS’98) (1998), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 70-80 · Zbl 0945.68523
[14]	Esparza, J.; Finkel, A.; Mayr, R., On the verification of broadcast protocols, (Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS’99) (1999), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 352-359
[15]	Finkel, A., Reduction and covering of infinite reachability trees, Inform. and Comput., 89, 2, 144-179 (1990) · Zbl 0753.68073
[16]	A. Finkel, J.-F. Raskin, M. Samuelides, L. Van Begin, Monotonic extensions of petri nets: forward and backward search revisited, in: Proceedings of the Fourth International Workshop on Verification of Infinite-state Systems (INFINITY 2002), ENTCS, vol. 68, Elsevier, Amsterdam, 2002.; A. Finkel, J.-F. Raskin, M. Samuelides, L. Van Begin, Monotonic extensions of petri nets: forward and backward search revisited, in: Proceedings of the Fourth International Workshop on Verification of Infinite-state Systems (INFINITY 2002), ENTCS, vol. 68, Elsevier, Amsterdam, 2002. · Zbl 1270.68214
[17]	Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theoret. Comput. Sci., 256, 1-2, 63-92 (2001) · Zbl 0973.68170
[18]	G. Geeraerts, J.-F. Raskin, L. Van Begin, Expand, enlarge and check: new algorithms for the coverability problem of WSTS, in: Proceedings of the 24th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 04), Lecture Notes in Computer Science, vol. 3328, Springer, Berlin, 2004, pp. 287-298.; G. Geeraerts, J.-F. Raskin, L. Van Begin, Expand, enlarge and check: new algorithms for the coverability problem of WSTS, in: Proceedings of the 24th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 04), Lecture Notes in Computer Science, vol. 3328, Springer, Berlin, 2004, pp. 287-298. · Zbl 1105.68353
[19]	G. Geeraerts, J.-F. Raskin, L. Van Begin, Expand, enlarge and check... made efficient, Proceedings of the seventeenth International Conference on Computer Aided Verification (CAV2005), Lecture Notes in Computer Science, vol. 3576, Springer, Berlin, 2005, pp. 394-407.; G. Geeraerts, J.-F. Raskin, L. Van Begin, Expand, enlarge and check... made efficient, Proceedings of the seventeenth International Conference on Computer Aided Verification (CAV2005), Lecture Notes in Computer Science, vol. 3576, Springer, Berlin, 2005, pp. 394-407. · Zbl 1081.68619
[20]	Henzinger, T. A., The theory of hybrid automata, (Proceedings of the 11th Symposium on Logic in Computer Science (LICS’96) (1996), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 278
[21]	Henzinger, T. A.; Kupferman, O.; Qadeer, S., From prehistoric to postmodern symbolic model checking, Formal Methods in System Design, 23, 3, 303-327 (2003) · Zbl 1074.68036
[22]	Immerman, N., Number of quantifiers is better than number of tape cells, J. Comput. Syst. Sci., 22, 3, 384-406 (1981) · Zbl 0486.03019
[23]	Karp, R. M.; Miller, R. E., Parallel program schemata, J. Comput. Syst. Sci., 3, 147-195 (1969) · Zbl 0198.32603
[24]	Milner, R., Communication and Concurrency, Prentice-Hall International Series in Computer Science (1989), Prentice-Hall: Prentice-Hall New York · Zbl 0683.68008
[25]	Peterson, J. L., Petri Net Theory and the Modeling of Systems (1981), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0461.68059
[26]	J.-F. Raskin, L. Van Begin, Petri nets with non-blocking arcs are difficult to analyse, in: Proceedings of the Fifth International Workshop on Verification of Infinite-state Systems (INFINITY 2003), ENTCS, vol. 96, Elsevier, Amsterdam, 2003.; J.-F. Raskin, L. Van Begin, Petri nets with non-blocking arcs are difficult to analyse, in: Proceedings of the Fifth International Workshop on Verification of Infinite-state Systems (INFINITY 2003), ENTCS, vol. 96, Elsevier, Amsterdam, 2003.
[27]	R. Valk, On the computational power of extended petri nets, in: Proceedings of the Seventh Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 64, Springer, Berlin, 1978, pp. 527-535.; R. Valk, On the computational power of extended petri nets, in: Proceedings of the Seventh Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 64, Springer, Berlin, 1978, pp. 527-535. · Zbl 0394.68044