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:

[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
[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
[17]	Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theoret. Comput. Sci., 256, 1-2, 63-92 (2001) · Zbl 0973.68170
[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
[25]	Peterson, J. L., Petri Net Theory and the Modeling of Systems (1981), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