Arrow Research search

Author name cluster

Jan Strejček

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers
1 author row

Possible papers

7

Highlights Conference 2024 Conference Abstract

Tighter Construction of Tight Büchi Automata

  • Jan Strejček

Tight automata are useful in providing the shortest counterexample in LTL model checking and also in constructing a maximally satisfying strategy in LTL strategy synthesis. There exists a translation of LTL formulas to tight Büchi automata and several translations of Büchi automata to equivalent tight Büchi automata. This paper presents another translation of Büchi automata to equivalent tight Büchi automata. The translation is designed to produce smaller tight automata and it asymptotically improves the best-known upper bound on the size of a tight Büchi automaton equivalent to a given Büchi automaton. We also provide a lower bound, which is more precise than the previously known one. Further, we show that automata reduction methods based on quotienting preserve tightness. Our translation was implemented in a tool called Tightener. Experimental evaluation shows that Tightener usually produces smaller tight automata than the translation from LTL to tight automata known as CGH. The talk is based on a paper presented at FoSSaCS 2024 and co-authored by Marek Jankola.

Details

Highlights Conference 2020 Conference Abstract

Advances in Emerson-Lei Automata

  • Jan Strejček

The talk presents two new results on Emerson-Lei automata. One is a new LTL to automata translator called ltl3tela. The tool produces nondeterministic or deterministic transition-based Emerson-Lei automata that are (on average) smaller than automata produced by state-of-the art translators. The second result is a new algorithm checking emptiness of Emerson-Lei automata. The algorithm has been implemented in Spot and PRISM and our experiments exhibit great performance improvements over previous solutions.

Details

Highlights Conference 2016 Conference Abstract

Complementing Semi-Deterministic Büchi Automata

  • Joint with Matthias Heizmann
  • Sven Schewe
  • Jan Strejček
  • Ming-Hsien Tsai.

We introduce an efficient complementation technique for semi-deterministic Büchi automata, which are Büchi automata that are deterministic in the limit: from every accepting state onward, their behaviour is deterministic. It is interesting to study semi-deterministic automata, because they play a role in practical applications of automata theory, such as the analysis of Markov decision processes. Our motivation to study their complementation comes from the termination analysis implemented in Ultimate Büchi Automizer, where these automata represent checked runs and have to be complemented to identify runs to be checked. We show that semi-determinism leads to a simpler complementation procedure. Our complementation is based on an extended breakpoint construction that allows for symbolic implementation. It also leads to significantly improved bounds as the complement of a semi-deterministic automaton with states has less than states. Moreover, the resulting automaton is unambiguous, which again offers new applications, like the analysis of Markov chains. We also motivate and present an on-the-fly modification of our complementation, which does not need to know the whole automaton before the complementation starts, which is a crucial property for Ultimate Büchi Automizer that uses implicitly encoded automata. The price for the on-the-fly approach is a slightly worse upper bound on the size of the produced automaton for the complement: it has less than 5^n states. We have evaluated our construction against the semi-deterministic automata produced by Ultimate Büchi Automizer applied to programs of the Termination category of the software verification competition SV-COMP 2015. We complemented these automata by our algorithm and by four standard complementation constructions and compare the resulting automata. The evaluation confirms that our algorithm outperforms the known complementation techniques that work for general nondeterministic Büchi automata. The presentation is based on the identically titled paper published at TACAS 2016.

Details

Highlights Conference 2013 Conference Abstract

Effective translation of LTL to deterministic Rabin automata: Beyond the (F, G)-fragment

  • Tomáš Babiak
  • František Blahoudek
  • Mojmir Kretinsky
  • Jan Strejček

Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to LTL(F, G) which is the LTL fragment using only modalities F and G. We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F, G). Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae.

PDF Details