Geodesic
Optimization procedures in affine model checking
Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 56-67.

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

Symbolic model checking is based on a compact representation of sets of states and transition relations. At present there are three basic approaches of symbolic model checking: BDD-methods, bounded model checking using SAT-solvers, and various algebraic techniques, for example, constraint based model checking and regular model checking. In this paper we suggest improved algorithms for an algebraic data representation, namely, optimization algorithms for affine data structures.
Keywords: symbolic model checking, algebraic data representation, distributed systems. 
@article{MAIS_2011_18_4_a5,
     author = {N. O. Garanina},
     title = {Optimization procedures in affine model checking},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {56--67},
     publisher = {mathdoc},
     volume = {18},
     number = {4},
     year = {2011},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a5/}
}
TY  - JOUR
AU  - N. O. Garanina
TI  - Optimization procedures in affine model checking
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2011
SP  - 56
EP  - 67
VL  - 18
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a5/
LA  - ru
ID  - MAIS_2011_18_4_a5
ER  - 
%0 Journal Article
%A N. O. Garanina
%T Optimization procedures in affine model checking
%J Modelirovanie i analiz informacionnyh sistem
%D 2011
%P 56-67
%V 18
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a5/
%G ru
%F MAIS_2011_18_4_a5
N. O. Garanina. Optimization procedures in affine model checking. Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 56-67. http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a5/

[1] P. A. Abdulla, B. Jonsson, M. Nilsson, M. Saksena, “A Survey of Regular Model Checking”, Proc. of CONCUR'04 – Concurrency Theory, 15th International Conference (London, UK, August 31 – September 3, 2004), Lect. Notes Comput. Sci., 3170, 2004, 35–48 | DOI | Zbl

[2] C. Bartzis, T. Bultan, “Efficient Symbolic Representations for Arithmetic Constraints in Verification”, Int. J. Found. Comput. Sci., 4 (2003), 605–624 | DOI | MR | Zbl

[3] B. Boigelot, P. Wolper, “Symbolic Verification with Periodic Sets”, Lect. Notes Comput. Sci., 818, 1994, 55–67

[4] B. Boigelot, A. Legay, P. Wolper, “Iterating transducers in the large”, Proc. 15th Int. Conf. on Computer Aided Verification (2003), Lecture Notes in Computer Science, 2725, 223–235 | DOI | MR | Zbl

[5] R. E. Bryant, “Symbolic boolean manipulation with ordered binary decision diagrams”, IEEE Trans. Computers, C-35:8 (1986), 293–318 | DOI

[6] T. Bultan, R. Gerber, W. Pugh, “Model Checking Concurrent Systems With Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results”, ACM Trans. Progr. Lang. and Systems, 21:4 (1999), 747–789 | DOI

[7] T. Bultan, “BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems”, Proc. of Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference (TACAS 2000, Berlin, Germany, March 25 – April 2, 2000), Lect. Notes Comput. Sci., 1785, 2000, 441–455 | DOI | Zbl

[8] E. M. Clarke, O. Grumberg, D. Peled, Model Checking, MIT Press, London, 1999, 314 pp.

[9] D. Kozen, “Results on the Propositional Mu-Calculus”, Theor. Comput. Sci., 27:3 (1983), 333–354 | DOI | MR | Zbl

[10] K. L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem, Kluwer Academic Publishers, 1993, 216 pp. | Zbl

[11] K. L. McMillan, “Applying SAT Methods in Unbounded Symbolic Model Checking”, Proc. of 14th International Conference, CAV'02 (Copenhagen, Denmark, July 27–31, 2002), Lect. Notes Comput. Sci., 2404, 2002, 250–264 | DOI | Zbl

[12] N. V. Shilov, N. O. Garanina, “A Polynomial Approximations for Model Checking”, Lect. Notes Comput. Sci., 2890, 2003, 395–400 | DOI | Zbl

[13] T. Yavuz-Kahveci, T. Bultan, “Heuristics for Efficient Manipulation of Composite Constraints”, Proc. of Frontiers of Combining Systems, 4th International Workshop (FroCoS 2002, Santa Margherita Ligure, Italy, April 8–10, 2002), Lect. Notes Comput. Sci., 2309, 2002, 57–71 | DOI | Zbl

[14] N. O. Garanina, Verifikatsiya raspredelennykh sistem s ispolzovaniem affinnogo predstavleniya dannykh, logik znanii i deistvii, dis. ... kand. fiz.-mat. nauk, Novosibirsk, 2004, 172 pp.

[15] N. O. Garanina, Affinnoe predstavlenie dannykh dlya proverki modelei programm, Prepr. Sib. otd-nie. RAN. ISI; #116, Novosibirsk, 2004, 48 pp.

[16] N. O. Garanina, “Proverka modelei raspredelennykh sistem s pomoschyu affinnogo predstavleniya dannykh”, Modelirovanie i analiz informatsionnykh sistem, 17:4 (2010), 52–59

[17] http://www.cs.umd.edu/projects/omega/