Model-Checking Counting Temporal Logics on Flat Structures

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


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 languageEnglish
Title of host publication28th International Conference on Concurrency Theory (CONCUR 2017)
Number of pages17
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Publication date01.08.2017
ISBN (Print)978-3-95977-048-4
Publication statusPublished - 01.08.2017
Event28th International Conference on Concurrency Theory - Berlin, Germany
Duration: 05.09.201708.09.2017
Conference number: 130722


Dive into the research topics of 'Model-Checking Counting Temporal Logics on Flat Structures'. Together they form a unique fingerprint.

Cite this