11th Asian School on Computer Science

Date : 13-15 December, 1999 (post- ASIAN'99)
Where : Prince of Songkhla University (Phuket Campus) Phuket, Thailand
Title : Automata and Circuit
Contact : Kanchana Kanchanasut <kk@cs.ait.ac.th>

Arithmetic Circuit Design
Explicit and Inplicit Automata
Verification by Model-Checking

Registration Fee:

3,000 THB (coffee breaks and lunch included)

Accommodation:

ASIAN'99 accommodation rates are applicable to attendees for the Asian School.
The Prince of Sogkhla University also provides comfortable
accommodation on campus at a very reasonable rate.

Title: Arithmetic Circuit Design
Speaker: Jean Vuillemin, Ecole Normale Superieure

Digital synchronous circuits DSC provide a mathematical representation for a wide class of electronic circuits. As such, they present the most efficient known implementations for algorithms at large.

In a first part, we review the known correspondances between DSC, automata and BDD, through their truth-tables. Basic circuit synthesis techniques follow, and links are made with the other two topics.

The rest specializes in the construction of basic arithmetic circuits (add, subtract, multiply and divide), in relation with bit-ordering (low to high, high to low) and carry rules. Systematic time/space tradeoffs are constructed. The theory is presented through actual applications, arising from image processing and high energy detectors.

Title: Explicit and Inplicit Automata
Speaker: Gerard Berry, Ecole des Mines de Paris and INRIA

Finite automata are one of the most fundamental structures of Computer Science. They have been extensively studied in several contexts: language theory, hardware circuits design, process calculi, reactive systems, etc. Our aim is to present a modern course on automata encompassing all these aspects.

In the first part, we review the classical properties of deterministic and non-deterministic automata, and we study in depth the translation from various kinds of regular expressions into automata. This translation is essential for most of the linguistic developments based on automata, such as reactive languages. Then, we study the implicit presentation of automata as Boolean functions and we present various normal forms for sequential functions. This parts links the course with both arithmetic circuit design and verification.

Title: Verification by Model-Checking
Speaker: Nicolas Halbwachs, Verimag/CNRS

We survey the basic techniques for verifying properties of logical systems (circuits, automata) by exploring their state space. These techniques are now of common usage in hardware verification, and their use for software becomes more and more important.

A first part is devoted to the verification of safety properties (something "bad" never happens), which can be verified by traversing the reachable (or unreachable) states of the system. This traversal can be done enumeratively, or symbolically (by encoding sets of states by means of Binary Decision Diagrams).

In a second part, we consider general properties, expressed in the temporal logic CTL. We show how the (BDD of the) set of states satisfying a CTL formula can be computed.