Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking

J. Barnat, L. Brim, P. Šimeček, M. Weber

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

20 Citations (Scopus)

Abstract

Revisiting resistant graph algorithms are those that can tolerate re-exploration of edges without yielding incorrect results. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.
Original languageUndefined
Title of host publication14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008
EditorsC.R. Ramakrishnan, J Rehof
Place of PublicationLondon
PublisherSpringer
Pages48-62
Number of pages14
ISBN (Print)978-3-540-78799-0
DOIs
Publication statusPublished - Mar 2008

Publication series

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

Keywords

  • EWI-12954
  • METIS-251039
  • IR-62369

Cite this

Barnat, J., Brim, L., Šimeček, P., & Weber, M. (2008). Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. In C. R. Ramakrishnan, & J. Rehof (Eds.), 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008 (pp. 48-62). [10.1007/978-3-540-78800-3_5] (Lecture Notes in Computer Science; Vol. 4963, No. 302). London: Springer. https://doi.org/10.1007/978-3-540-78800-3_5
Barnat, J. ; Brim, L. ; Šimeček, P. ; Weber, M. / Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008. editor / C.R. Ramakrishnan ; J Rehof. London : Springer, 2008. pp. 48-62 (Lecture Notes in Computer Science; 302).
@inproceedings{6c4a2ad547fc454aaa413b3a41ca9434,
title = "Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking",
abstract = "Revisiting resistant graph algorithms are those that can tolerate re-exploration of edges without yielding incorrect results. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.",
keywords = "EWI-12954, METIS-251039, IR-62369",
author = "J. Barnat and L. Brim and P. Šimeček and M. Weber",
note = "10.1007/978-3-540-78800-3_5",
year = "2008",
month = "3",
doi = "10.1007/978-3-540-78800-3_5",
language = "Undefined",
isbn = "978-3-540-78799-0",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "302",
pages = "48--62",
editor = "C.R. Ramakrishnan and J Rehof",
booktitle = "14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008",

}

Barnat, J, Brim, L, Šimeček, P & Weber, M 2008, Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. in CR Ramakrishnan & J Rehof (eds), 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008., 10.1007/978-3-540-78800-3_5, Lecture Notes in Computer Science, no. 302, vol. 4963, Springer, London, pp. 48-62. https://doi.org/10.1007/978-3-540-78800-3_5

Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. / Barnat, J.; Brim, L.; Šimeček, P.; Weber, M.

14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008. ed. / C.R. Ramakrishnan; J Rehof. London : Springer, 2008. p. 48-62 10.1007/978-3-540-78800-3_5 (Lecture Notes in Computer Science; Vol. 4963, No. 302).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking

AU - Barnat, J.

AU - Brim, L.

AU - Šimeček, P.

AU - Weber, M.

N1 - 10.1007/978-3-540-78800-3_5

PY - 2008/3

Y1 - 2008/3

N2 - Revisiting resistant graph algorithms are those that can tolerate re-exploration of edges without yielding incorrect results. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.

AB - Revisiting resistant graph algorithms are those that can tolerate re-exploration of edges without yielding incorrect results. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.

KW - EWI-12954

KW - METIS-251039

KW - IR-62369

U2 - 10.1007/978-3-540-78800-3_5

DO - 10.1007/978-3-540-78800-3_5

M3 - Conference contribution

SN - 978-3-540-78799-0

T3 - Lecture Notes in Computer Science

SP - 48

EP - 62

BT - 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008

A2 - Ramakrishnan, C.R.

A2 - Rehof, J

PB - Springer

CY - London

ER -

Barnat J, Brim L, Šimeček P, Weber M. Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. In Ramakrishnan CR, Rehof J, editors, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008. London: Springer. 2008. p. 48-62. 10.1007/978-3-540-78800-3_5. (Lecture Notes in Computer Science; 302). https://doi.org/10.1007/978-3-540-78800-3_5