CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report)
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911392095797248 |
|---|---|
| author | Pettinau, Roberto Matheja, Christoph |
| author_facet | Pettinau, Roberto Matheja, Christoph |
| contents | We study model checking algorithms for infinite families of finite-state labeled transition systems against temporal properties written in CTL*. Such families arise, for example, as models of highly configurable systems or software product lines.
We model families using context-free graph grammars. We then develop a state labeling algorithm that works compositionally on the grammar's production rules with limited information about the context in which the rule is applied. The result is a graph grammar modeling the same family but with extended labels. We leverage this grammar to decide whether all, some, or (in)finitely many members of a family satisfy a given temporal property. We have implemented our algorithms and present early experiments. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_15756 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report) Pettinau, Roberto Matheja, Christoph Logic in Computer Science We study model checking algorithms for infinite families of finite-state labeled transition systems against temporal properties written in CTL*. Such families arise, for example, as models of highly configurable systems or software product lines. We model families using context-free graph grammars. We then develop a state labeling algorithm that works compositionally on the grammar's production rules with limited information about the context in which the rule is applied. The result is a graph grammar modeling the same family but with extended labels. We leverage this grammar to decide whether all, some, or (in)finitely many members of a family satisfy a given temporal property. We have implemented our algorithms and present early experiments. |
| title | CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2601.15756 |