research-article

Asymptotic behaviour in temporal logic

Authors:

Chunyan MuAuthors Info & Claims

CSL-LICS '14: 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)

Article No.: 10, Pages 1 - 9

https://doi.org/10.1145/2603088.2603158

Published: 14 July 2014 Publication History

Get Access

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.

References

[1]

R. Alur, T. Feder, and T. A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116--146, 1996.

Digital Library

Google Scholar

[2]

R. Alur, K. Etessami, S. La Torre, and D. Peled. Parametric temporal logic for "model measuring". ACM Trans. Comput. Log., 2(3):388--407, 2001.

Digital Library

Google Scholar

[3]

N. Chomsky and G. A. Miller. Finite state languages. Information and Control, 1(2):91--112, 1958. ISSN 0019-9958.

Crossref

Google Scholar

[4]

J. M. Couvreur. On-the-fly verification of linear temporal logic. In World Congress on Formal Methods, pages 253--271, 1999.

Digital Library

Google Scholar

[5]

T. A. Henzinger and J. Otop. From model checking to model measuring. In P. R. D'Argenio and H. C. Melgratti, editors, CONCUR, volume 8052 of Lecture Notes in Computer Science, pages 273--287. Springer, 2013. ISBN 978-3-642-40183-1.

Digital Library

Google Scholar

[6]

M. Kwiatkowska. Quantitative verification: models techniques and tools. In FSE, pages 449--458. ACM SIGSOFT, 2007.

Digital Library

Google Scholar

[7]

D. Lind and B. Marcus. An Introduction to Symbolic Dynamics and Coding. Cambridge University Press, 1995.

Digital Library

Google Scholar

[8]

L. Staiger. Entropy of finite-state omega-languages. Problems of Control and Information Theory, 14(5):383--392, 1985.

Google Scholar

[9]

W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), pages 133--192. 1990.

Digital Library

Google Scholar

Cited By

View all

Cavezza DAlrajeh DGyörgy A(2018)A Weakness Measure for GR(1) FormulaeFormal Methods10.1007/978-3-319-95582-7_7(110-128)Online publication date: 12-Jul-2018
https://doi.org/10.1007/978-3-319-95582-7_7
Finkbeiner BTorfah H(2017)The Density of Linear-Time PropertiesAutomated Technology for Verification and Analysis10.1007/978-3-319-68167-2_10(139-155)Online publication date: 27-Sep-2017
https://doi.org/10.1007/978-3-319-68167-2_10

Index Terms

Asymptotic behaviour in temporal logic
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
      1. Temporal reasoning
2. Theory of computation
  1. Computational complexity and cryptography
    1. Complexity classes
  2. Logic
    1. Modal and temporal logics

Recommendations

Visibly Linear Temporal Logic

We introduce Visibly Linear Temporal Logic (VLTL), a linear-time temporal logic that captures the full class of Visibly Pushdown Languages over infinite words. The novel logic avoids fix points and instead provides natural temporal operators with simple ...
On temporal logic versus datalog
Logic and complexity in computer science

We provide a direct and modular translation from the temporal logics CTL, ETL, FCTL (CTL extended with the ability to express fairness) and the Modal µ-calculus to Monadic inf-Datalog with built-in predicates. We call it inf-Datalog because the ...
A complete proof system for propositional projection temporal logic

The paper presents a proof system for Propositional Projection Temporal Logic (PPTL) with projection-plus. The syntax, semantics, and logical laws of PPTL are introduced together with an axiom system consisting of axioms and inference rules. To ...

Comments

Information & Contributors

Information

Published In

July 2014

764 pages

ISBN:9781450328869

DOI:10.1145/2603088

Program Chairs:
Thomas Henzinger
Institute of Science and Technology (IST), Austria
,
Dale Miller
INRIA and LIX/Ecole Polytechnique, Palaiseau

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 July 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CSL-LICS '14

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

CSL-LICS '14: JOINT MEETING OF the Twenty-Third EACSL Annual Conference on COMPUTER SCIENCE LOGIC

July 14 - 18, 2014

Vienna, Austria

Acceptance Rates

CSL-LICS '14 Paper Acceptance Rate 74 of 212 submissions, 35%;

Overall Acceptance Rate 215 of 622 submissions, 35%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
136
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Cavezza DAlrajeh DGyörgy A(2018)A Weakness Measure for GR(1) FormulaeFormal Methods10.1007/978-3-319-95582-7_7(110-128)Online publication date: 12-Jul-2018
https://doi.org/10.1007/978-3-319-95582-7_7
Finkbeiner BTorfah H(2017)The Density of Linear-Time PropertiesAutomated Technology for Verification and Analysis10.1007/978-3-319-68167-2_10(139-155)Online publication date: 27-Sep-2017
https://doi.org/10.1007/978-3-319-68167-2_10

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations

Visibly Linear Temporal Logic

On temporal logic versus datalog

A complete proof system for propositional projection temporal logic

Comments

Information

Published In

Sponsors

In-Cooperation

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations