Model-checking Counting Temporal Logics on Flat Structures

TL;DR

This paper investigates the decidability of counting temporal logics on flat structures, showing that model-checking is generally undecidable but becomes feasible on flat Kripke structures using counter system techniques.

Contribution

It introduces decidability results for counting temporal logics on flat structures and develops decision procedures based on counter systems.

Findings

Model-checking counting temporal logics is undecidable on general structures.

Decidability is restored on flat Kripke structures with simple loops.

Counter systems are used to implement evaluation of counting operators.

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.