Computer Science – Logic in Computer Science
Scientific paper
2005-05-26
International Journal of Foundations of Computer Science, 18(1):87-112, February 2007
Computer Science
Logic in Computer Science
38 pages
Scientific paper
10.1142/S0129054107004589
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. We show that the satisfiability problem for the logics working on $\omega^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.
Demri Stéphane
Nowak David
No associations
LandOfFree
Reasoning about transfinite sequences does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Reasoning about transfinite sequences, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Reasoning about transfinite sequences will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-117377