Model Checking Succinct and Parametric One-Counter Automata.
We investigate the decidability and complexity of various model checking problems over one-counter automata. More specifically, we consider succinct one-counter automata, in which additive updates are encoded in binary, as well as parametric one-counter automata, in which additive updates may be giv...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Journal article |
| Language: | English |
| Published: |
Springer
2010
|
| _version_ | 1826258897829101568 |
|---|---|
| author | Göller, S Haase, C Ouaknine, J Worrell, J |
| author2 | Abramsky, S |
| author_facet | Abramsky, S Göller, S Haase, C Ouaknine, J Worrell, J |
| author_sort | Göller, S |
| collection | OXFORD |
| description | We investigate the decidability and complexity of various model checking problems over one-counter automata. More specifically, we consider succinct one-counter automata, in which additive updates are encoded in binary, as well as parametric one-counter automata, in which additive updates may be given as unspecified parameters. We fully determine the complexity of model checking these automata against CTL, LTL, and modal μ-calculus specifications. © 2010 Springer-Verlag Berlin Heidelberg. |
| first_indexed | 2024-03-06T18:41:18Z |
| format | Journal article |
| id | oxford-uuid:0cf27bce-e14f-47c5-9b02-d367c1a1893a |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T18:41:18Z |
| publishDate | 2010 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:0cf27bce-e14f-47c5-9b02-d367c1a1893a2022-03-26T09:37:53ZModel Checking Succinct and Parametric One-Counter Automata.Journal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:0cf27bce-e14f-47c5-9b02-d367c1a1893aEnglishSymplectic Elements at OxfordSpringer2010Göller, SHaase, COuaknine, JWorrell, JAbramsky, SGavoille, CKirchner, CHeide, FSpirakis, PWe investigate the decidability and complexity of various model checking problems over one-counter automata. More specifically, we consider succinct one-counter automata, in which additive updates are encoded in binary, as well as parametric one-counter automata, in which additive updates may be given as unspecified parameters. We fully determine the complexity of model checking these automata against CTL, LTL, and modal μ-calculus specifications. © 2010 Springer-Verlag Berlin Heidelberg. |
| spellingShingle | Göller, S Haase, C Ouaknine, J Worrell, J Model Checking Succinct and Parametric One-Counter Automata. |
| title | Model Checking Succinct and Parametric One-Counter Automata. |
| title_full | Model Checking Succinct and Parametric One-Counter Automata. |
| title_fullStr | Model Checking Succinct and Parametric One-Counter Automata. |
| title_full_unstemmed | Model Checking Succinct and Parametric One-Counter Automata. |
| title_short | Model Checking Succinct and Parametric One-Counter Automata. |
| title_sort | model checking succinct and parametric one counter automata |
| work_keys_str_mv | AT gollers modelcheckingsuccinctandparametriconecounterautomata AT haasec modelcheckingsuccinctandparametriconecounterautomata AT ouakninej modelcheckingsuccinctandparametriconecounterautomata AT worrellj modelcheckingsuccinctandparametriconecounterautomata |