We study decision procedures for the equivalence of regular languages represented as regular expressions or logical formulas. Traditional algorithms in this context dispose of this symbolic representation by translating it into finite automata, which then are minimized and checked for structural equality. We develop concise algorithms that avoid this explicit translation by working with the symbolic structures directly. Our procedures are specified and proved correct in the proof assistant Isabelle.     «

We study decision procedures for the equivalence of regular languages represented as regular expressions or logical formulas. Traditional algorithms in this context dispose of this symbolic representation by translating it into finite automata, which then are minimized and checked for structural equality. We develop concise algorithms that avoid this explicit translation by working with the symbolic structures directly. Our procedures are specified and proved correct in the proof assistant Isab...     »

Wir beschäftigen uns mit Entscheidungsprozeduren für die Äquivalenz regulärer Sprachen, die durch reguläre Ausdrücke oder logische Formeln dargestellt sind. Traditionelle Algorithmen hierfür entledigen sich dieser symbolischen Darstellung, indem sie sie in endliche Automaten übersetzen, welche anschließend minimiert und auf strukturelle Gleichheit überprüft werden. Wir entwickeln kompakte funktionale Algorithmen, die diese explizite Übersetzung vermeiden und stattdessen mit der symbolischen Darstellung arbeiten. Unsere Entscheidungsprozeduren sind in dem Theorembeweiser Isabelle spezifiziert und ihre Korrektheit ist formal verifiziert.     «

Wir beschäftigen uns mit Entscheidungsprozeduren für die Äquivalenz regulärer Sprachen, die durch reguläre Ausdrücke oder logische Formeln dargestellt sind. Traditionelle Algorithmen hierfür entledigen sich dieser symbolischen Darstellung, indem sie sie in endliche Automaten übersetzen, welche anschließend minimiert und auf strukturelle Gleichheit überprüft werden. Wir entwickeln kompakte funktionale Algorithmen, die diese explizite Übersetzung vermeiden und stattdessen mit der symbolischen Dars...     »