THE UNIVERSITY of EDINBURGH

DEGREE REGULATIONS & PROGRAMMES OF STUDY 2011/2012

University Homepage
DRPS Homepage
DRPS Search
DRPS Contact
DRPS : Course Catalogue : School of Informatics : Informatics

Postgraduate Course: Logic and Automata (Level 11) (INFR11051)

Course Outline
School School of Informatics College College of Science and Engineering
Course type Standard Availability Not available to visiting students
Credit level (Normal year taken) SCQF Level 11 (Postgraduate) Credits 10
Home subject area Informatics Other subject area None
Course website http://www.inf.ed.ac.uk/teaching/courses/la/ Taught in Gaelic? No
Course description 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 Co-requisites
Prohibited Combinations Students MUST NOT also be taking Logic and Automata (Level 10) (INFR10030)
Other requirements For Informatics PG and final year MInf students only, or by special permission of the School. Informatics 2D is strongly recommended.

Students should understand the following topics:

Computation: the definition as acceptor and transducer, deterministic/non deterministic machines, regular expressions, operations on FSMs

Propositional and predicate logic

Context-free languages and Push-down automata

Turing machines and computability
Additional Costs None
Course Delivery Information
Not being delivered
Summary of Intended Learning Outcomes
1 - 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.
2 - Students will be able to translate logical specifications into automata;
3 - Students will know how to solve decision problems for
different types of automata and their complexity.
4 - 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.
5 - Students will know how logical and automata formalisms
influence the design of XML schemas and query languages.
6 - Students will learn how automata provide algorithms for
deciding logical theories, and how these decision procedures are used in practice.
Assessment Information
Written Examination 0
Assessed Assignments 75
Oral Presentations 25

Three sets of exercises, worth 5% each.
Two assignments, worth 30% each.
Special Arrangements
None
Additional Information
Academic description Not entered
Syllabus Topics include:

- automata on finite strings - First-order, Second-order, and Monadic Second-order logics - Buchi's theorem, automata/logic connection - First-order logic on strings, star-free languages - Tree automata on finite trees, Thatcher-Wright theorem - Automata over unranked trees, XML applications - Infinite strings and logics over them - Automata over infinite strings; closure properties; logical characterisation - First-order over infinite words, temporal logics, verification problems - LTL to automata translation - Alternating automata, decision problems, connections with LTL - Automata over infinite trees - Rabin's theorem - Decidability of logical theories; applications in software verification

Relevant QAA Computing Curriculum Sections: Not yet available
Transferable skills Not entered
Reading list Not yet available
Study Abroad Not entered
Study Pattern Lectures 18
Tutorials 0
Timetabled Laboratories 0
Non-timetabled assessed assignments 38
Private Study/Other 44
Total 100
Keywords Not entered
Contacts
Course organiser Dr Michael Rovatsos
Tel: (0131 6)51 3263
Email: mrovatso@inf.ed.ac.uk
Course secretary Miss Kate Weston
Tel: (0131 6)50 2701
Email: Kate.Weston@ed.ac.uk
Navigation
Help & Information
Home
Introduction
Glossary
Search DPTs and Courses
Regulations
Regulations
Degree Programmes
Introduction
Browse DPTs
Courses
Introduction
Humanities and Social Science
Science and Engineering
Medicine and Veterinary Medicine
Other Information
Timetab
Prospectuses
Important Information
 
copyright 2011 The University of Edinburgh - 3 April 2011 11:21 am