Parameter Synthesis for Systems with Real Time - Bezděk, Peter (2018)
Časové automaty se staly standardem pro modelování systémů s časem. Parametrické časové automaty rozšiřují časové automaty o možnost použití parametrů ve strážích a invariantech automatu. Zatímco problém dosažitelnosti hledá valuace parametrů, pro které je daná lokace automatu dosažitelná, problém syntézy parametrů hledá valuace parametrů, pro které je splněna obecnější specifikace parametrického časového automatu, například formule lineární temporální logiky (LTL). V této práci představíme nové výsledky rozhodnutelnosti pro problém dosažitelnosti, zavedeme novou lineární temporální logiku vyjadřující se o hodinách (CA-LTL), a taktéž vyřešíme problém syntézy ohraničených celočíselných parametrů pro LTL a CA-LTL vlastnosti a parametrické časové automaty. Pro parametry s reálnými hodnotami je problém dosažitelnosti nerozhodnutelný. Proto se v práci zaměříme na celočíselné parametry, zatímco čas zůstane spojitý. Dokážeme, že problém dosažitelnosti zůstává nerozhodnutelný pro parametrické