Reachability in two-clock timed automata is PSPACE-complete

Recently, Haase, Ouaknine, and Worrell have shown that reachability in two-clock timed automata is log-space equivalent to reachability in bounded one-counter automata. We show that reachability in bounded one-counter automata is PSPACE-complete.

Saved in:
Bibliographic Details
Published in:Information and computation 2015-08, Vol.243, p.26-36
Main Authors: Fearnley, John, Jurdziński, Marcin
Format: Article
Language:English
Subjects:
Counter automata
PSPACE-complete
Timed automata
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Recently, Haase, Ouaknine, and Worrell have shown that reachability in two-clock timed automata is log-space equivalent to reachability in bounded one-counter automata. We show that reachability in bounded one-counter automata is PSPACE-complete.
ISSN:0890-5401
1090-2651
DOI:10.1016/j.ic.2014.12.004