Address

Jakob-Haringer-Str. 2

5020 Salzburg, Austria


Room 2.17


Phone

+43 (0)662 8044 6417

+43 (0)662 8044 611 (fax)


Skype ana_sokolova

Home

Papers

Talks

Teaching

Personal

Many thanks to Silviu Craciunas for the photo (RTAS 2010 in Stockholm) and his help with iWeb!

Theoretical Computer Science 911.024/025, Summer semester 2020

Schedule:           Thursdays 10am-1pm

                            starting 5.3.2020 in T03 see calendar


First meeting:       Thursday, March 5 at 10am in T03


Language:           English


Office hours:       upon appointment


Instructions:       Tuesdays 11am-1pm in T05


Due to the corona virus outbreak, some of our meetings will be online.

Literature: Reading material will be suggested in the schedule below / via PlusOnline -- each week after class, related to the covered topic. We will use (parts of) the books:


[RS] Reactive Systems: Modelling, Specification, and Verification, Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen, and Jiri Srba


[MC] Model Checking by E.M. Clarke, O. Grumberg, and D.A.Peled


[HR] Logic in Computer Science: Modelling and Reasoning about Systems, by Michael Huth and Mark Ryan


[LTBTS] The Linear-Time Branching-Time Spectrum, by Rob van Glabbeek

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.121.9596&rep=rep1&type=pdf


[Stirling95] Stirling, C. (1995). Local model checking games, in Proc. CONCUR 95. LNCS 962 pp. 1–11.

[Thomas93] Thomas, W. (1993). On the Ehrenfeucht–Fraısse ́ game in theoretical computer science, in Proc. TAPSOFT 93. LNCS 668 pp. 559–568.

[KS90] P.C. Kanellakis, S.A. Smolka, CCS expressions, finite-state processes, and three problems of equivalence, Information & Computation 86 (1), p. 43-68, 1990

[AIS11] Aceto, L., Ingolfsdottir, A, & Srba, J. The algorithmics of bisimilarity. In D. Sangiorgi & J. Rutten (Eds.), Advanced Topics in Bisimulation and Coinduction (Cabridge Tracts in Theoretical Computer Science, pp 100-172), CUP, 2011.


[FOL-Wiki] The Wikipedia article on FOL: https://en.wikipedia.org/wiki/First-order_logic


[FOL-Chapter] An introductory Chapter on FOL by James Worrell


[FOL-Undec] Undecidability of First-Order Logic, by Guram Bezhanishvilli and Lawrence S. Moss (beautiful text based on original sources)


[R00] Universal Coalgebra: A Theory of Systems, by Jan Rutten, TCS 249 (2000) p.3-80

Prerequisites:  Knowledge of the material covered by basic theory courses that are part of bachelor studies in computer science.

Exam:   The exam for the lecture part (911.024) is written. It consist of several exercises / questions from the material covered during the course. There will be three exam possibilities (in July, August, and September).


In order to pass via one of the exam possibilities one needs to have 55% of the maximal points available at the exam. That is, if the exam brings maximally 100 points, in order to pass one needs to have at least 55 points.


The grade for the instructions (PS) part (911.025) will depend on the presentation / mini project. See information below.


Exam dates: t.b.a.

Course description:  This is an obligatory master course on selected topics in theoretical computer science: logic in computer science, verification methods, semantics. In this course we will learn the basics of formal methods, by focusing on selected topics. In particular we will learn formal models of (software) systems, several basic verification techniques, different logics for reasoning about programs and systems, semantic equivalences for fighting state-space explosion, decision procedures and the foundations of proof assistants and automated theory provers.

Slides:  Whenever slides are used, they will be made available on this webpage / via PlusOnline. The slides are by no means complete and only serve as help for better presentation. More material is covered during the class (on the blackboard) than visible on the slides.

Schedule (lectures and instructions):


Due to traveling, we will not meet every Thursday, but in the weeks when we meet we will do 180 min of lectures. That means starting at 10:00am and ending at 1:15pm with a 15min break in the middle. We plan to have 10 such meetings.


For the instruction sessions, it also suffices to have 21 hours, i.e., 10 sessions of 2 hours (120 min) and one extra hour, or some variant thereof.



