Quantitative Model Checking

EIT Digital

Acerca de este Curso

4,080 vistas recientes

The integration of ICT (information and communications technology) in different applications is rapidly increasing in e.g. Embedded and Cyber physical systems, Communication protocols and Transportation systems. Hence, their reliability and dependability increasingly depends on software. Defects can be fatal and extremely costly (with regards to mass-production of products and safety-critical systems).
First, a model of the real system has to be built. In the simplest case, the model reflects all possible states that the system can reach and all possible transitions between states in a (labelled) State Transition System. When adding probabilities and discrete time to the model, we are dealing with so-called Discrete-time Markov chains which in turn can be extended with continuous timing to Continuous-time Markov chains. Both formalisms have been used widely for modeling and performance and dependability evaluation of computer and communication systems in a wide variety of domains. These formalisms are well understood, mathematically attractive while at the same time flexible enough to model complex systems. 

Model checking focuses on the qualitative evaluation of the model. As formal verification method, model checking analyzes
the functionality of the system model. A property that needs to be analyzed has to be specified in a logic with consistent syntax and semantics. For every state of the model, it is then checked whether the property is valid or not.
The main focus of this course is on quantitative model checking for Markov chains, for which we will discuss efficient computational algorithms. The learning objectives of this course are as follows:

- Express dependability properties for different kinds of transition systems .
- Compute the evolution over time for Markov chains.
- Check whether single states satisfy a certain formula and compute the satisfaction set for properties.

Certificado para compartir

Obtén un certificado al finalizar

100 % en línea

Comienza de inmediato y aprende a tu propio ritmo.

Fechas límite flexibles

Restablece las fechas límite en función de tus horarios.

Nivel intermedio

Aprox. 11 horas para completar

Inglés (English)

Subtítulos: Inglés (English)

Certificado para compartir

Obtén un certificado al finalizar

100 % en línea

Comienza de inmediato y aprende a tu propio ritmo.

Fechas límite flexibles

Restablece las fechas límite en función de tus horarios.

Nivel intermedio

Aprox. 11 horas para completar

Inglés (English)

Subtítulos: Inglés (English)

Instructor

Anne Remke

Prof. dr.

Computer Science

9,492 alumnos

2 cursos

ofrecido por

EIT Digital

EIT Digital is a pan-European organization whose mission is to foster digital technology innovation and entrepreneurial talent for economic growth and quality of life. By linking education, research and business, EIT Digital empowers digital top talents for the future.

EIT Digital provides online and blended Innovation and Entrepreneurship education to raise quality, increase diversity and availability of the top-level content provided by 20 leading technical universities around Europe. The universities deliver a unique blend of the best of technical excellence and entrepreneurial skills and mindset to digital engineers and entrepreneurs at all stages of their careers. The academic partners support Coursera’s bold vision to enable anyone, anywhere, to transform their lives by accessing the world’s best learning experience. This means that EIT Digital gradually shares parts of its entrepreneurial and academic education programmes to demonstrate its excellence and make it accessible to a much wider audience. EIT Digital’s online education portfolio can be used as part of blended education settings, in both Master and Doctorate programmes, and for professionals as a way to update their knowledge. EIT Digital offers an online programme in 'Internet of Things through Embedded Systems'. Achieving all certificates of the online courses and the specialization provides an opportunity to enroll in the on campus program and get a double degree. Please visit https://www.eitdigital.eu/eit-digital-academy/

Programa - Qué aprenderás en este curso

Semana

Semana 1

3 horas para completar

Module 1: Computational Tree Logic

We introduce Labeled Transition Systems (LTS), the syntax and semantics of Computational Tree Logic (CTL) and discuss the model checking algorithms that are necessary to compute the satisfaction set for specific CTL formulas.

3 horas para completar

6 videos (Total 61 minutos), 3 lecturas, 4 cuestionarios

6 videos

Welcome!1m

Introduction13m

Semantics of CTL13m

Model Checking CTL9m

The Until Operator12m

The Always Operator9m

3 lecturas

Script 1 and 2.110m

Script 2.2 and 2.310m

Script 2.420m

4 ejercicios de práctica

Formulate for yourself6m

Test your understanding of CTL semantics14m

Check your understanding of CTL20m

Model checking eventually, always and until22m

Semana

Semana 2

2 horas para completar

Discrete Time Markov Chains

We enhance transition systems by discrete time and add probabilities to transitions to model probabilistic choices. We discuss important properties of DTMCs, such as the memoryless property and time-homogeneity. State classification can be used to determine the existence of the limiting and / or stationary distribution.

