CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishnuXmv is a well-known symbolic model checker, which implements various state-of-the-art algorithms for the analysis of finite- and infinite-state transition systems and temporal logics. In this paper, we present a new version that supports timed systems and logics over continuous super-dense semantics. The system specification was extended with clocks to constrain the timed evolution. The support for temporal properties has been expanded to include MTL0,∞ formulas with parametric intervals. The analysis is performed via a reduction to verification problems in the discrete-time case. The internal representation of traces has been extended to go beyond the lasso-shaped form, to take into account the possible divergence of clocks. We evaluated the new features by comparing nuXmv with other verification tools for timed automata and MTL0,∞ , considering different benchmarks from the literature. The results show that nuXmv is competitive with and in many cases performs better than state-of-the-art tools, especially on validity problems for MTL0,∞ .
| Titolo: | Extending nuXmv with Timed Transition Systems and Timed Temporal Properties |
| Autori: | |
| Data di pubblicazione: | 2019 |
| Serie: | |
| Handle: | http://hdl.handle.net/11582/319344 |
| ISBN: | 978-3-030-25539-8 978-3-030-25540-4 |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
http://hdl.handle.net/11582/319344
Copyright © 2021