From LTL to deterministic automata (A safraless compositional approach)

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ESPARZA Javier KŘETÍNSKÝ Jan SICKERT Salomon

Year of publication 2016
Type Article in Periodical
Magazine / Source Formal Methods in System Design
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/s10703-016-0259-2
Field Informatics
Keywords automata; verification; logic
Description We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula \phi. The automaton is the product of a co-Büchi automaton for \phi and an array of Rabin automata, one for each G-subformula of \phi. The Rabin automaton for G\psi is in charge of recognizing whether FG\psi holds. This information is passed to the co-Büchi automaton that decides on acceptance. As opposed to standard procedures based on Safra’s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.