A co-Büching Toolbox

From LRDE

Revision as of 17:05, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Alexandre Gbaguidi Aïsse | title = A co-Büching Toolbox | year = 2017 | number = 1705 | abstract = Thanks to the HOA format there are less and less b...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

Thanks to the HOA format there are less and less barriers between -automata with different acceptance conditions. Spot, a library for -automata manipulation, supports arbitrary acceptance condition and performs some conversions between them. We augmented the set of supported acceptance conversions with new algorithms that convert (when possible) all common classes of non deterministic -automata to deterministic co-Büchi. Boker and Kupferman solved this conversion whith asymptotically tight constructions. We implement their methods with some optimizations and adjustments: we made it work with Streett-like acceptance, any acceptance in disjunctive normal form (including Rabin-like) and also transition-based acceptance. Using these conversions gives a new way to check whether an LTL formula is a persistence formula.