Asymptotic behaviour in temporal logic

E Asarin; M Bockelet; A Degorre; C Dima; Chunyan Mu

doi:10.1145/2603088.2603158

Asymptotic behaviour in temporal logic

E Asarin, M Bockelet, A Degorre, C Dima, Chunyan Mu

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

191 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	Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Publisher	ACM
Pages	1-9
Number of pages	10
ISBN (Electronic)	978-1-4503-2886-9
DOIs	https://doi.org/10.1145/2603088.2603158
Publication status	Published - 2014
Event	Joint meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) - Vienna, Austria Duration: 14 Jul 2014 → 18 Jul 2014

Conference

Conference	Joint meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Country/Territory	Austria
City	Vienna
Period	14/07/14 → 18/07/14

Access to Document

10.1145/2603088.2603158

PublicationFinal published version, 374 KBLicence: Other

Cite this

@inproceedings{2a1eb626a54242079ce197715e22caf8,

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 = "E Asarin and M Bockelet and A Degorre and C Dima and Chunyan Mu",

year = "2014",

doi = "10.1145/2603088.2603158",

language = "English",

pages = "1--9",

booktitle = "Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)",

publisher = "ACM",

note = "Joint meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) ; Conference date: 14-07-2014 Through 18-07-2014",

}

Asarin, E, Bockelet, M, Degorre, A, Dima, C & Mu, C 2014, Asymptotic behaviour in temporal logic. in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . ACM, pp. 1-9, Joint meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vienna, Austria, 14/07/14. https://doi.org/10.1145/2603088.2603158

Asymptotic behaviour in temporal logic. / Asarin, E; Bockelet, M; Degorre, A et al.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . ACM, 2014. p. 1-9.

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

TY - GEN

T1 - Asymptotic behaviour in temporal logic

AU - Asarin, E

AU - Bockelet, M

AU - Degorre, A

AU - Dima, C

AU - Mu, Chunyan

PY - 2014

Y1 - 2014

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 - Conference contribution

SP - 1

EP - 9

BT - Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

PB - ACM

T2 - Joint meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Y2 - 14 July 2014 through 18 July 2014

ER -

Asymptotic behaviour in temporal logic

Abstract

Conference

Access to Document

Fingerprint

Cite this