Lecture was led by Marina. Marina introduces us to model checking giving us some introductory tools. First she introduced the general structure where model checking appears: in the relation between real system (system model) and the formalization of its properties (property specification). The process has three posible outputs: yes, no or missing information for computing. The main theoretical tools are: automata theory (Büchi automata), language theory (properties will be language of infinite words), mathematical logic, graph and data algorithms. Then we saw an example of a system: traffic lights and establish the difference between safety and liveliness properties. Then Marina established a schema of our project: We have the real driving situation registered by tachograph (we need to model these) and the law (that we have to formalize with LTL, CTL, MSO or others): our property will be the law and the real situation is the situation of the driver. Then Marina talked about transition systems, which is a standard representation in computation theory. A transition system is a directed graph giving some formal representation of a system. It has four elements/aspects: the states, the stepwise behavior, the initial states and additional information. Then Marina defined the transition system as a tuple (state space, set of actions, transition relation, set of initial states, the set of atomic prepositions and the labeling function).
The lecture started like a dialogue between Joost, Moritz and Marina about the definition of the problem we want to solve during the project: the problem about the tachograph and what is the better model to solve the problem. Then Joost distinguished between the tachograph, which implies a lot of modeling problems, and the activity list, which can be seen as objective activities (driving, resting, etc.). It served as an introduction session about what the project is going to be.
The lecture was led by Marina. Marina talked about how to study and formalize the behavior of transition systems and linear time properties and how to formalize them. First, Marina repeated an introduction to the model checking characteristics. Marina talked about how to formalize a transition system. For obtaining knowledge about the behavior of a transition system, first we need to know a terminal state. Any transition system starts in an initial state and passes from this state to another until it arrives at a terminal state: it can have a final behavior or execute infinitely. In any case, this behavior is formalized with executions. An execution fragment is a sequence of states and actions. An execution fragment can be initial (it starts in an initial state) or maximal (that it can't be prolonged). Then we need to abstract from actions with a path fragment representing a possible behavior of a transition system. Then Marina explained how to pas from transition system with terminal state to transition system without terminal state. Then Marina explained the concept of linear-time properties that are requirements over the traces of a transition system. A lineal time property is a language of infinity words. Finally, we saw that three types of LT-properties.
We didn't have a lecture this week because it was holiday in Barcelona.
Lecture was led by Moritz. We started repeating what model checking is and then how to use transition systems and then explain how to use model checking as a model of transition systems. Moritz explained that the objective of a transition system is to satisfy the formal property of the requirement. Then he introduces a program graph. First, Moritz use an example of transition system drawing a schema of a model of three states. For lead from state to state he draw arrows. Then he explained what the execution is. An execution in transition system is a sequence of states and action names. The first state is the initial state and then we need a maximal that can be infinite or end in a deadlock (state without leaving arrows). Then he explained how to use a transition system as a model in a real program. Then he put an example of a transition system for explaining it in a concrete way. Then he explain the concept of Program Graph (PG) first using an example and then defining it. PG need a set of type variables: var is a set and it have a domain of the variables. There is the evaluation which is a function defined on the set of variables and the final thing is the condition that is a set of evaluations. Then, Moritz defined the program graphs being over var and dom, with loc set of locations, a set of actions (transition systems), initial states or locations (which is a subset of loc), g0 (which is the initial condition) and the arrows. Finally, he explained the transition system associated with the PG.
In this lecture, Moritz introduced Finite Automata. We saw the non-deterministic (NFA) and deterministic (DFA) and we saw the difference between them. At this point, we also remembered the notion of execution applied to automata, and we introduced the notion of acceptance, the regular languages, and what it means to be equivalent automata. We also saw an exemplification of NFA and DFA which were equivalent. After that, we saw the proof that every NFA is equivalent to a DFA . After that, keeping in mind that we want a model checker and it checks whether the structure satisfies the sentences, we saw the words as structures. The sentences we are interested in are from MSO logic. Lastly, the Büchi’s theorem was presented, whose proof we’ll see next week.
Lecture was led by Moritz. The session is dedicated to prove the Büchi's Theorem, that say that exactly the regular languages are MSO-definable. For proving this we have to show that each MSO-sentence has an equivalent non-deterministic finite automaton and that every non-deterministic finite automaton has an equivalent MSO-sentence. First we saw the first direction: that every NFA has an equivalent MSO-sentence and then we saw that every MSO-sentence has an equivalent NFA.
In this lecture, Moritz taught us the corollaries of Büchi's theorem seen in the session before. First, we saw that MSO collapse over words, namely that there is a computable function that maps a given MSO sentence to another MSO sentence composed of an existential quantifier, a tuple of set variables, and followed by a first-order sentence. The next corollary is that the model checking of MSO over words, which is to decide if the structure of the input satisfies phi (the MSO sentence), and is decidable in the time of the length of the word and the function of the length of phi. Finally, the third corollary is the MSO inexpressibility over words where we saw the Pumping Lemma and why it rises the problem that some properties can't be MSO-definable.
Lecture was lead by Moritz. This session was dedicated to questions and exercises.
Lecture was led by Moritz. He talked about finite automaton: non-deterministic finite automaton and deterministic finite automaton and we saw some propositions of them. We saw the lower bounds of them. Then Moritz showed how to extend the methodology to richer structures with infinite words. For doing this first we saw the ω-regular languages. Then we saw when the determination fails. Then we saw the McNaughton theorem that says that ω-regular languages is effectively closed under complementation. Then we applied what we see at the case of Büchi. Finally we saw corollaries about what we have seen. This session was dedicated to prove the ω version of Büchis theorem this says that ω words non deterministic Büchi automata and monadic second order sentences are the same, that there is an effective translation between both.
Lecture was led by Moritz and Eduardo: Moritz did the theoretical part and Eduardo introduced us to the UPPAAL program. Moritz part was dedicated to close the circle of the seminar and show how to use the machinery we developed, the monadic second order logic, Büchi automata and ω regularity to see how this can be used in order to do model checking to check specifications of desiderata of given transition systems. How to check the correctness of a specified formula or sense in a transition system. Then Eduardo introduced us to the basis of UPPAAL with an example of a model with this program.
Lecture was led by Moritz and Eduardo. This session is dedicated to close the session that we started last week. We saw the model-checking MSO-definable linear time properties, the linear temporal logic and the LTL Model Checking. We saw the LTL model checker and the automata theoretical methods. With Eduardo we corrected the exercises he had proposed in the last session.
Lecture was led by Moritz. It was dedicated to do something similar we did last session but with timed automata. We saw timed automata, how to execute a timed automata and how time computation tree logic worked.
Lecture was led by Moritz. We continued the timed automata commentary. We saw timed automata, transition systems, how to executed a timed automata, timed computation tree logic and we trait all of these for explain the model-checking TCTL (timed computation tree logic). We saw the theorem of model-checking TCTL and the proof.
Webpage maintained by Eric Sancho, Eduard Gisbert and Miguel Jalón.