Reasoning about transfinite sequences
| dc.creator | Demri, Stéphane | |
| dc.creator | Nowak, David | |
| dc.date | 2005-05-26 | |
| dc.date | 2006-08-17 | |
| dc.date.accessioned | 2026-07-07T13:01:22Z | |
| dc.date.available | 2026-07-07T13:01:22Z | |
| dc.description | 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 $ω$-sequences but interact synchronously with the system in order to restrict their behaviors. We show that 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. | |
| dc.description | 38 pages | |
| dc.identifier | https://arxiv.org/abs/cs/0505073 | |
| dc.identifier | http://arxiv.org/abs/cs/0505073 | |
| dc.identifier | International Journal of Foundations of Computer Science, 18(1):87-112, February 2007 | |
| dc.identifier | doi:10.1142/S0129054107004589 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/226128 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | Computational Complexity | |
| dc.title | Reasoning about transfinite sequences | |
| dc.type | text |