License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FSFMA.2013.18
URN: urn:nbn:de:0030-drops-40855
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4085/
Go to the corresponding OASIcs Volume Portal

André, Étienne

Dynamic Clock Elimination in Parametric Timed Automata

pdf-format:
5.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{andr:OASIcs:2013:4085,
  author =	{{\'E}tienne Andr{\'e}},
  title =	{{Dynamic Clock Elimination in Parametric Timed Automata}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{18--31},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Christine Choppy and Jun Sun},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4085},
  URN =		{urn:nbn:de:0030-drops-40855},
  doi =		{10.4230/OASIcs.FSFMA.2013.18},
  annote =	{Keywords: Verification, Real-time systems, Parameter synthesis, State space reduction, Inverse Method}
}

Keywords: Verification, Real-time systems, Parameter synthesis, State space reduction, Inverse Method
Collection: 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Issue Date: 2013
Date of publication: 14.07.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI