Campus Event Calendar
Event Entry
What and Who
Synthesis and Control of Infinite-State Systems with Partial ObservabilitySpeaker
Rayna Dimitrova
UdS
SWS Colloquium
Rayna Dimitrova is a PhD candidate at Saarland University working with Prof Bernd Finkbeiner
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, 18 April 2013
11:00
60 Minutes
G26
206
Kaiserslautern
Abstract
Synthesis methods automatically construct a system, or an individual
component within a system, such that the result satisfies a given
specification. The synthesis procedure must take into account the
component's interface and deliver implementations that comply with its
limitations. For example, what a component can observe about its
environment may be restricted by imprecise sensors or inaccessible
communication channels. In addition, sufficiently precise models of a
component's environment are typically infinite-state, for example due to
modeling real time or unbounded communication buffers. In this talk I
will present synthesis methods for infinite-state systems with partial
observability. First, I will describe a technique for automatic
generation of observation predicates (clock constraints) for timed
control with safety requirements. Finding the right observations is the
main challenge in timed control with partial observability. Our approach
follows the Counterexample-Guided Abstraction Refinement scheme, i.e.,
it uses counterexamples to guide the search. It employs novel refinement
techniques based on interpolation and model generation. Our approach
yields encouraging results, demonstrating better performance than
brute-force enumeration of observation sets, in particular for systems
where a fine granularity of the observations is necessary. Second, I
will outline a synthesis algorithm for Lossy Channel Systems (LCSs) with
partial observability and safety specifications. The algorithm uses an
extension of the symbolic representation common for backward analysis of
LCSs. Its termination relies on the fact that LCSs are better-quasi
ordered systems.
component within a system, such that the result satisfies a given
specification. The synthesis procedure must take into account the
component's interface and deliver implementations that comply with its
limitations. For example, what a component can observe about its
environment may be restricted by imprecise sensors or inaccessible
communication channels. In addition, sufficiently precise models of a
component's environment are typically infinite-state, for example due to
modeling real time or unbounded communication buffers. In this talk I
will present synthesis methods for infinite-state systems with partial
observability. First, I will describe a technique for automatic
generation of observation predicates (clock constraints) for timed
control with safety requirements. Finding the right observations is the
main challenge in timed control with partial observability. Our approach
follows the Counterexample-Guided Abstraction Refinement scheme, i.e.,
it uses counterexamples to guide the search. It employs novel refinement
techniques based on interpolation and model generation. Our approach
yields encouraging results, demonstrating better performance than
brute-force enumeration of observation sets, in particular for systems
where a fine granularity of the observations is necessary. Second, I
will outline a synthesis algorithm for Lossy Channel Systems (LCSs) with
partial observability and safety specifications. The algorithm uses an
extension of the symbolic representation common for backward analysis of
LCSs. Its termination relies on the fact that LCSs are better-quasi
ordered systems.
Contact
Susanne Rock
0631-9303-9600
--email hidden
Video Broadcast
Yes
Saarbrücken
E1 5
029
passcode not visible
logged in users only
Susanne Rock, 04/16/2013 13:23 -- Created document.