Detail publikace
A New Data Structure Based on Intervals
Originální název
A New Data Structure Based on Intervals
Anglický název
A New Data Structure Based on Intervals
Jazyk
en
Originální abstrakt
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.
Anglický abstrakt
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.
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"
}