29 citations · 40 across the 4 of their papers we have counts for
7 papers
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
Salomon Sickert, Javier Esparza
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formu…
The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results
Swen Jacobs, Roderick Bloem, Maximilien Colange +11
We report on the fifth reactive synthesis competition (SYNTCOMP 2018). We introduce four new benchmark classes that have been added to the SYNTCOMP library, and briefly describe th…
Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games
Michael Luttenberger, Philipp J. Meyer, Salomon Sickert
The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of…
LTL Store: Repository of LTL formulae from literature and case studies
Jan Křetínský, Tobias Meggendorfer, Salomon Sickert
This continuously extended technical report collects and compares commonly used formulae from the literature and provides them in a machine readable way.
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
Javier Esparza, Jan Kretinsky, Salomon Sickert
We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield…
LTL to Deterministic Emerson-Lei Automata
David Müller, Salomon Sickert
We introduce a new translation from linear temporal logic (LTL) to deterministic Emerson-Lei automata, which are omega-automata with a Muller acceptance condition symbolically expr…