A New Data Structure Based on Intervals
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F04%3APU49304" target="_blank" >RIV/00216305:26230/04:PU49304 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
A New Data Structure Based on Intervals
Original language description
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 mmay 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 counterautomata. 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
Czech name
Nová datová struktura postavená nad intervaly
Czech description
Tradiční přístupy k verifikaci RT systémů pracují s časovými modely, kde je čas vyjádřen proměnnými, které se porovnávají vůči explicitním hodnotám (např. celočíselným). Parametrické časované automaty a automaty s čítači používají k definici podmínek nahodinami a čítači parametry. Verifikace automatů s parametry je obecně nerozhodnutelná. Existují však omezené třídy parametrických systémů, které lze pomocí semi-algoritmických přístupů úspěšně verifikovat. Analýza často závisí na efektivitě datové strukktury, která se používá pro vyjádření chování systému. V tomto článku popisuje datové struktury používané pro reprezentaci časovaných automatů a automatů s čítači. Představíme zde novou strukturu založenou na intervalech s parametry pro automaty s čítačia operace nad ní. Tato struktura zjednodušuje některé operace ve srovnání s jinými přístupy.<br>
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
—
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2004
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of MOVEP'04
ISBN
—
ISSN
—
e-ISSN
—
Number of pages
6
Pages from-to
16-21
Publisher name
NEUVEDEN
Place of publication
Bruxelles
Event location
Brusel
Event date
Dec 13, 2004
Type of event by nationality
EUR - Evropská akce
UT code for WoS article
—