2026-07-22T11:39:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7770 2024-03-06T10:41:09Z ddc:004 open_access

Model-Checking Counting Temporal Logics on Flat Structures Decker, Normann Habermehl, Peter Leucker, Martin Sangnier, Arnaud Thoma, Daniel Counting Temporal Logic Model checking Flat Kripke Structure 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Normann Decker and Peter Habermehl and Martin Leucker and Arnaud Sangnier and Daniel Thoma 2017 Is Part Of LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2017.29 urn:nbn:de:0030-drops-77709 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.29 eng https://creativecommons.org/licenses/by/3.0/legalcode