Asymptotic behaviour in temporal logic

Eugene Asarin, Michel Blockelet, Aldric Degorre, Catalin Dima, Chunyan Mu

Research output: Chapter in Book/Report/Conference proceedingPublished conference contribution

3 Citations (Scopus)
5 Downloads (Pure)

Abstract

We study the “approximability” of unbounded temporal operators with time-bounded operators, as soon as some time bounds tend to∞. More specifically, for formulas in the fragments PLTL♦ and PLTL of the Parametric Linear Temporal Logic of Alur et al., we provide algorithms for computing the limit entropy as all parameters tend to∞. As a consequence, we can decide the problem whether the limit entropy of a formula in one of the two fragments coincides with that of its time-unbounded transformation, obtained by replacing each occurrence of a time-bounded operator into its time-unbounded version. The algorithms proceed by translation of the two fragments of PLTL into two classes of discrete-time timed automata and analysis of their strongly-connected components.
Original languageEnglish
Title of host publicationThe Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
EditorsThomas A. Henzinger, Dale Miller
PublisherACM
Pages1-9
Number of pages9
DOIs
Publication statusPublished - 14 Jul 2014

Fingerprint

Dive into the research topics of 'Asymptotic behaviour in temporal logic'. Together they form a unique fingerprint.

Cite this