CINECA IRIS Institutional Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishHybrid systems are a powerful formalism for modeling cyber-physical systems. Reachability analysis is a general method for checking safety properties, especially in the presence of uncertainty and non-determinism. Rigorous simulation is a convenient tool for reachability analysis of hybrid systems. However, to serve as proof tool, a rigorous simulator must be correct wrt a clearly defined notion of reachability,which captures what is intuitively eachable in finite time. As a step towards addressing this challenge, this paper presents a rigorous simulator in the form of an operational semantics and a specification in the form of a denotational semantics. We show that, under certain conditions about the representation of enclosures, the rigorous simulator is correct. We also show that finding a representation satisfying these assumptions is non-trivial.
| Titolo: | A Semantic Account of Rigorous Simulation |
| Autori: | |
| Data di pubblicazione: | 2018 |
| Handle: | http://hdl.handle.net/11567/914208 |
| ISBN: | 978-3-319-95245-1 978-3-319-95246-8 |
| Appare nelle tipologie: | 02.01 - Contributo in volume (Capitolo o saggio) |
File in questo prodotto:
| File | Descrizione | Tipologia | |
|---|---|---|---|
| EAL17.pdf | Pre-print articolo principale | Documento in Post-print | Open Access Visualizza/Apri |
Copyright © 2021