Concise Models for Efficient Reasoning

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.