Abstract

Specifications for non-terminating reactive systems are described by ω-regular properties. Such properties can be translated in various types of automata, e.g. Büchi, Rabin, and Parity. A model checker can then check for language containment and determine whether the system meets the specification. Checking these automata becomes more complex when introducing probabilities and/or an adversary, e.g. the uncontrollable environment, to the automaton. Parallel algorithms have become crucial for fully utilizing current hardware systems. With respect to model checking we therefore focus on designing scalable parallel algorithms for emptiness checking. This research focuses on designing and improving parallel graph searching algorithms for emptiness checking on various types of ω-automata. As a basis, we developed a scalable multi-core on-the-fly algorithm for the detection of strongly connected components (SCCs). Our aim is to contribute to the state-of-the-art techniques in parallel model checking, based on both theoretical complexity analysis and empirical studies on suitable benchmarks.
Original languageEnglish
Title of host publicationProceedings of the Formal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016)
EditorsAndrew Butterfield, Matteo Rossi
Place of PublicationAachen
PublisherCEUR Workshop Proceedings
Pages1
Number of pages6
StatePublished - 8 Nov 2016
EventFormal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016) - Limassol, Cyprus

Publication series

Name
PublisherCEUR Workshop Proceedings
Volume1744
ISSN (Print)1613-0073

Conference

ConferenceFormal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016)
Abbreviated titleFM-DS 2016
CountryCyprus
CityLimassol
Period8/11/168/11/16
Other8 Nov 2016

Fingerprint

Model checking
Parallel algorithms
Specifications
Hardware

Keywords

  • EWI-27452
  • Büchi
  • Model Checking
  • Multi-Core
  • IR-102923
  • LTL
  • Parallel
  • Parity
  • METIS-320899
  • Rabin

Cite this

Bloemen, V. (2016). Parallel Model Checking of ω-Automata. In A. Butterfield, & M. Rossi (Eds.), Proceedings of the Formal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016) (pp. 1). Aachen: CEUR Workshop Proceedings.

Bloemen, Vincent / Parallel Model Checking of ω-Automata.

Proceedings of the Formal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016). ed. / Andrew Butterfield; Matteo Rossi. Aachen : CEUR Workshop Proceedings, 2016. p. 1.

Research output: Scientific - peer-reviewConference contribution

@inbook{cd55e841b1f94fb5ae2ac534b92884be,
title = "Parallel Model Checking of ω-Automata",
abstract = "Specifications for non-terminating reactive systems are described by ω-regular properties. Such properties can be translated in various types of automata, e.g. Büchi, Rabin, and Parity. A model checker can then check for language containment and determine whether the system meets the specification. Checking these automata becomes more complex when introducing probabilities and/or an adversary, e.g. the uncontrollable environment, to the automaton. Parallel algorithms have become crucial for fully utilizing current hardware systems. With respect to model checking we therefore focus on designing scalable parallel algorithms for emptiness checking. This research focuses on designing and improving parallel graph searching algorithms for emptiness checking on various types of ω-automata. As a basis, we developed a scalable multi-core on-the-fly algorithm for the detection of strongly connected components (SCCs). Our aim is to contribute to the state-of-the-art techniques in parallel model checking, based on both theoretical complexity analysis and empirical studies on suitable benchmarks.",
keywords = "EWI-27452, Büchi, Model Checking, Multi-Core, IR-102923, LTL, Parallel, Parity, METIS-320899, Rabin",
author = "Vincent Bloemen",
year = "2016",
month = "11",
publisher = "CEUR Workshop Proceedings",
pages = "1",
editor = "Andrew Butterfield and Matteo Rossi",
booktitle = "Proceedings of the Formal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016)",

}

Bloemen, V 2016, Parallel Model Checking of ω-Automata. in A Butterfield & M Rossi (eds), Proceedings of the Formal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016). CEUR Workshop Proceedings, Aachen, pp. 1, Formal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016), Limassol, Cyprus, 8-8 November.

Parallel Model Checking of ω-Automata. / Bloemen, Vincent.

Proceedings of the Formal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016). ed. / Andrew Butterfield; Matteo Rossi. Aachen : CEUR Workshop Proceedings, 2016. p. 1.

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Parallel Model Checking of ω-Automata

AU - Bloemen,Vincent

PY - 2016/11/8

Y1 - 2016/11/8

N2 - Specifications for non-terminating reactive systems are described by ω-regular properties. Such properties can be translated in various types of automata, e.g. Büchi, Rabin, and Parity. A model checker can then check for language containment and determine whether the system meets the specification. Checking these automata becomes more complex when introducing probabilities and/or an adversary, e.g. the uncontrollable environment, to the automaton. Parallel algorithms have become crucial for fully utilizing current hardware systems. With respect to model checking we therefore focus on designing scalable parallel algorithms for emptiness checking. This research focuses on designing and improving parallel graph searching algorithms for emptiness checking on various types of ω-automata. As a basis, we developed a scalable multi-core on-the-fly algorithm for the detection of strongly connected components (SCCs). Our aim is to contribute to the state-of-the-art techniques in parallel model checking, based on both theoretical complexity analysis and empirical studies on suitable benchmarks.

AB - Specifications for non-terminating reactive systems are described by ω-regular properties. Such properties can be translated in various types of automata, e.g. Büchi, Rabin, and Parity. A model checker can then check for language containment and determine whether the system meets the specification. Checking these automata becomes more complex when introducing probabilities and/or an adversary, e.g. the uncontrollable environment, to the automaton. Parallel algorithms have become crucial for fully utilizing current hardware systems. With respect to model checking we therefore focus on designing scalable parallel algorithms for emptiness checking. This research focuses on designing and improving parallel graph searching algorithms for emptiness checking on various types of ω-automata. As a basis, we developed a scalable multi-core on-the-fly algorithm for the detection of strongly connected components (SCCs). Our aim is to contribute to the state-of-the-art techniques in parallel model checking, based on both theoretical complexity analysis and empirical studies on suitable benchmarks.

KW - EWI-27452

KW - Büchi

KW - Model Checking

KW - Multi-Core

KW - IR-102923

KW - LTL

KW - Parallel

KW - Parity

KW - METIS-320899

KW - Rabin

M3 - Conference contribution

SP - 1

BT - Proceedings of the Formal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016)

PB - CEUR Workshop Proceedings

ER -

Bloemen V. Parallel Model Checking of ω-Automata. In Butterfield A, Rossi M, editors, Proceedings of the Formal Methods 2016 Doctoral Symposium co-located with 21st International Symposium on Formal Methods (FM 2016). Aachen: CEUR Workshop Proceedings. 2016. p. 1.