Jan Strejček

Seminator 2 can complement generalized Büchi automata via improved semi-determinization

By František Blahoudek, Alexandre Duret-Lutz, Jan Strejček

2020-05-14

In Proceedings of the 32nd international conference on computer-aided verification (CAV’20)

Abstract

We present the second generation of the tool Seminator that transforms transition-based generalized Büchi automata (TGBAs) into equivalent semi-deterministic automata. The tool has been extended with numerous optimizations and produces considerably smaller automata than its first version. In connection with the state-of-the-art LTL to TGBAs translator Spot, Seminator 2 produces smaller (on average) semi-deterministic automata than the direct LTL to semi-deterministic automata translator ltl2ldgba of the Owl library. Further, Seminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automata, providing a new way to complement automata that is competitive with state-of-the-art complementation tools.

Continue reading

Generic emptiness check for fun and profit

By Christel Baier, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, Jan Strejček

2019-07-29

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

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

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

By František Blahoudek, Alexandre Duret-Lutz, Mikuláš Klokočka, Mojmír Křetínský, Jan Strejček

2017-04-03

In Proceedings of the 21th international conference on logic for programming, artificial intelligence, and reasoning (LP<AR’17)

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

On refinement of Büchi automata for explicit model checking

By František Blahoudek, Alexandre Duret-Lutz, Vojtčech Rujbr, Jan Strejček

2015-06-15

In Proceedings of the 22th international SPIN symposium on model checking of software (SPIN’15)

Abstract

In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand and, more importantly, for which the explicit model checking process performs better.

Continue reading

The Hanoi Omega-Automata format

By Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, Jan Strejček

2015-04-27

In Proceedings of the 27th international conference on computer aided verification (CAV’15)

Abstract

We propose a flexible exchange format for $\omega$-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.

Continue reading

Is there a best Büchi automaton for explicit model checking?

By František Blahoudek, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček

2014-06-16

In Proceedings of the 21th international SPIN symposium on model checking of software (SPIN’14)

Abstract

LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.

Continue reading

Compositional approach to suspension and other improvements to LTL translation

By Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček

2013-04-28

In Proceedings of the 20th international SPIN symposium on model checking of software (SPIN’13)

Abstract

Recently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show how existing simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton.

Continue reading

Search

Tags