Abstract
We study the “approximability” of unbounded temporal operators
with timebounded 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 timeunbounded transformation, obtained
by replacing each occurrence of a timebounded operator into its
timeunbounded version. The algorithms proceed by translation of
the two fragments of PLTL into two classes of discretetime timed
automata and analysis of their stronglyconnected components.
Original language  English 

Title of host publication  Proceedings of the Joint Meeting of the TwentyThird EACSL Annual Conference on Computer Science Logic (CSL) and the TwentyNinth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 
Publisher  ACM 
Pages  19 
Number of pages  10 
ISBN (Electronic)  9781450328869 
DOIs  
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 
Fingerprint
Dive into the research topics of 'Asymptotic behaviour in temporal logic'. Together they form a unique fingerprint.Profiles

Chunyan Mu
 Centre for Digital Innovation
 Department of Computing & Games  Senior Lecturer in Computer Science
Person: Academic