Publication detail

A New Data Structure Based on Intervals

MATOUŠEK, P.

Original Title

A New Data Structure Based on Intervals

English Title

A New Data Structure Based on Intervals

Type

conference paper

Language

en

Original Abstract

 Traditional approaches to the verification of real-time systems deal with timed models where time is expressed by variables that are compared with explicite values (e.g., integers). Parametric timed and counter models use parameters to define constraints over clocks or counters. Verification of automata with parameters is generally   undecidable. However, it is decidable for some restricted   classes of parametric systems and moreover many practical system outside of these classes may be successfully verified using semi-algorithms. Analysis  mostly depends on the efficient data structure that is used to express behavior of the system. In this paper we discuss data structures used for representation of timed and  counter automata. We introduce a new data structure based on parametrized intervals for counter automata and operation that are needed for verification. This structure makes operations over  parametric counter automata simple in comparison to other approaches.

English abstract

 Traditional approaches to the verification of real-time systems deal with timed models where time is expressed by variables that are compared with explicite values (e.g., integers). Parametric timed and counter models use parameters to define constraints over clocks or counters. Verification of automata with parameters is generally   undecidable. However, it is decidable for some restricted   classes of parametric systems and moreover many practical system outside of these classes may be successfully verified using semi-algorithms. Analysis  mostly depends on the efficient data structure that is used to express behavior of the system. In this paper we discuss data structures used for representation of timed and  counter automata. We introduce a new data structure based on parametrized intervals for counter automata and operation that are needed for verification. This structure makes operations over  parametric counter automata simple in comparison to other approaches.

Keywords

parametric verification, symbolic data structure, intervals

RIV year

2004

Released

20.12.2004

Location

Bruxelles

Pages from

16

Pages to

21

Pages count

6

URL

Documents

BibTex


@inproceedings{BUT17590,
  author="Petr {Matoušek}",
  title="A New Data Structure Based on Intervals",
  annote=" Traditional approaches to the verification of real-time systems
deal with timed models where time is expressed by variables that are
compared with explicite values (e.g., integers). Parametric timed and
counter models use parameters to define constraints over clocks or
counters. Verification of automata with parameters is
generally   undecidable. However, it is decidable for some
restricted   classes of parametric systems and moreover many
practical system outside of these classes may be successfully verified
using semi-algorithms. Analysis  mostly depends on the efficient
data structure that is used to express behavior of the system. In this
paper we discuss data structures used for representation of timed
and  counter automata. We introduce a new data structure based on
parametrized intervals for counter automata and operation that are
needed for verification. This structure makes operations over 
parametric counter automata simple in comparison to other approaches.

", booktitle="Proceedings of MOVEP'04", chapter="17590", year="2004", month="december", pages="16--21", type="conference paper" }