Hans-Jörg Peter

Atrenta Inc. 7 parvis Louis Neel 38040 Grenoble Cedex 9, France Phone: +33 4 38 12 05 91 ext. 440 Fax: +33 4 76 84 65 51 eMail: hans at atrenta.com

I finished my Ph.D. and moved to Grenoble, France, where I am now working in the Advanced Research Center of Atrenta Inc.

Before that, I was working as a research and teaching assistant in the Reactive Systems Group in the Computer Science Department at Saarland University, where I was also involved in the AVACS project (DFG SFB/TR 14). I was working in industry as co-founder of startup BPS IT-Solutions and as project and team leader at META-LEVEL Software AG.

Thesis

My 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 resource-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.

(pdf) (bib)

Publications

[PF12]	The Complexity of Bounded Synthesis for Timed Control with Partial Observability with Bernd Finkbeiner. FORMATS 2012.
[GEFP12]	FlexRay for Avionics: Automatic Verification with Parametric Physical Layers with Michael Gerke, Rüdiger Ehlers, and Bernd Finkbeiner. AIAA I@A 2012.
[FP12]	Template-based Controller Synthesis for Timed Systems with Bernd Finkbeiner. TACAS 2012.
[DPRW12]	Can We Build It: Formal Synthesis of Control Strategies for Cooperative Driver Assistance Systems with Werner Damm, Jan Rakow, and Bernd Westphal. Accepted in MSCS 2012.
[PEM11]	Synthia: Verification and Synthesis for Timed Automata with Rüdiger Ehlers and Robert Mattmüller. CAV 2011.
[EFGP10]	Fully Symbolic Timed Model Checking using Constraint Matrix Diagrams with Rüdiger Ehlers, Daniel Fass, and Michael Gerke. RTSS 2010.
[EGP10]	Making the Right Cut in Model Checking Data-Intensive Timed Systems with Rüdiger Ehlers and Michael Gerke. ICFEM 2010.
[GEFP10]	Model Checking the FlexRay Physical Layer Protocol with Michael Gerke, Rüdiger Ehlers, and Bernd Finkbeiner. FMICS 2010.
[EMP10]	Combining Symbolic Representations for Solving Timed Games with Rüdiger Ehlers and Robert Mattmüller. FORMATS 2010.
[FPS10]	Synthesising Certificates in Networks of Timed Automata with Bernd Finkbeiner and Sven Schewe. IET-Software, June 2010, Volume 4, Issue 3, Automated compositional verification.
[PM09]	Component-based Abstraction Refinement for Timed Controller Synthesis with Robert Mattmüller. RTSS 2009.
[FPS08b]	Synthesizing Certificates in Networks of Timed Automata with Bernd Finkbeiner and Sven Schewe. RTSS 2008.
[FPS08a]	RESY: Requirement Synthesis for Compositional Model Checking with Bernd Finkbeiner and Sven Schewe. TACAS 2008.
[Pet05]	Controller Program Synthesis for Industrial Machines Diploma Thesis 2005. Won the Software-Engineering-Prize 2006 of the Ernst-Denert-Foundation.

Teaching

WS 2010/11	Core lecture teaching assistant Embedded Systems.
WS 2008/09	Core lecture teaching assistant Embedded Systems.
SS 2008	Seminar adviser Games in Verification and Synthesis.
SS 2006	Proseminar adviser The Time Machine.

Student Projects

[Ger10]	Zone State Diagrams – Model Checking Data-Intensive Real-Time Systems. Master Thesis by Michael Gerke.
[Fas10]	Fully Symbolic Model Checking using Constraint Matrix Diagrams. Master Thesis by Daniel Fass.
[Fas09]	Clock Matrix Diagrams. Bachelor Thesis by Daniel Fass.
[Bau07]	Symbolic Game Solving with Arithmetic Data Types. Bachelor Thesis by Martin Bauer.

Miscellaneous

Blumen Raber is a great place for flowers and all kinds of nice stuff.