Instructor:
Dr. A. Miner
Office: 233 Atanasoff Hall
Office Hours: By appointment
Lecture: MWF, 1:10 - 2, Gilman 1114
Text: None.
(References and lecture notes will be posted on
Blackboard.)
The course will focus on model checking theory and algorithms for a variety of models, including Kripke structures and Markov chains. Broadly speaking, topics to be covered include temporal operators, Kripke structures, computation tree logic (CTL), linear temporal logic (LTL), discrete-time Markov chains (DTMCs) numerical analysis of DTMCs, probabilistic CTL and LTL, high-level formalisms to describe systems, and advanced topics as time permits (Markov decision processes, continuous-time Markov chains, and decision diagrams). Coursework will be a mixture of theory and practice, including programming in C/C++.
If you have a disability that may require some modification of seating, testing, or other class requirements, please obtain a SAAR (Student Academic Accommodation Request) form verifying your disability and specifying the accommodation you will need from the Disability Resources staff and present it to the instructor as soon as possible so that appropriate arrangements may be made.
The lecture schedule, course assignments, grades, and other information can be found on Blackboard
Officially, the prerequisites are ComS 331, Math 307, and Stat 330 or equivalents. These are discussed below.
Students will be expected to have programming experience in a contemporary high-level language, such as C, C++, or Java (any example code will be given in C or C++). The use of dynamic structures (e.g., linked lists, queues, etc.) will be required. Course work will be unpleasant without a strong programming background.
Students should also have a working knowledge of algorithm complexity, and should be comfortable working with graph algorithms and finite automata (ComS 331).
Students should be familiar with basic boolean logic.
Students should have a working knowledge of probability, including random variables, expectation, and conditioning (Stat 330).
Homework exercises will be assigned regularly. These will include programming assignments, mathematical exercises, and applications. Problem sets are due by 11:59 pm on their due date, subject to the following lateness penalty:
Problem sets will represent about 40% of your grade.
There will be a midterm take-home exam, worth about 30% of your grade. This will be due at the precise time specified on the exam, and will not be accepted late without prior permission of the instructor.
Students may opt either for a take-home final exam, or a semester-long research project (requiring a written report) on a topic to be developed with the instructor. This will be due at the University-scheduled final exam time, and is worth about 30% of your grade. This will not be accepted late without prior permission of the instructor.
Solutions to problem sets and exam questions consist of two parts.
Hardcopy (written) solutions should consist of a self-contained explanation of your solution, complete with an overview of mathematical derivations (if necessary), algorithm development (if necessary), and/or specification models. The other student viewpoint is a guide to the level of explanation expected for written solutions: another student in the class, who didn't know how to do the exercise/question, should be able to read your solution and learn a correct answer, without asking questions. Solutions should be typeset using appropriate software. My personal preference is to use LaTeX as it produces excellent quality with minimal effort, especially for equations. However, content is much more important than style. Point(s) will be deducted for incomplete or poorly-written solutions. An example solution is provided below for illustration.
In addition to written solutions, you must submit a complete solution electronically (via Blackboard). Think of this as the appendix to your written solution, containing things like source code and raw data as appropriate. This is necessary for me to replicate your results and check for errors. Also, be sure to submit an electronic version of your hardcopy, preferably as a PDF.
Students enrolled in Computer Science courses at ISU are expected to maintain the highest standards of academic integrity. Cases of cheating that go undetected and hence unpunished skew the grading curve in a class, thereby lowering the grades for students who do not cheat. Students who cheat rob themselves not only of knowledge and skills that they should have acquired in a course, but also of the experience of learning how to learn, arguably the most valuable benefit of a university education. The reputation of the department, the university, and the value of the degree suffer if employers find the graduates of a program lacking in abilities that successful completion specific courses should guarantee. Most professions, including Computer Science, have codes of ethics or standards to which individuals will be expected to abide by. At the University you practice the integrity that you must demonstrate later.
Suspected cases of academic misconduct will be pursued fully in accordance with ISU policies which require that all suspected cases of academic misconduct be reported to the dean of students. Any student found responsible for academic misconduct will receive a failing grade (F) in the course (even if the student chooses to drop the course). The dean of students may impose additional sanctions (ranging from a disciplinary reprimand to expulsion from the university). You are strongly urged to consult the university's policy on academic dishonesty.
The information included here is intended to help students avoid unintentionally committing academic dishonesty. The primary purpose of problem sets is to clarify and enhance the understanding of the concepts covered in the lectures. Past experience with this course has shown that this is helped by increased interaction among students. Discussion of general concepts and questions concerning the homework and laboratory assignments among students is encouraged. However, each student is expected to work on the solutions individually (except in the case of assignments that are explicitly assigned to teams of students).
When discussing problems with other students, you may:
It is expected that you have independently arrived at solutions that you submit. The following are examples of activities that are PROHIBITED:
[1] The academic honesty policy has been compiled using material adapted from several sources including the past offerings of this course, other computer science courses at Iowa State University, as well as other universities.
Last updated $Date: 2012-01-03 13:32:55 -0600 (Tue, 03 Jan 2012) $