zbMATH — the first resource for mathematics

Decision problems for the verification of real-time software. (English) Zbl 1178.68340
Hespanha, João (ed.) et al., Hybrid systems: Computation and control. 9th international workshop, HSCC 2006, Santa Barbara, CA, USA, March 29–31, 2006. Proceedings. Berlin: Springer (ISBN 3-540-33170-0/pbk). Lecture Notes in Computer Science 3927, 200-211 (2006).
Summary: We study two questions in the theory of timed automata concerning timed language inclusion of real-time programs modeled as timed pushdown automata in real-time specifications with just one clock. We show that if the specification \(B\) is modeled as a timed automaton with one clock, then the language inclusion problem \(L(A) \subseteq L(B)\) for a timed pushdown automaton \(A\) is decidable. On the other hand, we show that the universality problem of timed visibly pushdown automata with only one clock is undecidable. Thus there is no algorithm to check language inclusion of real-time programs for specifications given by visibly pushdown specifications with just one clock.
For the entire collection see [Zbl 1103.68006].

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q45 Formal languages and automata
Full Text: DOI