Automata over finite or infinite words or binary decision diagrams (BDDs) are ubiquitous in modern computer science, providing robust foundations for applications in automated reasoning, verification, information processing, etc. Applications based on these models usually largely benefit when the handled automata or BDDs are small, reducing memory requirements and improving the runtime of their processing. Recently, compact representations of automata based on extensions of the basic models started appearing, often in an ad hoc manner relevant for particular applications, with many basic questions unanswered and their full potential unexplored. One goal of the project is to fill the gap by designing novel, practically relevant, concise kinds of automata and algorithms for their efficient manipulation, and applications based on these automata. The second is to reduce the size of manipulated BDDs by combining them with approximative reasoning. By achieving these goals, the project aims to push the applicability and scalability of automata- and BDD-based tools to a new level.

Klíčová slova
formal languages;finite automata;automata over infinite words;omega-automata;Emerson-Lei automata;TELA;binary decision diagrams;BDD;partial BDD;approximation;complementation

26-22640S

angličtina

Lengál Ondřej, doc. Ing., Ph.D. - hlavní řešitel
Dacík Tomáš, Ing. - spoluřešitel
Havlena Vojtěch, Ing., Ph.D. - spoluřešitel

Ústav inteligentních systémů
- odpovědné pracoviště (24.3.2025 - nezadáno)
Ústav inteligentních systémů
- spolupříjemce (24.3.2025 - 31.12.2028)
Fakulta informatiky
- příjemce (24.3.2025 - 31.12.2028)

Odpovědnost: Lengál Ondřej, doc. Ing., Ph.D.