Logic and Automata (Level 11) (P02181)

? Credit Points : 10 ? SCQF Level : 11 ? Acronym : INF-P-LA

Automata are a natural procedural counterpart of declarative, or logical formalisms that appear in various areas of computer science. The most visible applications of the logic/automata connections are in the areas of formal verification, XML, and decidability of logical theories. In verification, automata are used to reason about infinite computations; in XML, they are used to specify and transform tree-structured documents.

While all computer scientists see finite-state automata over strings, it is other types of automata that are commonly used in applications nowadays: they differ in structures over which they run (strings or trees, finite or infinite), and the mode of running (deterministic, nondeterministic, alternating).

The course is about these models of automata, their logical counterparts, and applications of the logic/automata connections in various areas of computer science.

Entry Requirements

? Pre-requisites : Informatics 1A Informatics 2A Knowledge of: deterministic and nondeterministic automata on finite strings; context-free grammars; first-order propositional and predicate logic; basic complexity theory; basics of algorithms

? Prohibited combinations : Logic and Automata (Level 10)

Subject Areas

Home subject area

Theoretical Computer Science, (School of Informatics, Schedule O)

Delivery Information

? Normal year taken : Postgraduate

? Delivery Period : Semester 2 (Blocks 3-4)

? Contact Teaching Time : 2 hour(s) per week for 10 weeks

First Class Information

Date	Start	End	Room	Area	Additional Information
08/01/2007	16:10	18:00			Appleton Tower Room 2.02

All of the following classes

Type	Day	Start	End	Area
Lecture	Monday	16:10	18:00	Central

Summary of Intended Learning Outcomes

This course is to expose students to the rich connections between declarative (logical) and procedural (automata) formalisms used in various areas of computer science. There will be several learning outcomes:
- Students will be able to identify different models of automata, in particular, automata on finite trees, infinite strings, infinite trees, as well as different running modes of automata: deterministic, nondeterministic, alternating.
- Students will be able to translate logical specifications into automata;
- Students will know how to solve decision problems for different types of automata and their complexity.
- Students will know how to use logical formalisms and automata in specifying software and hardware properties, and how to use automata decision problems for solving verification problems.
- Students will know how logical and automata formalisms influence the design of many features of XML description and query languages.
- Students will learn how automata provide algorithms for deciding logical theories, and how these decision procedures are used in practice.