Search

• < Previous
• 1
• Next >

---

Verification for Timed Automata extended with Unbounded Discrete Data Structures

Karin Quaas.

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&nbsp;[&hellip;]

---

Path Checking for MTL and TPTL over Data Words

Shiguang Feng ; Markus Lohrey ; Karin Quaas.

Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are quantitative extensions of linear temporal logic, which are prominent and widely used in the verification of real-timed systems. It was recently shown that the path checking problem for MTL, when evaluated over finite&nbsp;[&hellip;]

---

The Complexity of Flat Freeze LTL

Benedikt Bollig ; Karin Quaas ; Arnaud Sangnier.

We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable&nbsp;[&hellip;]

---