Read, Write and Copy Dependencies for Symbolic Model Checking

Jeroen Meijer, Gijs Kant, Stefan Blom, Jan Cornelis van de Pol

  • 4 Citations

Abstract

This paper aims at improving symbolic model checking for explicit state modeling languages, e.g., Promela, Dve and mCRL2. The modular Pins architecture of LTSmin supports a notion of event locality, by merely indicating for each event on which variables it depends. However, one could distinguish four separate dependencies: read, may-write, must-write and copy. In this paper, we introduce these notions in a language-independent manner. In particular, models with arrays need to distinguish overwriting and copying of values. We also adapt the symbolic model checking algorithms to exploit the refined dependency information. We have implemented refined dependency matrices for Promela, Dve and mCRL2, in order to compare our new algorithms to the original version of LTSmin. The results show that the amount of successor computations and memory footprint are greatly reduced. Finally, the optimal variable ordering is also affected by the refined dependencies: We determined experimentally that variables with a read dependency should occur at a higher BDD level than variables with a write dependency.
Original languageUndefined
Title of host publicationProceedings of the 10th International Haifa Verification Conference, HVC 2014
Place of PublicationBerlin
PublisherSpringer
Pages204-219
Number of pages16
ISBN (Print)978-3-319-13337-9
DOIs
StatePublished - Nov 2014

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume8855
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Model checking
Copying
Modeling languages

Keywords

  • EWI-25296
  • METIS-309656
  • IR-93290

Cite this

Meijer, J., Kant, G., Blom, S., & van de Pol, J. C. (2014). Read, Write and Copy Dependencies for Symbolic Model Checking. In Proceedings of the 10th International Haifa Verification Conference, HVC 2014 (pp. 204-219). (Lecture Notes in Computer Science; Vol. 8855). Berlin: Springer. DOI: 10.1007/978-3-319-13338-6_16

Meijer, Jeroen; Kant, Gijs; Blom, Stefan; van de Pol, Jan Cornelis / Read, Write and Copy Dependencies for Symbolic Model Checking.

Proceedings of the 10th International Haifa Verification Conference, HVC 2014. Berlin : Springer, 2014. p. 204-219 (Lecture Notes in Computer Science; Vol. 8855).

Research output: Scientific - peer-reviewConference contribution

@inbook{20597d20bcc04c19b3d0729e66649bdc,
title = "Read, Write and Copy Dependencies for Symbolic Model Checking",
abstract = "This paper aims at improving symbolic model checking for explicit state modeling languages, e.g., Promela, Dve and mCRL2. The modular Pins architecture of LTSmin supports a notion of event locality, by merely indicating for each event on which variables it depends. However, one could distinguish four separate dependencies: read, may-write, must-write and copy. In this paper, we introduce these notions in a language-independent manner. In particular, models with arrays need to distinguish overwriting and copying of values. We also adapt the symbolic model checking algorithms to exploit the refined dependency information. We have implemented refined dependency matrices for Promela, Dve and mCRL2, in order to compare our new algorithms to the original version of LTSmin. The results show that the amount of successor computations and memory footprint are greatly reduced. Finally, the optimal variable ordering is also affected by the refined dependencies: We determined experimentally that variables with a read dependency should occur at a higher BDD level than variables with a write dependency.",
keywords = "EWI-25296, METIS-309656, IR-93290",
author = "Jeroen Meijer and Gijs Kant and Stefan Blom and {van de Pol}, {Jan Cornelis}",
note = "10.1007/978-3-319-13338-6_16",
year = "2014",
month = "11",
doi = "10.1007/978-3-319-13338-6_16",
isbn = "978-3-319-13337-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "204--219",
booktitle = "Proceedings of the 10th International Haifa Verification Conference, HVC 2014",

}

Meijer, J, Kant, G, Blom, S & van de Pol, JC 2014, Read, Write and Copy Dependencies for Symbolic Model Checking. in Proceedings of the 10th International Haifa Verification Conference, HVC 2014. Lecture Notes in Computer Science, vol. 8855, Springer, Berlin, pp. 204-219. DOI: 10.1007/978-3-319-13338-6_16

Read, Write and Copy Dependencies for Symbolic Model Checking. / Meijer, Jeroen; Kant, Gijs; Blom, Stefan; van de Pol, Jan Cornelis.

Proceedings of the 10th International Haifa Verification Conference, HVC 2014. Berlin : Springer, 2014. p. 204-219 (Lecture Notes in Computer Science; Vol. 8855).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Read, Write and Copy Dependencies for Symbolic Model Checking

AU - Meijer,Jeroen

AU - Kant,Gijs

AU - Blom,Stefan

AU - van de Pol,Jan Cornelis

N1 - 10.1007/978-3-319-13338-6_16

PY - 2014/11

Y1 - 2014/11

N2 - This paper aims at improving symbolic model checking for explicit state modeling languages, e.g., Promela, Dve and mCRL2. The modular Pins architecture of LTSmin supports a notion of event locality, by merely indicating for each event on which variables it depends. However, one could distinguish four separate dependencies: read, may-write, must-write and copy. In this paper, we introduce these notions in a language-independent manner. In particular, models with arrays need to distinguish overwriting and copying of values. We also adapt the symbolic model checking algorithms to exploit the refined dependency information. We have implemented refined dependency matrices for Promela, Dve and mCRL2, in order to compare our new algorithms to the original version of LTSmin. The results show that the amount of successor computations and memory footprint are greatly reduced. Finally, the optimal variable ordering is also affected by the refined dependencies: We determined experimentally that variables with a read dependency should occur at a higher BDD level than variables with a write dependency.

AB - This paper aims at improving symbolic model checking for explicit state modeling languages, e.g., Promela, Dve and mCRL2. The modular Pins architecture of LTSmin supports a notion of event locality, by merely indicating for each event on which variables it depends. However, one could distinguish four separate dependencies: read, may-write, must-write and copy. In this paper, we introduce these notions in a language-independent manner. In particular, models with arrays need to distinguish overwriting and copying of values. We also adapt the symbolic model checking algorithms to exploit the refined dependency information. We have implemented refined dependency matrices for Promela, Dve and mCRL2, in order to compare our new algorithms to the original version of LTSmin. The results show that the amount of successor computations and memory footprint are greatly reduced. Finally, the optimal variable ordering is also affected by the refined dependencies: We determined experimentally that variables with a read dependency should occur at a higher BDD level than variables with a write dependency.

KW - EWI-25296

KW - METIS-309656

KW - IR-93290

U2 - 10.1007/978-3-319-13338-6_16

DO - 10.1007/978-3-319-13338-6_16

M3 - Conference contribution

SN - 978-3-319-13337-9

T3 - Lecture Notes in Computer Science

SP - 204

EP - 219

BT - Proceedings of the 10th International Haifa Verification Conference, HVC 2014

PB - Springer

ER -

Meijer J, Kant G, Blom S, van de Pol JC. Read, Write and Copy Dependencies for Symbolic Model Checking. In Proceedings of the 10th International Haifa Verification Conference, HVC 2014. Berlin: Springer. 2014. p. 204-219. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-13338-6_16