research-article

Weight monitoring with linear temporal logic: complexity and decidability

Authors:

Christel Baier,

Sascha Klüppelholz,

Sascha WunderlichAuthors 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.: 11, Pages 1 - 10

https://doi.org/10.1145/2603088.2603162

Published: 14 July 2014 Publication History

Abstract

Many important performance and reliability measures can be formalized as the accumulated values of weight functions. In this paper, we introduce an extension of linear time logic including past (LTL) with new operators that impose constraints on the accumulated weight along path fragments. The fragments are characterized by regular conditions formalized by deterministic finite automata (monitor DFA). This new logic covers properties expressible by several recently proposed formalisms. We study the model-checking problem for weighted transition systems, Markov chains and Markov decision processes with rational weights. While the general problem is undecidable, we provide algorithms and sharp complexity bounds for several sublogics that arise by restricting the monitoring DFA.

References

[1]

P. A. Abdulla, R. Mayr, A. Sangnier, and J. Sproston. Solving parity games on integer vectors. In 24th International Conference on Concurrency Theory (CONCUR), volume 8052 of Lecture Notes in Computer Science, pages 106--120. Springer, 2013.

Digital Library

[2]

S. Andova, H. Hermanns, and J.-P. Katoen. Discrete-time rewards model-checked. In First International Workshop on Formal Modeling and Analysis of Timed Systems Workshop (FORMATS), volume 2791 of Lecture Notes in Computer Science, pages 88--104. Springer, 2003.

[3]

C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.

Digital Library

[4]

C. Baier, L. Cloth, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Performability assessment by model checking of Markov reward models. Formal Methods in System Design, 36(1):1--36, 2010.

Digital Library

[5]

C. Baier, J. Klein, S. Klüppelholz, and S. Wunderlich. Weight monitoring with linear temporal logic: Complexity and decidability. Technical report, TU Dresden, 2014. See http://wwwtcs.inf.tu-dresden.de/ALGI/PUB/CSL-LICS14/.

Digital Library

[6]

J. Barnat, L. Brim, I. Cema, M. Ceska, and J. Tumova. ProbDiVinE: A parallel qualitative ltl model checker. 4th International Conference on Quantitative Evaluation of SysTems (QEST), pages 215--216, 2007.

Digital Library

[7]

R. Bloem, K. Chatterjee, T. Henzinger, and B. Jobstmann. Better quality in synthesis through quantitative objectives. In 21st International Conference on Computer Aided Verification (CAV), volume 5643 of Lecture Notes in Computer Science, pages 140--156. Springer, 2009.

Digital Library

[8]

U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman. Temporal specifications with accumulative values. In 26th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 43--52. IEEE Computer Society, 2011.

Digital Library

[9]

T. Brázdil, V. Brozek, K. Chatterjee, V. Forejt, and A. Kucera. Two views on multiple mean-payoff objectives in Markov decision processes. In 26th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 33--42. IEEE Computer Society, 2011. ISBN 978-0-7695-4412-0.

Digital Library

[10]

K. Chatterjee and L. Doyen. Energy and mean-payoff parity Markov decision processes. In 36th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 6907 of Lecture Notes in Computer Science, pages 206--218. Springer, 2011.

Digital Library

[11]

K. Chatterjee and L. Doyen. Energy parity games. Theoretical Computer Science, 458:49--60, 2012.

Digital Library

[12]

K. Chatterjee, R. Majumdar, and T. A. Henzinger. Markov decision processes with multiple objectives. In 23rd Annual Symposium on Theoretical Aspects of Computer Science (STACS), volume 3884 of Lecture Notes in Computer Science, pages 325--336. Springer, 2006. ISBN 978-3-540-32301-3.

Digital Library

[13]

K. Chatterjee, T. Henzinger, B. Jobstmann, and R. Singh. Measuring and synthesizing systems in probabilistic environments. In 22nd International Conference on Computer Aided Verification (CAV), volume 6174 of Lecture Notes in Computer Science, pages 380--395. Springer, 2010.

Digital Library

[14]

K. Chatterjee, L. Doyen, M. Randour, and J.-F. Raskin. Looking at mean-payoff and total-payoff through windows. In 11th International Symposium on Automated Technology for Verification and Analysis (ATVA), pages 118--132, 2013.

[15]

E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.

Digital Library

[16]

C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857--907, 1995.

Digital Library

[17]

L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, Department of Computer Science, 1997.

[18]

L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In 13th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 454--465. IEEE Computer Society, 1998.

Digital Library

[19]

K. Etessami, M. Kwiatkowska, M. Vardi, and M. Yannakakis. Multi-objective model checking of Markov decision processes. Logical Methods in Computer Science, 4(4), 2008.

[20]

V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker. Automated verification techniques for probabilistic systems. In 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM), volume 6659 of Lecture Notes in Computer Science, pages 53--113. Springer, 2011.

[21]

J.-P. Katoen, I. Zapreev, E. Hahn, H. Hermanns, and D. Jansen. The ins and outs of the probabilistic model checker MRMC. Performance Evaluation, 68(2):90--104, 2011.

Digital Library

[22]

M. Kwiatkowska, G. Norman, and D. Parker. Advances and challenges of probabilistic model checking. In 48th Annual Allerton Conference on Communication, Control and Computing, pages 1691--1698. IEEE Press, 2010.

[23]

