Document Open Access Logo

Dynamic Clock Elimination in Parametric Timed Automata

Author Étienne André

PDF

File

Thumbnail PDF
PDF
OASIcs.FSFMA.2013.18.pdf
  • Filesize: 0.56 MB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • Verification
  • Real-time systems
  • Parameter synthesis
  • State space reduction
  • Inverse Method

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

The formalism of parametric timed automata provides designers with a formal way to specify and verify real-time concurrent systems where iming requirements are unknown (or parameters). Such models are usually subject to the state space explosion. A popular way to partially reduce the size of the state space is to reduce the number of clock variables. In this work, we present a technique for dynamically eliminating clocks. Experiments using IMITATOR show a diminution of the number of states and of the computation time, and in some cases allow termination of the analysis of models that could not terminate otherwise. More surprisingly, even when the number of clocks remains constant, there is little noticeable overhead in applying the proposed clock elimination.

Cite As Get BibTex

Étienne André. Dynamic Clock Elimination in Parametric Timed Automata. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 18-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013) https://doi.org/10.4230/OASIcs.FSFMA.2013.18

Author Details

Étienne André
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact