Alexandre Duret-Lutz

Generic emptiness check for fun and profit

Abstract

We present a new algorithm for checking the emptiness of $\omega$-automata with an Emerson-Lei acceptance condition (i.e., a positive Boolean formula over sets of states or transitions that must be visited infinitely or finitely often). The algorithm can also solve the model checking problem of probabilistic positiveness of MDP under a property given as a deterministic Emerson-Lei automaton. Although both these problems are known to be NP-complete and our algorithm is exponential in general, it runs in polynomial time for simpler acceptance conditions like generalized Rabin, Streett, or parity. In fact, the algorithm provides a unifying view on emptiness checks for these simpler automata classes. We have implemented the algorithm in Spot and PRISM and our experiments show improved performance over previous solutions.

Continue reading

Model checking with generalized Rabin and Fin-less automata

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. With recent advances in probabilistic model checking and LTL to TGRA translators, it is only natural to ask whether checking a TGRA directly is more advantageous in practice.We designed a multi-core TGRA checking algorithm and performed experiments on a subset of the models and formulas from the 2015 Model Checking Contest and generated LTL formulas for models from the BEEM database. While we found little to no improvement by checking TGRAs directly, we show how various aspects of a TGRA’s structure influences the model checking performance.In this paper, we also introduce a Fin-less acceptance condition, which is a disjunction of TGBAs. We show how to convert TGRAs into automata with Fin-less acceptance and show how a TGBA emptiness procedure can be extended to check Fin-less automata.

Continue reading

Parallel model checking algorithms for linear-time temporal logic

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. We discuss several parallel algorithms that attack this problem in various ways, each with different characteristics: Depth-first search (DFS) based algorithms rely on heuristics for good parallelization, but exhibit a low complexity and good on-the-fly behavior. Breadth-first search (BFS) based approaches, on the other hand, offer good parallel scalability and support distributed parallelism. In addition, we present various simpler model checking tasks, which still solve a large and important subset of the LTL model checking problem, and show how these can be exploited to yield more efficient algorithms. In particular, we provide simplified DFS-based search algorithms and show that the BFS-based algorithms exhibit optimal runtimes in certain cases.

Continue reading

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

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. With recent advances in probabilistic model checking and LTL to TGRA translators, it is only natural to ask whether checking a TGRA directly is more advantageous in practice.We designed a multi-core TGRA checking algorithm and performed experiments on a subset of the models and formulas from the 2015 Model Checking Contest. We observed that our algorithm can be used to replace a TGBA checking algorithm without losing performance. In general, we found little to no improvement by checking TGRAs directly.

Continue reading

Seminator: A tool for semi-determinization of omega-automata

Abstract

We present a tool that transforms nondeterministic $\omega$-automata to semi-deterministic $\omega$-automata. The tool Seminator accepts transition-based generalized Büchi automata (TGBA) as an input and produces automata with two kinds of semi-determinism. The implemented procedure performs degeneralization and semi-determinization simultaneously and employs several other optimizations. We experimentally evaluate Seminator in the context of LTL to semi-deterministic automata translation.

Continue reading

Contributions to LTL and $\omega$-automata for model checking

Abstract

Continue reading

Heuristics for checking liveness properties with partial order reductions

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

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

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

SAT-based minimization of deterministic $\omega$-automata

Abstract

We describe a tool that inputs a deterministic $\omega$-automaton with any acceptance condition, and synthesizes an equivalent $\omega$-automaton with another arbitrary acceptance condition and a given number of states, if such an automaton exists. This tool, that relies on a SAT-based encoding of the problem, can be used to provide minimal $\omega$-automata equivalent to given properties, for different acceptance conditions.

Continue reading