Denis Poitrenaud

In Proceedings of the 41th IFIP international conference on formal techniques for distributed objects, components and systems (FORTE’22)

Abstract Verification of properties expressed as omega-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity.

Combining parallel emptiness checks with partial order reductions

By Denis Poitrenaud, Étienne Renault

2019-08-02

In Proceedings of the 21st international conference on formal engineering methods (ICFEM’19)

Abstract In explicit state model checking ofconcurrent systems, multicore emptiness checks and partial order reductions (POR) are two major techniques to handle large state spaces. The first one tries to take advantage of multi-core architectures while the second one may decrease exponentially the size of the state space to explore. For checking LTL properties, Bloemen and van de Pol [2] shown that the best performance is currently obtained using their multi-core SCC-based emptiness check.

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.

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.

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.

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.

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.

Self-loop aggregation product — a new hybrid approach to on-the-fly LTL model checking

By Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg

2011-06-23

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

Abstract We present the Self-Loop Aggregation Product (SLAP), a new hybrid technique that replaces the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed product is an explicit graph of aggregates (symbolic sets of states) that can be interpreted as a Büchi automata. The criterion used by SLAP to aggregate states from the Kripke structure is based on the analysis of self-loops that occur in the Büchi automaton expressing the property to verify.

Combining explicit and symbolic approaches for better on-the-fly LTL model checking

By Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg

2011-06-01

In

Abstract We present two new hybrid techniques that replace the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed products are explicit graphs of aggregates (symbolic sets of states) that can be interpreted as Büchi automata. These hybrid approaches allow on the one hand to use classical emptiness-check algorithms and build the graph on-the-fly, and on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates.

On-the-fly emptiness check of transition-based Streett automata

By Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur

2009-10-01

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

Abstract In the automata theoretic approach to model checking, checking a state-space $S$ against a linear-time property $\varphi$ can be done in $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|)})$ time. When model checking under $n$ strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|+n)})$.Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under $n$ strong fairness hypotheses in $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|)}\times n)$. We focus on transition-based Streett automata, because it allows us to express strong fairness hypotheses by injecting Streett acceptance conditions into the state-space without any blowup.

LTL under reductions with weaker conditions than stutter invariance

Combining parallel emptiness checks with partial order reductions

Heuristics for checking liveness properties with partial order reductions

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

Parallel explicit model checking for generalized Büchi automata

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

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

Self-loop aggregation product — a new hybrid approach to on-the-fly LTL model checking

Combining explicit and symbolic approaches for better on-the-fly LTL model checking

On-the-fly emptiness check of transition-based Streett automata

Search

Tags