Abstract
Complex computer systems play an important role in every part of everyday life
and their correctness is often vital to human safety. In light of the recent
advances in the area of formal methods and the increasing availability and
maturity of tools and techniques, the use of verification techniques to show
that a system satisfies a specified property is about to become an integral
part of the development process. To minimize the development costs, formal
methods must be applied as early as possible, before the entire system is fully
developed, or even at the stage when only its specification is available. The
goal of synthesis is to automatically construct an implementation guaranteed to
fulfill the provided specification, and, if no implementation exists, to report
that the given requirements cannot be realized. When synthesizing an individual
component within a system and its external environment, the synthesis procedure
must take into account the component�s interface and deliver implementations
that comply with it. 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. This thesis presents
novel synthesis methods that respect the given interface limitations of the
synthesized system components and are applicable to infinite-state models. The
studied computational model is that of infinite-state two-player games under
incomplete information. The contributions are structured into three parts,
corresponding to a classification of such games according to the interface
between the synthesized component and its environment.
In the first part, we obtain decidability results for a class of game
structures where the player corresponding to the synthesized component has a
given finite set of possible observations and a finite set of possible actions.
A prominent type of systems for which the interface of a component naturally
defines a finite set of observations are Lossy Channel Systems. We provide
symbolic game solving and strategy synthesis algorithms for lossy channel games
under incomplete information with safety and reachability winning conditions.
Our second contribution is a counterexample-guided abstraction refinement
scheme for solving infinite-state under incomplete information in which the
actions available to the component are still finitely many, but no finite set
of possible observations is given. This situation is common, for example, in
the synthesis of mutex protocols or robot controllers. In this setting, the
observations correspond to observation predicates, which are logical formulas,
and their computation is an integral part of our synthesis procedure. The
resulting game solving method is applicable to games that are out of the scope
of other available techniques. Last we study systems in which, in addition to
the possibly infinite set of observation predicates, the component can choose
between infinitely many possible actions. Timed games under incomplete
information are a fundamental class of games for which this is the case. We
extend the abstraction-refinement procedure to develop the first systematic
method for the synthesis of observation predicates for timed control.
Automatically refining the set of candidate observations based on
counterexamples demonstrates better potential than brute-force enumeration of
observation sets, in particular for systems where fine granularity of the
observations is necessary.
