Model-Checking Counting Temporal Logics on Flat Structures

Normann Decker; Peter Habermehl; Martin Leucker; Arnaud Sangnier; Daniel Thoma

doi:10.4230/LIPIcs.CONCUR.2017.29

Model-Checking Counting Temporal Logics on Flat Structures

Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, Daniel Thoma

Institute of Software Engineering and Programming Languages

Abstract

We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the modelchecking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.

Original language	English
Title of host publication	28th International Conference on Concurrency Theory (CONCUR 2017)
Number of pages	17
Volume	85
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Publication date	01.08.2017
Pages	29:1--29:17
ISBN (Print)	978-3-95977-048-4
DOIs	https://doi.org/10.4230/LIPIcs.CONCUR.2017.29
Publication status	Published - 01.08.2017
Event	28th International Conference on Concurrency Theory - Berlin, Germany Duration: 05.09.2017 → 08.09.2017 Conference number: 130722

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.4230/LIPIcs.CONCUR.2017.29

Cite this

Decker, N., Habermehl, P., Leucker, M., Sangnier, A., & Thoma, D. (2017). Model-Checking Counting Temporal Logics on Flat Structures. In 28th International Conference on Concurrency Theory (CONCUR 2017) (Vol. 85, pp. 29:1--29:17). (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 85). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.29

@inproceedings{27d3edc065754504969ea46c0a7ef4eb,

title = "Model-Checking Counting Temporal Logics on Flat Structures",

abstract = "We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the modelchecking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.",

author = "Normann Decker and Peter Habermehl and Martin Leucker and Arnaud Sangnier and Daniel Thoma",

year = "2017",

month = aug,

day = "1",

doi = "10.4230/LIPIcs.CONCUR.2017.29",

language = "English",

isbn = "978-3-95977-048-4",

volume = "85",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

pages = "29:1----29:17",

booktitle = "28th International Conference on Concurrency Theory (CONCUR 2017)",

note = "28th International Conference on Concurrency Theory , CONCUR 2017 ; Conference date: 05-09-2017 Through 08-09-2017",

}

Decker, N, Habermehl, P, Leucker, M, Sangnier, A & Thoma, D 2017, Model-Checking Counting Temporal Logics on Flat Structures. in 28th International Conference on Concurrency Theory (CONCUR 2017). vol. 85, Leibniz International Proceedings in Informatics, LIPIcs, vol. 85, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 29:1--29:17, 28th International Conference on Concurrency Theory , Berlin, Berlin, Germany, 05.09.17. https://doi.org/10.4230/LIPIcs.CONCUR.2017.29

Model-Checking Counting Temporal Logics on Flat Structures. / Decker, Normann; Habermehl, Peter; Leucker, Martin et al.
28th International Conference on Concurrency Theory (CONCUR 2017). Vol. 85 Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. p. 29:1--29:17 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 85).

Research output: Chapters in Books/Reports/Conference Proceedings › Conference contribution › peer-review

TY - GEN

T1 - Model-Checking Counting Temporal Logics on Flat Structures

AU - Decker, Normann

AU - Habermehl, Peter

AU - Leucker, Martin

AU - Sangnier, Arnaud

AU - Thoma, Daniel

N1 - Conference code: 130722

PY - 2017/8/1

Y1 - 2017/8/1

N2 - We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the modelchecking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.

AB - We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the modelchecking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.

UR - https://www.scopus.com/record/display.uri?eid=2-s2.0-85030640021&origin=inward&txGid=355787a147f3cc17da0138ca9e4e79fd

U2 - 10.4230/LIPIcs.CONCUR.2017.29

DO - 10.4230/LIPIcs.CONCUR.2017.29

M3 - Conference contribution

SN - 978-3-95977-048-4

VL - 85

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 29:1--29:17

BT - 28th International Conference on Concurrency Theory (CONCUR 2017)

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

T2 - 28th International Conference on Concurrency Theory

Y2 - 5 September 2017 through 8 September 2017

ER -

Model-Checking Counting Temporal Logics on Flat Structures

Abstract

UN SDGs

Access to Document

Other files and links

Fingerprint

Cite this