Campus Event Calendar
Event Entry
What and Who
Reactive Synthesis
Prof. Dr. Bernd Finkbeiner
Fachrichtung Informatik - Saarbrücken
Ringvorlesung
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 5 February 2009
13:00
120 Minutes
E1 3 - Hörsaal Gebäude
0.16
Saarbrücken
Abstract
Reactive synthesis transforms a logical specification into a concurrent
implementation that is guaranteed to satisfy the specification. In this
talk I will describe two approaches for synthesis from linear-time
temporal logic. The first solution, based on automata-theoretic
transformations, provides a uniform synthesis algorithm for all
distributed system architectures for which the realizability question is
decidable, but has nonelementary complexity. The second solution reduces
synthesis to a satisfiability problem, where the existence of an
implementation is specified as a quantified formula in the theory (N,<)
of the ordered natural numbers with uninterpreted function symbols. The
second solution also has nonelementary complexity in the size of the
specification, but becomes tractable if we fix an upper bound on the
number of states in the implementatíon. By iteratively increasing the
bound, we obtain an effective semialgorithm for reactive synthesis. The
talk is based on joint work with Sven Schewe.
implementation that is guaranteed to satisfy the specification. In this
talk I will describe two approaches for synthesis from linear-time
temporal logic. The first solution, based on automata-theoretic
transformations, provides a uniform synthesis algorithm for all
distributed system architectures for which the realizability question is
decidable, but has nonelementary complexity. The second solution reduces
synthesis to a satisfiability problem, where the existence of an
implementation is specified as a quantified formula in the theory (N,<)
of the ordered natural numbers with uninterpreted function symbols. The
second solution also has nonelementary complexity in the size of the
specification, but becomes tractable if we fix an upper bound on the
number of states in the implementatíon. By iteratively increasing the
bound, we obtain an effective semialgorithm for reactive synthesis. The
talk is based on joint work with Sven Schewe.
Contact
imprs
225
--email hidden
passcode not visible
logged in users only
Jennifer Gerling, 02/03/2009 09:54 -- Created document.