Geodesic
Local entailment test in the reachability problem for well structured transition systems
Sibirskij žurnal čistoj i prikladnoj matematiki, Tome 6 (2006) no. 3, pp. 88-97 
D. L. Chubarov. Local entailment test in the reachability problem for well structured transition systems. Sibirskij žurnal čistoj i prikladnoj matematiki, Tome 6 (2006) no. 3, pp. 88-97. http://geodesic.mathdoc.fr/item/VNGU_2006_6_3_a6/
@article{VNGU_2006_6_3_a6,
     author = {D. L. Chubarov},
     title = {Local entailment test in the reachability problem for well structured transition systems},
     journal = {Sibirskij \v{z}urnal \v{c}istoj i prikladnoj matematiki},
     pages = {88--97},
     year = {2006},
     volume = {6},
     number = {3},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VNGU_2006_6_3_a6/}
}
TY  - JOUR
AU  - D. L. Chubarov
TI  - Local entailment test in the reachability problem for well structured transition systems
JO  - Sibirskij žurnal čistoj i prikladnoj matematiki
PY  - 2006
SP  - 88
EP  - 97
VL  - 6
IS  - 3
UR  - http://geodesic.mathdoc.fr/item/VNGU_2006_6_3_a6/
LA  - ru
ID  - VNGU_2006_6_3_a6
ER  - 
%0 Journal Article
%A D. L. Chubarov
%T Local entailment test in the reachability problem for well structured transition systems
%J Sibirskij žurnal čistoj i prikladnoj matematiki
%D 2006
%P 88-97
%V 6
%N 3
%U http://geodesic.mathdoc.fr/item/VNGU_2006_6_3_a6/
%G ru
%F VNGU_2006_6_3_a6

Voir la notice de l'article provenant de la source Math-Net.Ru

We describe the symbolic backward reachability procedure for infinite state systems and show that the variant of the procedure with the local entailment test still decides coverability properties of well structured systems.

[1] Yu. L. Ershov, S. S. Goncharov, Konstruktivnye modeli. Sibirskaya shkola algebry i logiki, Nauchnaya kniga, Novosibirsk, 1999

[2] E. V. Kuzmin, V. A. Sokolov, Vpolne strukturirovannye sistemy pomechennykh perekhodov, Fizmatlit, M., 2005 | Zbl

[3] E. V. Kuzmin, V. A. Sokolov, Strukturirovannye sistemy perekhodov, Fizmatlit, M., 2006 | MR

[4] P. A. Abdulla, K. C̆erāns, B. Jonsson, Y.-K. Tsay, “General decidability theorems for infinite state systems”, LICS, 1996, 313–321 | MR

[5] S. Bardin, A. Finkel, J. Leroux, L. Petrucci, “FAST: Fast Accelereation of Symbolic Transition systems”, Proc. 15th Conf. Computer Aided Verification (CAV'2003), Lect. Notes in Comput. Sci., 2725, Springer, 2003, 118–121 | DOI

[6] G. Delzanno, A. Podelski, “Constraint-based deductive model checking”, STTT, 3:3 (2001), 250–270 | Zbl

[7] J. Esparza, A. Finkel, R. Mayr, “On the verification of broadcast protocols”, LICS, 1999, 352–359 | MR

[8] A. Finkel, “A generalization of the procedure of Karp and Miller to well structured transition system”, ICALP, 1987, 499–508 | MR | Zbl

[9] A. Finkel, Ph. Schnoebelen, “Fundamental structures in well-structured infinite transition systems”, LATIN, 1998, 102–118 | MR

[10] A. Finkel, “Reduction and covering of infinite reachability trees”, Inf. Comput., 89:2 (1990), 144–179 | DOI | MR | Zbl

[11] J. Jaffar, M. J. Maher, “Constraint logic programming: A survey”, J. Log. Program., 19–20 (1994), 503–581 | DOI | MR

[12] J. Kruskal, “The theory of well-quasi-ordering: a frequently discovered concept”, J. Comb. Theory, Ser. A, 13 (1972), 297–305 | DOI | MR | Zbl

[13] T. Rybina, A. Voronkov, “BRAIN: Backward reachability analysis with integers”, AMAST, Lect. Notes Comput. Sci., 2422, 2002, 489–494 | DOI | MR

[14] T. Rybina, A. Voronkov, “A logical reconstruction of reachability”, Ershov Memorial Conference, 2003, 222–237 | Zbl

[15] Divesh Srivastava, “Subsumption and indexing in constraint query languages with linear arithmetic constraints”, Ann. Math. Artif. Intell., 8:3–4 (1993), 315–343 | MR | Zbl