MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable

Parametric timed automata extend timed automata (Alur and Dill, 1991) in that they allow the specification of parametric bounds on the clock values. Since their introduction in 1993 by Alur, Henzinger, and Vardi, it is known that the emptiness problem for parametric timed automata with one clock is...

Full description

Bibliographic Details
Main Author: Karin Quaas
Format: Article
Language:English
Published: Open Publishing Association 2014-03-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1404.0087v1