|
|
 |
|
Mercredi 14 Janvier
| Heure: |
15:30 - 16:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Cost Linear Temporal Logic for Verification |
| Description: |
Maximilien Colange Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton.
The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton.
This method can be extended with various automata flavors to handle quantitative properties.
We focus on an extension of Linear Temporal Logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL).
This logics can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking.
We describe the new properties that this extension allows to handle, illustrated with examples.
We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses.
We also propose a CEGAR-like approach to answer compute the bounds of the values reached by the automata. |
|
|
