|
|
 |
|
Jeudi 19 Janvier
| Heure: |
15:30 - 16:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Whats decidable about parametric timed automata? |
| Description: |
Étienne André Parametric timed automata (PTA) are a powerful formalism to reason,
simulate and formally verify critical real-time systems.
After two decades of research on PTA, it is now well-understood that
any non-trivial problem studied is undecidable for general PTA.
We provide here a survey of decision and computation problems for PTA.
On the one hand, bounding time, bounding the number of parameters or
the domain of the parameters does not (in general) lead to any decidability.
On the other hand, restricting the number of clocks, the use of
clocks (compared or not with the parameters), and the use of parameters
(e.g. used only as upper or lower bounds) leads to decidability of some
problems. |
|
|