2 horas para completar

5 videos (Total 49 minutos), 2 lecturas, 5 cuestionarios

5 videos

Introduction to DTMCs7m

Evolution in Time13m

Transient probabilities9m

State classification5m

Steady-state probabilities12m

2 lecturas

Script 3.1 and 3.210m

Script 3.310m

5 ejercicios de práctica

Evolution of DTMCs6m

Compute transient probabilities10m

Classification of DTMC states True or False?14m

State classification16m

Steady-state computation12m

Semana

Semana 3

2 horas para completar

Probabilistic Computational Tree Logic

We discuss the syntax and semantics of Probabilistic Computational Tree logic and check out the model checking algorithms that are necessary to decide the validity of different kinds of PCTL formulas. We shortly discuss the complexity of PCTL model checking.

2 horas para completar

5 videos (Total 36 minutos), 3 lecturas, 6 cuestionarios

5 videos

Syntax of PCTL8m

Model checking and the Next operator7m

Time-bounded Until6m

Backwards computation4m

Unbounded Until8m

3 lecturas

Script: 4.1 and 4.210m

Script: 4.3.1 and 4.3.225m

Script 4.3.310m

6 ejercicios de práctica

PCTL Syntax8m

Checking PCTL next4m

Test your understanding of PCTL Until6m

Checking time-bounded until16m

Checking unbounded until10m

Test your understanding of PCTL6m

Semana

Semana 4

2 horas para completar

Continuous Time Markov Chains

We enhance Discrete-Time Markov Chains with real time and discuss how the resulting modelling formalism evolves over time. We compute the steady-state for different kinds of CMTCs and discuss how the transient probabilities can be efficiently computed using a method called uniformisation.

2 horas para completar

5 videos (Total 57 minutos), 2 lecturas, 6 cuestionarios

5 videos

Definition of a CTMC10m

Generator matrix11m

Steady-state probabilities11m

Triple Modular Redundancy11m

Uniformisation12m

2 lecturas

Script: 5.1 and 5.220m

Script: 5.315m

6 ejercicios de práctica

Generator matrix6m

Test your understanding of CTMCs6m

Steady state probability in CTMCs10m

Identifying BSCCs12m

Test your understanding of Uniformisation6m

Uniformisation12m

Preguntas Frecuentes

¿Cuándo podré acceder a las lecciones y tareas?
Access to lectures and assignments depends on your type of enrollment. If you take a course in audit mode, you will be able to see most course materials for free. To access graded assignments and to earn a Certificate, you will need to purchase the Certificate experience, during or after your audit. If you don't see the audit option:
The course may not offer an audit option. You can try a Free Trial instead, or apply for Financial Aid.
The course may offer 'Full Course, No Certificate' instead. This option lets you see all course materials, submit required assessments, and get a final grade. This also means that you will not be able to purchase a Certificate experience.
¿Qué recibiré si compro el Certificado?
Cuando compras un Certificado, obtienes acceso a todos los materiales del curso, incluidas las tareas calificadas. Una vez que completes el curso, se añadirá tu Certificado electrónico a la página Logros. Desde allí, puedes imprimir tu Certificado o añadirlo a tu perfil de LinkedIn. Si solo quieres leer y visualizar el contenido del curso, puedes participar del curso como oyente sin costo.
¿Cuál es la política de reembolsos?
Puedes solicitar un reembolso completo hasta dos semanas después de tu fecha de pago o (para los cursos que se lanzaron recientemente) hasta dos semanas después del comienzo de la primera sesión del curso, lo que ocurra después. No puedes recibir un reembolso luego de obtener un Certificado de curso, aun cuando completes el curso dentro del período de reembolso de dos semanas. Consulta nuestra política de reembolsos completa.
¿Hay ayuda económica disponible?
Sí, Coursera ofrece ayuda económica a los estudiantes que no pueden pagar la tarifa. Solicítala haciendo clic en el vínculo de Ayuda económica que está debajo del botón 'Inscribirse' a la izquierda. Se te pedirá que completes una solicitud y recibirás una notificación cuando se apruebe. Obtén más información.
¿Recibiré crédito universitario por completar el Curso?
Este Curso no otorga crédito universitario, pero algunas universidades pueden aceptar los Certificados del curso para obtener crédito. Consulta con tu institución para obtener más información. Los Títulos en línea y los Certificados Mastertrack™ de Coursera brindan la oportunidad de obtener créditos universitarios.

¿Tienes más preguntas? Visita el Centro de Ayuda al Alumno.

Quantitative Model Checking