Parameter Synthesis for Systems with Real Time /
Č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 s...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2018
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/i4kyb/ |
| Shrnutí: | Č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é For modelling of behaviour with time aspects the timed extension of nondeterministic finite automata called timed automata became the standard. Parametric timed automata extend the timed automata with the possibility to use parameters in the clock constraints. While the reachability problem for parametric timed automata computes parameter valuations for which certain locations are reachable, the parameter synthesis problem computes parameter valuations for which a more general type of specification is satisfied, e.g. linear temporal logic (LTL) formula. In the thesis we provide new decidability results for the reachability problem, we introduce new clock-aware linear temporal logic (CA-LTL) as an extension of LTL, and we solve the parameter synthesis problem for CA-LTL properties and restricted parameters. In general, if the parameters are real-valued, the reachability problem for parametric timed automata is undecidable even for various restricted subclasses. We thus focus on the cas |
|---|---|
| Popis jednotky: | Vedoucí práce: Ivana Černá |
| Fyzický popis: | 120 stran |