Item

Abstract

This thesis provides a unifying view on the succinctness of systems: the
capability of a modeling formalism to describe the behavior of a system of
exponential size using a polynomial syntax.
The key theoretical contribution is the introduction of sequential circuit
machines as a new universal computation model that focuses on succinctness
as the central aspect. The thesis demonstrates that many well-known modeling
formalisms such as communicating state machines, linear-time temporal
logic, or timed automata exhibit an immediate connection to this
machine model. Once a (syntactic) connection is established, many complexity
bounds for structurally restricted sequential circuit machines can be
transferred to a certain formalism in a uniform manner. As a consequence,
besides a far-reaching unification of independent lines of research, we are
also able to provide matching complexity bounds for various analysis problems,
whose complexities were not known so far. For example, we establish
matching lower and upper bounds of the small witness problem and several
variants of the bounded synthesis problem for timed automata, a particularly
important succinct modeling formalism.
Also for timed automata, our complexity-theoretic analysis leads to the
identification of tractable fragments of the timed synthesis problem under
partial observability. Specifically, we identify timed controller synthesis
based on discrete or template-based controllers to be equivalent to model
checking. Based on this discovery, we develop a new model checking-based
algorithm to efficiently find feasible template instantiations.
From a more practical perspective, this thesis also studies the preservation
of succinctness in analysis algorithms using symbolic data structures.
While efficient techniques exist for specific forms of succinctness considered
in isolation, we present a general approach based on abstraction refinement
to combine off-the-shelf symbolic data structures. In particular, for handling
the combination of concurrency and quantitative timing behavior in
networks of timed automata, we report on the tool Synthia which combines
binary decision diagrams with difference bound matrices. In a comparison
with the timed model checker Uppaal and the timed game solver Uppaal-
Tiga running on standard benchmarks from the timed model checking and
synthesis domain, respectively, the experimental results clearly demonstrate
the effectiveness of our new approach.