Skip to Main content Skip to Navigation
Journal articles

Integer Parameter Synthesis for Real-Time Systems

Aleksandra Jovanovic 1 Didier Lime 1 Olivier Henri Roux 1
1 STR - STR
LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : We provide a subclass of parametric timed au-tomata (PTA) that we can actually and efficiently analyze, and we argue that it retains most of the practical usefulness of PTA for the modeling of real-time systems. The currently most useful known subclass of PTA, L/U automata, has a strong syntactical restriction for practical purposes, and we show that the associated theoretical results are mixed. We therefore advocate for a different restriction scheme: since in classical timed automata, real-valued clocks are always compared to integers for all practical purposes, we also search for parameter values as bounded integers. We show that the problem of the existence of parameter values such that some TCTL property is satisfied is PSPACE-complete. In such a setting, we can of course synthesize all the values of parameters and we give symbolic algorithms, for reachability and unavoidability properties, to do it efficiently, i.e., without an explicit enumeration. This also has the practical advantage of giving the result as symbolic constraints between the parameters. We finally report on a few experimental results to illustrate the practical usefulness of our approach.
Complete list of metadatas

Cited literature [36 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-02939617
Contributor : Didier Lime <>
Submitted on : Tuesday, September 15, 2020 - 4:57:33 PM
Last modification on : Wednesday, September 30, 2020 - 3:36:06 PM

File

jovanovic-TSE-15.pdf
Files produced by the author(s)

Identifiers

Citation

Aleksandra Jovanovic, Didier Lime, Olivier Henri Roux. Integer Parameter Synthesis for Real-Time Systems. IEEE Transactions on Software Engineering, Institute of Electrical and Electronics Engineers, 2015, 41 (5), pp.445-461. ⟨10.1109/TSE.2014.2357445⟩. ⟨hal-02939617⟩

Share

Metrics

Record views

24

Files downloads

60