Denis Poitrenaud

LTL under reductions with weaker conditions than stutter invariance

By Emmanuel Paviot-Adet, Denis Poitrenaud, Étienne Renault, Yann Thierry-Mieg

2022-04-18

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. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton’s transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. An implementation and experimental evidence is provided showing most non- random properties sensitive to stutter are actually shortening or lengthening in- sensitive. Performance of experiments on a large (random) benchmark from the model-checking competition indicate that despite being a semi-decision proce- dure, the approach can still improve state of the art verification tools. 1 Introduction Model checking is an automatic verification technique for proving the correctness of systems that have finite state abstractions. Properties can be expressed using the popular Linear-time Temporal Logic (LTL). To verify LTL properties, the automata-theoretic approach [25] builds a product between a Buchi automaton representing the negation of the LTL formula and the reachable state graph of the system (seen as a set of infinite runs). This approach has been used successfully to verify both hardware and software components, but it suffers from the so called “state explosion problem”: as the number of state variables in the system increases, the size of the system state space grows exponentially.

Continue reading

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. However, combining the latest SCC-based algorithm with POR is not trivial since a condition on cycles, the proviso, must be enforced on an algorithm which processes collaboratively cycles. In this paper, we suggest a pessimistic approach to tackle this problem for liveness properties. For safety ones, we propose an algorithm which takes benefit from the information computed by the SCC-based algorithm. We also present new parallel provisos for both safety and liveness prop- erties that relies on other multi-core emptiness checks. We observe that all presented algorithms maintain good reductions and scalability.

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

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. The results from an extensive experimentation of our algorithms and their variations show encouraging performances, especially when the decomposition technique is used.

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

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. This leads us to define two new emptiness check algorithms (one of them based on the Union Find data structure), introduce new optimizations, and show that one of these can be of benefit to a classic SCCs enumeration algorithm. We have implemented all these variants to compare their relative performances and the overhead induced by the emptiness check compared to the corresponding SCCs enumeration algorithm. Our experiments shows that these three algorithms are comparable.

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. The three corresponding emptiness checks can be performed independently, using the most appropriate algorithm. Such a decomposition approach can be used with any automata-based model checker. We illustrate the interest of this new approach using explicit and symbolic LTL model checkers.

Continue reading

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. Our hybrid approach allows 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. Our experiments show that this technique often outperforms other existing (hybrid or fully symbolic) approaches.

Continue reading

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. The Symbolic Observation Product assumes a globally stuttering property (e.g., LTL-X) to aggregate states. The Self-Loop Aggregation Product does not require the property to be globally stuttering (i.e., it can tackle full LTL), but dynamically detects and exploits a form of stuttering where possible. Our experiments show that these two variants, while incomparable with each other, can outperform other existing approaches.

Continue reading

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.

Continue reading

Search

Tags