Paper Info
Title
On the Expressiveness of Parametric Timed Automata.
Abstract
Parametric timed automata (PTAs) are a powerful formalism to reason about, model and verify real-time systems in which some constraints are unknown, or subject to uncertainty. In the literature, PTAs come in several variants: in particular the domain of parameters can be integers or rationals, and can be bounded or not. Also clocks can either be compared only to a single parameter, or to more complex linear expressions. Yet we do not know how these variants compare in terms of expressiveness, and even the notion of expressiveness for parametric timed models does not exist in the literature. Furthermore, since most interesting problems are undecidable for PTAs, subclasses, such as L/U-PTAs, have been proposed for which some of those problems are decidable. It is not clear however what can actually be modeled with those restricted formalisms and their expressiveness is thus a crucial issue. We therefore propose two definitions for the expressiveness of parametric timed models: the first in terms of all the untimed words that can be generated for all possible valuations of the parameters, the second with the additional information of which parameter valuations allow which word, thus more suitable for synthesis issues. We then use these two definitions to propose a first comparison of the aforementioned PTA variants.
Year
DOI
Venue
2016
10.1007/978-3-319-44878-7_2
Lecture Notes in Computer Science
Keywords
Field
DocType
Parametric timed automata,L/U-PTAs,Hidden parameters
Expression (mathematics),Computer science,Automaton,Theoretical computer science,Decidability,Timed automaton,Parametric statistics,Rotation formalisms in three dimensions,Bounded function,Undecidable problem
Conference
Volume
ISSN
Citations 
9884
0302-9743
5
PageRank 
References 
Authors
0.48
7
3
Name
Order
Citations
PageRank
Étienne André129435.08
didier lime278746.02
olivier h roux367146.30