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.