Verification for Timed Automata extended with Unbounded Discrete Data Structures
We study decidability of verification problems for timed automata extended with unbounded discrete data structures. More detailed, we extend timed automata with a pushdown stack. In this way, we obtain a strong model that may for instance be used to model real-time programs with procedure calls. It...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2015-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1596/pdf |
| _version_ | 1797988593494392832 |
|---|---|
| author | Karin Quaas |
| author_facet | Karin Quaas |
| author_sort | Karin Quaas |
| collection | DOAJ |
| description | We study decidability of verification problems for timed automata extended
with unbounded discrete data structures. More detailed, we extend timed
automata with a pushdown stack. In this way, we obtain a strong model that may
for instance be used to model real-time programs with procedure calls. It is
long known that the reachability problem for this model is decidable. The goal
of this paper is to identify subclasses of timed pushdown automata for which
the language inclusion problem and related problems are decidable. |
| first_indexed | 2024-04-11T08:06:34Z |
| format | Article |
| id | doaj.art-0db1ea88824e4e73993000e2b78db94f |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-11T08:06:34Z |
| publishDate | 2015-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-0db1ea88824e4e73993000e2b78db94f2022-12-22T04:35:32ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742015-09-01Volume 11, Issue 310.2168/LMCS-11(3:20)20151596Verification for Timed Automata extended with Unbounded Discrete Data StructuresKarin QuaasWe study decidability of verification problems for timed automata extended with unbounded discrete data structures. More detailed, we extend timed automata with a pushdown stack. In this way, we obtain a strong model that may for instance be used to model real-time programs with procedure calls. It is long known that the reachability problem for this model is decidable. The goal of this paper is to identify subclasses of timed pushdown automata for which the language inclusion problem and related problems are decidable.https://lmcs.episciences.org/1596/pdfcomputer science - logic in computer science |
| spellingShingle | Karin Quaas Verification for Timed Automata extended with Unbounded Discrete Data Structures Logical Methods in Computer Science computer science - logic in computer science |
| title | Verification for Timed Automata extended with Unbounded Discrete Data Structures |
| title_full | Verification for Timed Automata extended with Unbounded Discrete Data Structures |
| title_fullStr | Verification for Timed Automata extended with Unbounded Discrete Data Structures |
| title_full_unstemmed | Verification for Timed Automata extended with Unbounded Discrete Data Structures |
| title_short | Verification for Timed Automata extended with Unbounded Discrete Data Structures |
| title_sort | verification for timed automata extended with unbounded discrete data structures |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/1596/pdf |
| work_keys_str_mv | AT karinquaas verificationfortimedautomataextendedwithunboundeddiscretedatastructures |