Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Masterat
Domeniul: Informatica
Programul de studii: Metode formale în programare - în limba engleză
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MML1015	Temporal Logic	

Semester	Hours: C+S+L	Category	Status	
2	2+2+0	speciality	compulsory	

II. Full status faculty members
Name and	Scientific	Didactic	Chair	Type of activity	
surname	title	title		C	S	L	
BREAZ Simion Sorin	Ph.D.	Assoc.Prof.	Algebra	*			

Associated faculty members
Name and	Scientific	Institution	Type of	Type of activity	
surname	title		position	C	S	L	

III. Course objectives
We will present basic facts on Temporal Logic and applications in formal programming. By the graduation of this class, the students will get the following competences:
 - Understanding the syntax and semantics in Temporal Logic
 - Using temporal properties
 - Realizing algorithmic verifications that a given logic formula holds in a given structure
 - Using formal execution sequences and Temporal Logic&#8217;s  objects in Programming

IV. Course contents
 1.Concepts and notions in Classical Logic.
 2.Propositional Temporal Logic. Language and semantics.
 3.Propositional Temporal Logic. Laws and Operators.
 4.Axiomatization of Propositional Temporal Logic.
 5.First order Temporal Logic.
 6.Programs. Execution Sequences.
 7.Program Axioms and Program Properties.
 8.Basic Invariant Method. Applications.
 9.Invariant Methods for Precedente Properties. Applications.
10. Fair Execution Sequences. The Finite Chain Reasoning Method.
11.Well-Founded Orderings.
12.Special Methods for Sequential Programs.

V. Bibliography
1.Chomicki, J., Toman, D.: Temporal Logic in Information Systems, BRICS Lecture Series, 1997.

2.Kroger, F.: Temporal Logic and Programs, Springer-Verlag, 1987.

3. Breaz, S., Covaci, R.: Elemente de logica matematica, teoria multimilor si aritmetica, editura EFES, 2006.

VI. Thematic of didactic activities per weeks

VII. Didactic methods used

VIII. Assessment
A written final exam (grade E), a test at the seminar (grade T) and a referee (R). The exam subjects have theoretical questions from all the studied topics, and one problem, among the problems studied at the course and last 4 seminars. The test subject have
practical questions (exercices and problems) from topics which are studied in first 10 weeks. The final grade is the weighted mean of the three grades mentioned above, conditioned by all the grades being at least 5 from 10. Otherwise, the exam will not be passed.
The final grade = 50%E + 25%T + 25%R.

IX. Additional references

	Dean,							Chair head,

	Date,							Course responsible,
								Assoc.Prof. BREAZ Simion Sorin, Ph.D.