zbMATH — the first resource for mathematics

Merge and conquer: state merging in parametric timed automata. (English) Zbl 1410.68194
Hung, Dang Van (ed.) et al., Automated technology for verification and analysis. 11th international symposium, ATVA 2013, Hanoi, Vietnam, October 15–18, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8172, 381-396 (2013).
Summary: Parameter synthesis for real-time systems aims at synthesizing dense sets of valuations for the timing requirements, guaranteeing a good behavior. A popular formalism for modeling parameterized real-time systems is parametric timed automata (PTAs). Compacting the state space of PTAs as much as possible is fundamental. We present here a state merging reduction based on convex union, that reduces the state space, but yields an over-approximation of the executable paths. However, we show that it preserves the sets of reachable locations and executable actions. We also show that our merging technique associated with the inverse method, an algorithm for parameter synthesis, preserves locations as well, and outputs larger sets of parameter valuations.
For the entire collection see [Zbl 1291.68023].

68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI