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

Institut für Softwaretechnik und Programmiersprachen

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.

Originalsprache	Englisch
Titel	28th International Conference on Concurrency Theory (CONCUR 2017)
Seitenumfang	17
Band	85
Herausgeber (Verlag)	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Erscheinungsdatum	01.08.2017
Seiten	29:1--29:17
ISBN (Print)	978-3-95977-048-4
DOIs	https://doi.org/10.4230/LIPIcs.CONCUR.2017.29
Publikationsstatus	Veröffentlicht - 01.08.2017
Veranstaltung	28th International Conference on Concurrency Theory - Berlin, Deutschland Dauer: 05.09.2017 → 08.09.2017 Konferenznummer: 130722

UN SDGs

Dieser Output leistet einen Beitrag zu folgendem(n) Ziel(en) für nachhaltige Entwicklung

Zugriff auf Dokument

10.4230/LIPIcs.CONCUR.2017.29

Andere Dateien und Links

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

Zitieren

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) (Band 85, S. 29:1--29:17). (Leibniz International Proceedings in Informatics, LIPIcs; Band 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). Bd. 85, Leibniz International Proceedings in Informatics, LIPIcs, Bd. 85, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, S. 29:1--29:17, 28th International Conference on Concurrency Theory , Berlin, Berlin, Deutschland, 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). Band 85 Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. S. 29:1--29:17 (Leibniz International Proceedings in Informatics, LIPIcs; Band 85).

Publikation: Kapitel in Büchern/Berichten/Konferenzbänden › Konferenzbeitrag › Begutachtung

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

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Zitieren