Due to the corona virus outbreak, some of our meetings will be online.


  1. •March 5 (180min): Introduction an basic models used in formal methods. We discussed what theoretical computer science and formal methods covers, different areas and directions, and made a rough plan of topics that we would like to cover in the course of this course :-). Then we also learned the basic models: labelled transition systems, Kripke structures, and discussed some examples. Good reading material for this part is Chapter 2 of [MC] as well as Section 2.2.1 from [RS].

  2. •March 10 Instructions (105min): Modelling reactive systems and programs and learned (briefly) the syntax and semantics of CCS. This serves two purposes: To see that expressions / terms of a certain language can be used to represent models, and to get acquainted with CCS which is used to specify most examples and tasks in [RS]. This meeting was rather like a lecture, as we still do not have enough material to do exercises. I was explaining some examples. Please read the rest of Chapter 2 from [RS], especially if you would like to have a gentle informal introduction to CCS (Section 2.1).

On March 12 and March 17 there will be no classes. We will use this break to try out an online setup, so that the class on March 19 can take place this way. Our next topic is behavioral equivalences. I will contact you via email in order to try out different online options.


  1. •March 17 Instructions (75min): We spent this meeting checking up the setup and various possibilities for online teaching. Google Meet in combination with Slack works well, also students can share screen and present solutions -- this is good. Most students voted for a combination of slides / notes for presenting. I am using my new iPad, and despite of the fact that I need a lot still to learn, it works well. In this class we still discussed semantics of CCS a bit more with another example or two.


  1. •March 19 (180min): Semantics - behavioural equivalences. Introduction to behavioural equivalences & semantics, trace semantics, bisimulation & bisimilarity, simulation & similarity. This class was based on video clips that I recorded offline (using Good Notes 5), and shared with the students in the slack channel and via google drive. In the class we watched these video clips, and discussed questions / problems / ideas related to them. We also did a proof of one more property online, by sharing my screen in Good Notes 5. I will also provide you the notes created in this videos as pdf files (via Google Drive or slack / plusonline). We also briefly looked at the learning tool of Arno Wilhelm-Weidner (TU Berlin) that covers this topics in a learning unit. Please read Sections 3.1, 3.2, 3.3 from Chapter 3 from [RS]. We did not prove most of the properties /
    theorems comparing the various semantics, we will do this next time. For now, focus only on the definitions and examples. Please also learn through the behavioural equivalences learning unit from Arno’s learning tool. We also mentioned the paper [LTBTS] “lineaar-time branching-time spectrum” see above --- if you are interested please read (parts of) this paper.

  2. •March 24 Instructions (120min): The plan here is to go through the tasks from the learning unit from Arno’s tool related to behavioural equivalences. We will meet again via Google Meet. This plan worked very well, using Google Meet it was possible for all students to share their screen and discuss the solutions of the tasks. Having the online tool and the many simple tasks was also a very good and pleasant basis for the class. Many thanks, Arno! Thanks also to all of you, students in this course, for working nicely on the tasks and providing great explanations!


  1. •March 26 (195min): Semantics - behavioural equivalences, results and properties. We proceed with the video clips that I record offline, share with you in the slack channel and via google drive.  In the class we watched these video clips, and brifly discussed questions / problems / ideas related to them. We proved a theorem providing deeper understanding of bisimilarity, another theorem comparing bisimilarity with trace euivalence (and completed trace equivalence), we discussed a compositionality theorem for CCS terms, and finally also learned the bisimulation game. The discussion was brief because this time we suffered from network problems in the first part of the class. I shared with you (in the Google Drive) the notes from the class as pdf files). You can also read about the material of today in Sections 3.3 and 3.5, Chapter 3 in [RS]. It would be nice to read all of Chapter 3. You may also wish to look at the original papers about the bisimulation game [Stirling95] above and [Thomas93]


  1. •March 31 Instructions (130min): According to the plan we discuss several more theoretical tasks that I chose for you and shared (end of pdf notebook “TCS2020-Instructions.pdf” in the google drive). We also spent some more time discussing the bisimulation game. Again the google-meet setup with screen sharing worked very well.


  1. •April 2 (135min): Fixpoints - background, definitions and properties. We proceed with three more video clips, that were this time perfectly timely prepared, shared in the google drive and in the slack channel: 1-Fixpoints: Introduction to fixpoints -- order structures, posets, complete lattices, monotone functions, and fixpoints. 2-Tarski: Tarksi’s fixpoint theorem for complete lattices stated, proven, and discussed. 3-Kleene: Kleene’s iterative fixpoint theorem for finite complete lattices stated, proven, and discussed. We discussed examples along the way and answered some questions. You may read Chapter 4 from [RS] -- until Section 4.3 or any other source discussing fixpoints and their use in computer science. This class was intentionally a little bit shorter, as the two previous ones were longer than planned.


