Symbolic Data Structure Based on Intervals for Parametric Verification

Úspěšná analýza časovaných systému s parametry závisí ve velké míře na způsobu representace dat (zejména hodin a čítačů). Tradiční techniky využívají parametrické DBMs (např. TReX) nebo mnohostěny (Hytech). Zde představíme novou datovou strukturu založenou na intervalech a operace nad ní. Tato struktura redukuje stavový prostor potřebný pro uložení data, zjednodušuje některé operace nad daty a rozšiřuje vyjadřovací schopnost při zápisu podmínek nad hranami v modelu ve srovnání s ostatními metodami. Návrh a implementace této struktury je náplní disertační práce autora.