2026-08-06T20:37:31Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19392 2024-03-06T11:03:55Z ddc:004 open_access

Synchronized CTL over One-Counter Automata Almagor, Shaull Assa, Daniel Boker, Udi CTL Synchronization One Counter Automata Model Checking We consider the model-checking problem of Synchronized Computation-Tree Logic (CTL+Sync) over One-Counter Automata (OCAs). CTL+Sync augments CTL with temporal operators that require several paths to satisfy properties in a synchronous manner, e.g., the property "all paths should eventually see p at the same time". The model-checking problem for CTL+Sync over finite-state Kripke structures was shown to be in 𝖯^{NP^NP}. OCAs are labelled transition systems equipped with a non-negative counter that can be zero-tested. Thus, they induce infinite-state systems whose computation trees are not regular. The model-checking problem for CTL over OCAs was shown to be PSPACE-complete. We show that the model-checking problem for CTL+Sync over OCAs is decidable. However, the upper bound we give is non-elementary. We therefore proceed to study the problem for a central fragment of CTL+Sync, extending CTL with operators that require all paths to satisfy properties in a synchronous manner, and show that it is in EXP^NEXP (and in particular in EXPSPACE), by exhibiting a certain "segmented periodicity" in the computation trees of OCAs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Shaull Almagor and Daniel Assa and Udi Boker 2023 Is Part Of LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2023.19 urn:nbn:de:0030-drops-193921 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.19 eng https://creativecommons.org/licenses/by/4.0/legalcode