Asymptotic behaviour in temporal logic

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

doi:10.1145/2603088.2603158

Asymptotic behaviour in temporal logic

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

Computing Science

Research output: Chapter in Book/Report/Conference proceeding › Published conference contribution

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 language	English
Title of host publication	The Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Editors	Thomas A. Henzinger, Dale Miller
Publisher	ACM
Pages	1-9
Number of pages	9
DOIs	https://doi.org/10.1145/2603088.2603158
Publication status	Published - 14 Jul 2014

Access to Document

10.1145/2603088.2603158

lics14

Cite this

@inproceedings{67c9e87b66964e578dfacf66ddfccde7,

title = "Asymptotic behaviour in temporal logic",

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.",

author = "Eugene Asarin and Michel Blockelet and Aldric Degorre and Catalin Dima and Chunyan Mu",

year = "2014",

month = jul,

day = "14",

doi = "10.1145/2603088.2603158",

language = "English",

pages = "1--9",

editor = "Henzinger, {Thomas A.} and Dale Miller",

booktitle = "The Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)",

publisher = "ACM",

}

TY - GEN

T1 - Asymptotic behaviour in temporal logic

AU - Asarin, Eugene

AU - Blockelet, Michel

AU - Degorre, Aldric

AU - Dima, Catalin

AU - Mu, Chunyan

PY - 2014/7/14

Y1 - 2014/7/14

N2 - 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.

AB - 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.

U2 - 10.1145/2603088.2603158

DO - 10.1145/2603088.2603158

M3 - Published conference contribution

SP - 1

EP - 9

BT - The Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

A2 - Henzinger, Thomas A.

A2 - Miller, Dale

PB - ACM

ER -

Asymptotic behaviour in temporal logic

Abstract

Access to Document

Fingerprint

Cite this