Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2017.29
URN: urn:nbn:de:0030-drops-77709
URL: https://drops.dagstuhl.de/opus/volltexte/2017/7770/
Decker, Normann ; Habermehl, Peter ; Leucker, Martin ; Sangnier, Arnaud ; Thoma, Daniel
Model-Checking Counting Temporal Logics on Flat Structures
| pdf-format: |
|
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 model-checking 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.
BibTeX - Entry
@InProceedings{decker_et_al:LIPIcs:2017:7770,
author = {Normann Decker and Peter Habermehl and Martin Leucker and Arnaud Sangnier and Daniel Thoma},
title = {{Model-Checking Counting Temporal Logics on Flat Structures}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {29:1--29:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Roland Meyer and Uwe Nestmann},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7770},
URN = {urn:nbn:de:0030-drops-77709},
doi = {10.4230/LIPIcs.CONCUR.2017.29},
annote = {Keywords: Counting Temporal Logic, Model checking, Flat Kripke Structure}
}
| Keywords: | Counting Temporal Logic, Model checking, Flat Kripke Structure | |
| Seminar: | 28th International Conference on Concurrency Theory (CONCUR 2017) | |
| Issue date: | 2017 | |
| Date of publication: | 01.09.2017 |
