Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden.
powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden.
powered by
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.
×
Anzeige
Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.
Readers familiar with LTL can interpret Inf(s), Fin(s), Inf(!s), Fin(!s) as meaning \(\mathsf {G}\mathsf {F}p_s\), \(\mathsf {F}\mathsf {G}\lnot p_s\), \(\mathsf {G}\mathsf {F}\lnot p_s\), \(\mathsf {F}\mathsf {G}p_s\), where \(p_s\) is the property “belongs to set s”.
