Sumários
P01 - Exercises on Linear Temporal Logic
20 outubro 2020, 15:00 • Paulo Alexandre Carreira Mateus
Exercises on LTL and Spin
Project description
15 outubro 2020, 14:00 • Paulo Alexandre Carreira Mateus
Project description. Channels in promela. BGP problem.
Lecture 8 - Linear Time Logic
13 outubro 2020, 15:00 • Paulo Alexandre Carreira Mateus
Model checking algorithm for omega-regular languages. Linear Temporal Logic: syntax and semantics. Examples. Satisfaction of a formula by a transition system, state and path.
Lecture 7: Empty language problem
8 outubro 2020, 14:00 • Paulo Alexandre Carreira Mateus
Empty language problem for Buchi automata and its complexity. Regular omega-language safety and its reduction to the empty language problem. Liveness properties.
Lecture 5: Regular omega languages
6 outubro 2020, 15:00 • Paulo Alexandre Carreira Mateus
Regular omega languages. Buchi automata.