MVS - Lecture Notes Summary

Lecture Info

Introduzione al corso

Esempi

• Termometro

• Controllore di Accesso

Lecture Info

Definizione di Automa

Esempi

• Controllore di Accesso

• Printer Manager

Lecture Info

Problema della Verifica

Flattening

Lecture Info

Come Sincronizzazione

Prodotto Cartesiano tra Automi

Esempi di Sincronizzazione

• Sincronizzazione tramite messaggi

• Sincronizzazione tramite Variabili Condivise

  • Algoritmo di Peterson

Lecture Info

Summary so Far

• Syncronization

• Verification

The need for Temporal Logic

Computational Tree Logic

• Atomic propositions

• Boolean combinators

• Temporal combinators

  • Next (X)

  • Future (F)

  • Globally (G)

  • Until (U)

• Examples

Lecture Info

Extending CTL

• All (A)

• Exists (E)

On the Nature of Time

Exercises

Lecture Info

The Problem with CTL

Restricted CTL

• Example

• The Locality of Restricted CTL

Propositional Linear Temporal Logic (PLTL)

Summary so Far

Lecture Info

Reachability Analysis

Model Checking Algorithm

• Case 1: \(\phi = P\)

• Case 2: \(\phi = \neg \psi\)

• Case 3: \(\phi = \psi_1 \land \psi_2\)

• Case 4: \(\phi = EX \psi\)

• Case 5: \(\phi = EF \psi\)

• Case 6: \(\phi = E \psi_1 U \psi_2\)

• Case 7: \(\phi = A \psi_1 U \psi_2\)

Lecture Info

Extended Regex

Model Checking in PLTL

• Example

• Theory of infinite automata

The State Explosion Problem

Lecture Info

Symbolic Model Checking

Symbolic Computation of State Sets

• Necessary Properties

• Representation Example

Lecture Info

Binary Decision Diagrams (BDDs)

Lecture Info

Lecture Info