Easter break


  1. •April 21 Instructions (120min): We went through the tasks from the learning unit on Fixpoints from Arno’s tool. The link is on PlusOnline and in the slack channel. We met again via Google Meet. We solved all the tasks and everything worked perfectly well again.

  2. •April 23 (180min) Fixpoints in Computer Science. We proceed with the theory behind several examples of fixpoints in computer science: Bisimilarity as a fixpoint, and transitive closure as a fixpoint. We looked at additional examples how to compute bisimilarity with the fixpoint algorithm, and discussed the algorithm itself. You may finish reading Chapter 4 from [RS]. All videos and notes are in the google drive folder. I also shared with you couple of papers on algorithms for bisimilarity (see above [KS90], [AIS11]) via the slack channel.

  3. •April 28 Instructions (120min): We solved and discussed the theoretical exercises, that were already stated in the notes in the google drive folder and I shared with you in the slack channel. We also discussed anything that popped up as a question on the topic of computing bisimilarity as a fixedpoint and other examples of fixedpoints in computer science.


  1. •April 30 (180min) First-Order Logic (FOL) and its undecidability (the Entscheidungsproblem). Most of you are familiar with instantiated first-order logic formulas from preliminary courses in your bachelor studies. However, no course really teaches you formal FOL, which is why I dedicated these three hours to a brief introduction and overview of most important results in FOL. This class was online, without videos, but we do have the lecture notes as material and I also selected quite some reading material for you. This are already in the google drive folder, and listed above. Please read [FOL-Wiki], [FOL-Intro-Chapter], [FOL-Undec] -- you may also read on FOL in any other source, in any textbook on Logic, in particular in [HR].


  1. •May 5 Instructions (120min): Presentation of the first two larger homeworks, namely: (1) Kanellakis&Smolka’s algorithm for computing bisimilarity, by Tim Ungerhofer; (2) Paige&Tarjan’s partition refinement algorithm, by Sara Seidl.

  2. •May 7 (180min) Hennessy-Milner Logic (HML). Syntax and semantics, examples and properties, Hennessy-Milner Theorem (expressivity of HML). Please read Chapter 5 in [RS]


  1. •May 12 Instructions (50min) Presentation on automata minimization as a fixpoint, by Katharina Reiter. From now on the whole time we have in the PS will be spent on student presentations, we may still meet in the other weeks to discuss small tasks but that is on voluntary bases.

  2. •May 14 (180min) Temporal Logics. Syntax and semantics, examples and properties of CTL*, LTL, and CTL. Please read Chapter 4 in [MC].


  1. •May 19 Extra Instructions class (120min - voluntarily) With the few students who were present, we discussed the small homework tasks that I suggested for you from the [RS] book, related to HML.


  1. •No class on May 21 (holiday).


  1. •May 26 Instructions (100min): Presentations on (1) CTL via fixpoints by Selina Milla, and (2) Resolution by Hichem Belhocine.


  1. •May 28 (180min) Hoare Logic. Syntax, semantics, proof system. Proving (non) termination. We discussed many examples and verified couple of larger examples. Please read Chapter 4 in [HR]. My slides and videos for the lectures are in the google drive. I also sent you another interesting set of slides in the slack channel.

  2. •No instructions class on June 2 (holiday).


  1. •June 4 (180min) Coalgebra. The very basics of category theory and coalgebra theory, examples and behavioural equivalences. This was an *online* class, in the sense that there were no prerecorded videos except for a tiny introductory video. The produced notes and the paper [R00] (see above) are in the google drive folder. This is the end of the lectures part of a nice (mainly online) course (in my opinion). Thanks everyone for being part of it!













Ana Sokolova

Dr. TU Eindhoven, The Netherlands, 2005



Associate Professor


Computational Systems Group

Department of Computer Sciences

University of Salzburg

Austria


anas@cs.uni-salzburg.at

Instructions and homework:  Each week in the lectures you will be given small homework assignment, to help you check if you understood the topic that we dealt with in class. These excersises can / will be discussed in the instructions sessions, or in the office hours. We will also select papers to read / tools to experiment with, and use them as assignments for the instruction hours. Some of the instruction hours will be blocked towards the end of the semester, and each student will give a one hour presentation on a selected paper/chapter or tool.