Reachability in Succinct and Parametric One-Counter Automata
One-counter automata are a fundamental and widely-studied class of infinite-state systems. In this paper we consider one-counter automata with counter updates encoded in binary-which we refer to as the succinct encoding. It is easily seen that the reachability problem for this class of machines is i...
| Main Authors: | , , , |
|---|---|
| Format: | Book section |
| Published: |
2009
|
| _version_ | 1826261133674151936 |
|---|---|
| author | Haase, C Kreutzer, S Ouaknine, J Worrell, J |
| author_facet | Haase, C Kreutzer, S Ouaknine, J Worrell, J |
| author_sort | Haase, C |
| collection | OXFORD |
| description | One-counter automata are a fundamental and widely-studied class of infinite-state systems. In this paper we consider one-counter automata with counter updates encoded in binary-which we refer to as the succinct encoding. It is easily seen that the reachability problem for this class of machines is in PSpace and is NP-hard. One of the main results of this paper is to show that this problem is in fact in NP, and is thus NP-complete. We also consider parametric one-counter automata, in which counter updates be integer-valued parameters. The reachability problem asks whether there are values for the parameters such that a final state can be reached from an initial state. Our second main result shows decidability of the reachability problem for parametric one-counter automata by reduction to existential Presburger arithmetic with divisibility. © 2009 Springer Berlin Heidelberg. |
| first_indexed | 2024-03-06T19:16:48Z |
| format | Book section |
| id | oxford-uuid:18ad460c-18d3-482b-bb90-393904c57087 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T19:16:48Z |
| publishDate | 2009 |
| record_format | dspace |
| spelling | oxford-uuid:18ad460c-18d3-482b-bb90-393904c570872022-03-26T10:44:28ZReachability in Succinct and Parametric One-Counter AutomataBook sectionhttp://purl.org/coar/resource_type/c_3248uuid:18ad460c-18d3-482b-bb90-393904c57087Symplectic Elements at Oxford2009Haase, CKreutzer, SOuaknine, JWorrell, JOne-counter automata are a fundamental and widely-studied class of infinite-state systems. In this paper we consider one-counter automata with counter updates encoded in binary-which we refer to as the succinct encoding. It is easily seen that the reachability problem for this class of machines is in PSpace and is NP-hard. One of the main results of this paper is to show that this problem is in fact in NP, and is thus NP-complete. We also consider parametric one-counter automata, in which counter updates be integer-valued parameters. The reachability problem asks whether there are values for the parameters such that a final state can be reached from an initial state. Our second main result shows decidability of the reachability problem for parametric one-counter automata by reduction to existential Presburger arithmetic with divisibility. © 2009 Springer Berlin Heidelberg. |
| spellingShingle | Haase, C Kreutzer, S Ouaknine, J Worrell, J Reachability in Succinct and Parametric One-Counter Automata |
| title | Reachability in Succinct and Parametric One-Counter Automata |
| title_full | Reachability in Succinct and Parametric One-Counter Automata |
| title_fullStr | Reachability in Succinct and Parametric One-Counter Automata |
| title_full_unstemmed | Reachability in Succinct and Parametric One-Counter Automata |
| title_short | Reachability in Succinct and Parametric One-Counter Automata |
| title_sort | reachability in succinct and parametric one counter automata |
| work_keys_str_mv | AT haasec reachabilityinsuccinctandparametriconecounterautomata AT kreutzers reachabilityinsuccinctandparametriconecounterautomata AT ouakninej reachabilityinsuccinctandparametriconecounterautomata AT worrellj reachabilityinsuccinctandparametriconecounterautomata |