Asymptotic behaviour in temporal logic
| Autor: | Eugene Asarin, Aldric Degorre, Michel Blockelet, Chunyan Mu, Catalin Dima |
|---|---|
| Přispěvatelé: | Laboratoire d'informatique Algorithmique : Fondements et Applications (LIAFA), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Algorithmique Complexité et Logique (LACL), Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: |
Discrete mathematics
020207 software engineering 0102 computer and information sciences 02 engineering and technology 16. Peace & justice 01 natural sciences Automaton Operator (computer programming) Linear temporal logic 010201 computation theory & mathematics Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering Temporal logic [INFO]Computer Science [cs] Entropy (arrow of time) ComputingMilieux_MISCELLANEOUS Parametric statistics Mathematics |
| Zdroj: | 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), CSL-LICS '14, Vienna, Austria, July 14-18, 2014 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), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, 2014, Unknown, Unknown Region. pp.10:1--10:9, ⟨10.1145/2603088.2603158⟩ CSL-LICS |
| DOI: | 10.1145/2603088.2603158⟩ |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|