Using non-convex approximations for efficient analysis of timed automata

Authors Frédéric Herbreteau, Dileep Kini, B. Srivathsan, Igor Walukiewicz



PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2011.78.pdf
  • Filesize: 0.53 MB
  • 12 pages

Document Identifiers

Author Details

Frédéric Herbreteau
Dileep Kini
B. Srivathsan
Igor Walukiewicz

Cite As Get BibTex

Frédéric Herbreteau, Dileep Kini, B. Srivathsan, and Igor Walukiewicz. Using non-convex approximations for efficient analysis of timed automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 78-89, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011) https://doi.org/10.4230/LIPIcs.FSTTCS.2011.78

Abstract

The reachability problem for timed automata asks if there exists a
path from an initial state to a target state. The standard
solution to this problem involves computing the zone graph of the
automaton, which in principle could be infinite. In order to make
the graph finite, zones are approximated using an extrapolation
operator. For reasons of efficiency in current algorithms
extrapolation of a zone is always a zone; and in particular it
is convex.

In this paper, we propose to solve the reachability problem without
such extrapolation operators. To ensure termination, we provide an
efficient algorithm to check if a zone is included in the so
called region closure of another. Although theoretically better,
closure cannot be used in the standard algorithm since a closure of
a zone may not be convex.

An additional benefit of the proposed approach is that it permits to
calculate approximating parameters on-the-fly during exploration of
the zone graph, as opposed to the current methods which do it by a
static analysis of the automaton prior to the exploration. This
allows for further improvements in the algorithm. Promising
experimental results are presented.

Subject Classification

Keywords
  • Timed Automata
  • Model-checking
  • Non-convex abstraction
  • On-the-fly abstraction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
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