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

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

doi:10.1007/978-3-540-78800-3_5

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 proceeding › Conference contribution › Academic › peer-review

24 Citations (Scopus)

2 Downloads (Pure)

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 language	Undefined
Title of host publication	14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008
Editors	C.R. Ramakrishnan, J Rehof
Place of Publication	London
Publisher	Springer
Pages	48-62
Number of pages	14
ISBN (Print)	978-3-540-78799-0
DOIs	https://doi.org/10.1007/978-3-540-78800-3_5
Publication status	Published - Mar 2008
Event	14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008 - Budapest, Hungary Duration: 29 Mar 2008 → 6 Apr 2008

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Number	302
Volume	4963
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008
Period	29/03/08 → 6/04/08
Other	29 Mar - 06 Apr 2008

Keywords

EWI-12954
METIS-251039
IR-62369

Access to Document

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

http://eprints.eemcs.utwente.nl/secure2/12954/01/tacas-2008-io-map-rr.pdf

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). Article 10.1007/978-3-540-78800-3_5 (Lecture Notes in Computer Science; Vol. 4963, No. 302). Springer. https://doi.org/10.1007/978-3-540-78800-3_5

@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. {\v S}ime{\v c}ek and M. Weber",

note = "10.1007/978-3-540-78800-3_5 ; 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008 ; Conference date: 29-03-2008 Through 06-04-2008",

year = "2008",

month = mar,

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",

address = "Germany",

}

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, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008, 29/03/08. 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. et al.
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 proceeding › Conference contribution › Academic › peer-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

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

Y2 - 29 March 2008 through 6 April 2008

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). doi: 10.1007/978-3-540-78800-3_5