|
Reasoning about transfinite sequences| old_uid | 575 |
|---|
| title | Reasoning about transfinite sequences |
|---|
| start_date | 2006/01/31 |
|---|
| schedule | 14h30 |
|---|
| online | no |
|---|
| summary | We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequences of actions and quantitative temporal operators indexed by ordinals replace the standard next-time and until future-time operators. Our aim is to control such systems by designing controllers that safely work on omega-sequences but interact synchronously with the system in order to restrict their behaviors. In this talk, we show why the satisfiability problem for the logics working on É÷k-sequences is EXPSPACE-complete when the integers are represented in binary, and PSPACE-complete with a unary representation. To do so, we substantially extend standard results about LTL by introducing a new class of succinct ordinal automata that can encode the interaction between the different quantitative temporal operators.
This is a joint work with David Nowak. |
|---|
| responsibles | Rispal, Clément |
|---|
| |
|