Vincent Bloemen

In International Journal on Software Tools for Technology Transfer

Abstract In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) Büchi automaton (TGBA) is used for this procedure.This paper investigates whether using a more general form of acceptance, namely a transition-based generalized Rabin automaton (TGRA), improves the model checking procedure. TGRAs can have significantly fewer states than TGBAs, however the corresponding emptiness checking procedure is more involved.

Parallel model checking algorithms for linear-time temporal logic

By Jiřı́ Barnat, Vincent Bloemen, Alexandre Duret-Lutz, Alfons Laarman, Laure Petrucci, Jaco van de Pol, Étienne Renault

2018-04-10

In Handbook of parallel constraint reasoning

Abstract Model checking is a fully automated, formal method for demonstrating absence of bugs in reactive systems. Here, bugs are violations of properties in Linear-time Temporal Logic (LTL). A fundamental challenge to its application is the exponential explosion in the number of system states. The current chapter discusses the use of parallelism in order to overcome this challenge. We reiterate the textbook automata-theoretic approach, which reduces the model checking problem to the graph problem of finding cycles.

Explicit state model checking with generalized büchi and rabin automata

By Vincent Bloemen, Alexandre Duret-Lutz, Jaco van de Pol

2017-05-22

In Proceedings of the 24th international SPIN symposium on model checking of software (SPIN’17)

Abstract In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) Büchi automaton (TGBA) is used for this procedure.This paper investigates whether using a more general form of acceptance, namely transition-based generalized Rabin automata (TGRAs), improves the model checking procedure. TGRAs can have significantly fewer states than TGBAs, however the corresponding emptiness checking procedure is more involved.

Model checking with generalized Rabin and Fin-less automata

Parallel model checking algorithms for linear-time temporal logic

Explicit state model checking with generalized büchi and rabin automata

Search

Tags