Étienne Renault

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.

Continue reading

Heuristics for checking liveness properties with partial order reductions

By Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Étienne Renault

2016-06-17

In Proceedings of the 14th international symposium on automated technology for verification and analysis (ATVA’16)

Abstract Checking liveness properties with partial-order reductions requires a cycle proviso to ensure that an action cannot be postponed forever. The proviso forces each cycle to contain at least one fully expanded state. We present new heuristics to select which state to expand, hoping to reduce the size of the resulting graph. The choice of the state to expand is done when encountering a dangerous edge. Almost all existing provisos expand the source of this edge, while this paper also explores the expansion of the destination and the use of SCC-based information.

Continue reading

Spot 2.0 — a framework for LTL and $\omega$-automata manipulation

By Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Étienne Renault, Laurent Xu

2016-06-17

In Proceedings of the 14th international symposium on automated technology for verification and analysis (ATVA’16)

Abstract We present Spot 2.0, a C++ library with Python bindings and an assortment of command-line tools designed to manipulate LTL and $\omega$-automata in batch. New automata-manipulation tools were introduced in Spot 2.0; they support arbitrary acceptance conditions, as expressible in the Hanoi Omega Automaton format. Besides being useful to researchers who have automata to process, its Python bindings can also be used in interactive environments to teach $\omega$-automata and model checking.

Continue reading

Variations on parallel explicit model checking for generalized Büchi automata

By Étienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud

2015-10-26

In International Journal on Software Tools for Technology Transfer (STTT)

Abstract We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a Strongly Connected Component (SCC) enumeration, support generalized Büchi acceptance, and require no synchronization points nor recomputing procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton checked. Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks.

Continue reading

Parallel explicit model checking for generalized Büchi automata

By Étienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud

2015-01-13

In Proceedings of the 19th international conference on tools and algorithms for the construction and analysis of systems (TACAS’15)

Abstract We present new parallel emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on an SCC enumeration, support generalized Buchi acceptance, and require no synchronization points nor repair procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton being checked. Our prototype implementation has encouraging performances: the new emptiness checks have better speedup than existing algorithms in half of our experiments.

Continue reading

Contribution aux tests de vacuité pour le model checking explicite

By Étienne Renault

2014-12-05

In

Abstract The automata-theoretic approach to linear time model-checking is a standard technique for formal verification of concurrent systems. The system and the property to check are modeled with omega-automata that recognizes infinite words. Operations overs these automata (synchronized product and emptiness checks) allows to determine whether the system satisfies the property or not. In this thesis we focus on a particular type of omega-automata that enable a concise representation of weak fairness properties: transitions-based generalized Büchi automata (TGBA).

Continue reading

Three SCC-based emptiness checks for generalized Büchi automata

By Étienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud

2013-10-09

In Proceedings of the 19th international conference on logic for programming, artificial intelligence, and reasoning (LPAR’13)

Abstract The automata-theoretic approach for the verification of linear time properties involves checking the emptiness of a Büchi automaton. However generalized Büchi automata, with multiple acceptance sets, are preferred when verifying under weak fairness hypotheses. Existing emptiness checks for which the complexity is independent of the number of acceptance sets are all based on the enumeration of Strongly Connected Components (SCCs). In this paper, we review the state of the art SCC enumeration algorithms to study how they can be turned into emptiness checks.

Continue reading

Strength-based decomposition of the property Büchi automaton for faster model checking

By Étienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud

2013-01-08

In Proceedings of the 19th international conference on tools and algorithms for the construction and analysis of systems (TACAS’13)

Abstract The automata-theoretic approach for model checking of linear-time temporal properties involves the emptiness check of a large Büchi automaton. Specialized emptiness-check algorithms have been proposed for the cases where the property is represented by a weak or terminal automaton. When the property automaton does not fall into these categories, a general emptiness check is required. This paper focuses on this class of properties. We refine previous approaches by classifying strongly-connected components rather than automata, and suggest a decomposition of the property automaton into three smaller automata capturing the terminal, weak, and the remaining strong behaviors of the property.

Continue reading

Search

Tags