F. Laroussinie and J. Sproston. Model checking durational probabilistic systems. In 8th International Conference on Foundations of Software Science and Computational Structures (FOSSACS), volume 3441 of Lecture Notes in Computer Science, pages 140--154. Springer, 2005.

Digital Library

[24]

M. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, 1994.

Digital Library

[25]

A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logic. Journal of the ACM, 32(3):733--749, 1985.

Digital Library

[26]

T. Tomita, S. Hiura, S. Hagihara, and N. Yonezaki. A temporal logic with mean-payoff constraints. In 14th International Conference on Formal Engineering Methods. Formal Methods and Software Engineering (ICFEM), volume 7635 of Lecture Notes in Computer Science, pages 249--265. Springer, 2012.

Digital Library

[27]

M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In 1st Symposium on Logic in Computer Science (LICS), pages 332--344. IEEE Computer Society Press, 1986.

[28]

C. von Essen and B. Jobstmann. Synthesizing systems with optimal average-case behavior for ratio objectives. In International Workshop on Interactions, Games and Protocols (iWIGP), volume 50 of EPTCS, pages 17--32, 2011.

Cited By

Lu JXu M(2022)Bisection Value Iteration2022 29th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC57359.2022.00023(109-118)Online publication date: Dec-2022
https://doi.org/10.1109/APSEC57359.2022.00023
Main JRandour MSproston J(2022)Timed Games with Bounded Window Parity ObjectivesFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_10(165-182)Online publication date: 29-Aug-2022
https://doi.org/10.1007/978-3-031-15839-1_10
Baier CHermanns HKatoen J(2019)The 10,000 Facets of MDP Model CheckingComputing and Software Science10.1007/978-3-319-91908-9_21(420-451)Online publication date: 2019
https://doi.org/10.1007/978-3-319-91908-9_21
Show More Cited By

Index Terms

Weight monitoring with linear temporal logic: complexity and decidability
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
      1. Temporal reasoning
2. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

The common fragment of CTL and LTL
FOCS '00: Proceedings of the 41st Annual Symposium on Foundations of Computer Science

It is well-known that CTL (computation tree logic) and LTL (linear time logic) have incomparable expressive power. In this paper, we give an inductive definition of those ACTL (Action-based CTL) formulas that can be expressed in LTL. In addition, we ...
Regular Linear-Time Temporal Logic
TIME '10: Proceedings of the 2010 17th International Symposium on Temporal Representation and Reasoning

This extended abstract presents the main ideas behind regular linear-time temporal logic (RLTL), a logic that generalizes linear-time temporal logic (LTL) with the ability to use regular expressions arbitrarily as sub-expressions. Unlike LTL, RLTL can ...
Experiments with deterministic ω-automata for formulas of linear temporal logic
Implementation and application of automata

This paper addresses the problem of generating deterministic ω-automata for formulas of linear temporal logic, which can be solved by applying well-known algorithms to construct a nondeterministic Büchi automaton for the given formula on which we then ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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)

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

Copyright © 2014 ACM.

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]

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

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

Funding Sources

European Social Fund
Deutsche Forschungsgemeinschaft
Graduiertenkolleg 1763 (QuantLA)
Seventh Framework Programme
cfAED (center for Advancing Electronics Dresden)

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%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
185
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lu JXu M(2022)Bisection Value Iteration2022 29th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC57359.2022.00023(109-118)Online publication date: Dec-2022
https://doi.org/10.1109/APSEC57359.2022.00023
Main JRandour MSproston J(2022)Timed Games with Bounded Window Parity ObjectivesFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_10(165-182)Online publication date: 29-Aug-2022
https://doi.org/10.1007/978-3-031-15839-1_10
Baier CHermanns HKatoen J(2019)The 10,000 Facets of MDP Model CheckingComputing and Software Science10.1007/978-3-319-91908-9_21(420-451)Online publication date: 2019
https://doi.org/10.1007/978-3-319-91908-9_21
Gburek DBaier C(2018)Bisimulations, logics, and trace distributions for stochastic systems with rewardsProceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)10.1145/3178126.3178139(31-40)Online publication date: 11-Apr-2018
https://dl.acm.org/doi/10.1145/3178126.3178139
Haase CKiefer SLohrey MAceto LIngólfsdóttir A(2017)Computing quantiles in Markov chains with multi-dimensional costsProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330025(1-12)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330025
Haase CKiefer SLohrey M(2017)Computing quantiles in Markov chains with multi-dimensional costs2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS.2017.8005090(1-12)Online publication date: Jun-2017
https://doi.org/10.1109/LICS.2017.8005090
Baier CKlein JKlüppelholz SWunderlich S(2017)Maximizing the Conditional Expected Reward for Reaching the GoalProceedings, Part II, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020610.1007/978-3-662-54580-5_16(269-285)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54580-5_16
Baier CKlein JLeuschner LParker DWunderlich S(2017)Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision ProcessesComputer Aided Verification10.1007/978-3-319-63387-9_8(160-180)Online publication date: 13-Jul-2017
https://doi.org/10.1007/978-3-319-63387-9_8
Bruyère VHautem QRandour M(2016)Window Parity Games: An Alternative Approach Toward Parity Games with Time BoundsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.226.10226(135-148)Online publication date: 13-Sep-2016
https://doi.org/10.4204/EPTCS.226.10
Chatterjee KDoyen LKoskinen EGrohe MShankar N(2016)Perfect-Information Stochastic Games with Generalized Mean-Payoff ObjectivesProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2934513(247-256)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2934513
Show More Cited By

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.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents