Synchronized CTL over One-Counter Automata

Shaull Almagor, Daniel Assa, Udi Boker

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 requir…